std.tzdb

The tz database the system keeps: its zones read from their files, as NodaTime’s DateTimeZoneProviders.Tzdb gives them, and the zone the system is set to. A zone is named by its id in the IANA tz database, Asia/Taipei, America/New_York, UTC, the path of its TZif file under the system’s zoneinfo directory, /usr/share/zoneinfo on macOS (a link to the system’s own copy) and on Linux; the file is read by std.filesystem, and std.datetimezone’s fromTZif reads its bytes, in the program, so the data is the system’s, updated with it, and no libc time-zone function is called. Windows keeps no tz database: there a zone is not found, and the error says so.

What could not be read is thrown as a ZoneError, over the exception effect. Import it by a name, import std.tzdb as TZDB, as its names are short.

import co
import exception
import std.filesystem
import std.instant as Instant
import std.tzdb as TZDB
import std.zoneddatetime as ZonedDateTime

-- | the instant as the clocks of Taipei tell it
inTaipei : {e : HFunctor}
         -> {{disk : filesystem <: e}}
         -> {{ex : exception TZDB.ZoneError <: e}}
         -> Instant.Instant
         -> Co e String
inTaipei t = do
  taipei <- TZDB.zone "Asia/Taipei"
  pure (show (ZonedDateTime.at t taipei))

ZoneError

type ZoneError = { id : String, message : String }

Why a zone could not be had: the id it was asked by (for the system’s own, what TZ says, or localtime), and why.

instanceShowZoneError

instance instanceShowZoneError : Show ZoneError

As a system’s tools say it: the id, and why.

>>> show ({ id = "Asia/Taipe", message = "/usr/share/zoneinfo/Asia/Taipe: ENOENT: No such file or directory" } : ZoneError)
"Asia/Taipe: /usr/share/zoneinfo/Asia/Taipe: ENOENT: No such file or directory"

directory

directory : String

Where the system keeps the tz database, its zones’ TZif files: /usr/share/zoneinfo.

zoneIn

zoneIn : {e : HFunctor}
       -> {{disk : filesystem <: e}}
       -> {{ex : exception ZoneError <: e}}
       -> String
       -> String
       -> Co e DateTimeZone.DateTimeZone

The zone of the id, Asia/Taipei, as the TZif files under the directory dir have it. A ZoneError where the id is none (a path out of the directory, ../x, or empty), there is no directory, or the file cannot be read or is no TZif.

zone

zone : {e : HFunctor}
     -> {{disk : filesystem <: e}}
     -> {{ex : exception ZoneError <: e}}
     -> String
     -> Co e DateTimeZone.DateTimeZone

The zone of the id, Asia/Taipei, as the system’s tz database has it, at directory. A ZoneError where the id is none, there is no tz database there (as on Windows), or its file cannot be read or is no TZif.

system

system : {e : HFunctor}
       -> {{disk : filesystem <: e}}
       -> {{env : process <: e}}
       -> {{ex : exception ZoneError <: e}}
       -> Co e DateTimeZone.DateTimeZone

The zone the system is set to, as the tz code reads it: the environment’s TZ if it is set — empty, UTC; a path, /..., the TZif file there; an id of the tz database, Asia/Taipei, its zone; else a POSIX rule, EST5EDT,M3.2.0,M11.1.0, a : before any of them passed over — and else /etc/localtime, its id where it links in the tz database (localtime if not), and UTC where there is none. A ZoneError where TZ names no zone, or a file cannot be read or is no TZif.