std.zoneddatetime

A date and time of day in a time zone: 2024-03-10T03:00:00-04:00 in America/New_York, what the clocks there said, at the offset they were at — an instant (std.instant), and how it was read there. NodaTime’s ZonedDateTime is the model: a std.localdatetime, a std.datetimezone, and the zone’s offset there, a std.offset. An instant is one in a zone (at). A date and time on its clocks is one by resolve, which the program tells what a date-time the clocks skipped over becomes, and one they went back over (NodaTime’s ZoneLocalMappingResolver): none is chosen for it. Two are equal where their date-times, offsets and zones are; they have no order, as std.offsetdatetime’s have none — compare their instants. Import it by a name, import std.zoneddatetime as ZonedDateTime, as its names are short.

import std.datetimezone as DateTimeZone
import std.localdatetime as LocalDateTime
import std.zoneddatetime as ZonedDateTime

-- | a meeting at a date and time in New York, said so: a time skipped
-- | in spring is moved on by the gap, one repeated in autumn is the
-- | first
-- | >>> List.map meeting ["2024-03-10T02:30:00", "2024-11-03T01:30:00"]
-- | ["2024-03-10T03:30:00-04:00[EST5EDT,M3.2.0,M11.1.0]", "2024-11-03T01:30:00-04:00[EST5EDT,M3.2.0,M11.1.0]"]
meeting : String -> String
meeting s =
  case (DateTimeZone.fromPosix "EST5EDT,M3.2.0,M11.1.0", LocalDateTime.parse s) of
    (Just zone, Just t) ->
      maybe
        ""
        show
        (ZonedDateTime.resolve
           { skipped = ShiftForward, ambiguous = Earlier }
           zone
           t)
    _ -> ""

ZonedDateTime

data ZonedDateTime

A date-time in a zone: the date and time of day its clocks say, the offset they are at, and the zone.

SkippedTime

data SkippedTime = Earlier | Later | ShiftForward | Fail

What a date-time the zone’s clocks skipped over becomes: the last instant before the gap, at the offset before it (Earlier); the instant the gap ends, at the offset after it (Later); the instant it is at the offset before the gap, so the date-time moved on by the gap’s length (ShiftForward), as NodaTime’s lenient resolver has it; or none (Fail).

AmbiguousTime

data AmbiguousTime = Earlier | Later | Fail

What a date-time the zone’s clocks went back over, so twice, becomes: the earlier of its two instants (Earlier), the later (Later), or none (Fail).

Resolver

type Resolver = { skipped : SkippedTime, ambiguous : AmbiguousTime }

What a date-time is resolved by, where it is not one instant in the zone: one skipped over, one gone back over.

lenient

lenient : Resolver

NodaTime’s lenient resolver: a date-time skipped over moved on by the gap, one gone back over the earlier.

strict

strict : Resolver

Neither resolved: none for a date-time skipped over or gone back over, NodaTime’s strict resolver.

local

local : ZonedDateTime -> LocalDateTime.LocalDateTime

Its date and time of day, as the zone’s clocks say it.

offset

offset : ZonedDateTime -> Offset.Offset

The offset of the zone’s clocks then.

zone

zone : ZonedDateTime -> DateTimeZone.DateTimeZone

Its zone.

toOffsetDateTime

toOffsetDateTime : ZonedDateTime -> OffsetDateTime.OffsetDateTime

The date-time at its offset, without the zone.

instanceEqualityZonedDateTime

instance instanceEqualityZonedDateTime : Equality ZonedDateTime

The same date-time at the same offset in the same zone, as NodaTime has it: the same instant in two zones is two values.

instanceDebugZonedDateTime

instance instanceDebugZonedDateTime : Debug ZonedDateTime

As show writes it, 2024-03-10T03:00:00-04:00[America/New_York].

instanceShowZonedDateTime

instance instanceShowZonedDateTime : Show ZonedDateTime

As RFC 9557 writes it, as Java’s ZonedDateTime does: the date-time at its offset as std.offsetdatetime writes it, then the zone’s id in brackets (2024-03-10T03:00:00-04:00[America/New_York]).

at

at : Instant.Instant -> DateTimeZone.DateTimeZone -> ZonedDateTime

The instant in the zone: its date and time there, at the zone’s offset then.

>>> show (at Instant.epoch DateTimeZone.utc)
"1970-01-01T00:00:00Z[UTC]"
>>> at Instant.epoch DateTimeZone.utc == at Instant.epoch DateTimeZone.utc
True
>>> maybe True (\o -> at Instant.epoch DateTimeZone.utc == at Instant.epoch (DateTimeZone.fixed o)) (Offset.fromHours 8)
False

instant

instant : ZonedDateTime -> Instant.Instant

The instant it is: its date-time less its offset.

plus

plus : ZonedDateTime -> Duration.Duration -> ZonedDateTime

The date-time the duration after it, in its zone: so an hour after 01:30 on the day the clocks go forward at 02:00 is 03:30.

>>> maybe "" (\o -> show (plus (at Instant.epoch (DateTimeZone.fixed o)) (Duration.hours 1))) (Offset.fromHours 8)
"1970-01-01T09:00:00+08:00[UTC+08:00]"

resolve

resolve : Resolver
        -> DateTimeZone.DateTimeZone
        -> LocalDateTime.LocalDateTime
        -> Maybe ZonedDateTime

The date and time on the zone’s clocks, as one instant there: where it is one, that; where the clocks skipped over it, or went back over it, what the resolver says — none where it says Fail (std.datetimezone’s mapLocal tells which it was).

>>> List.map (\r -> maybe "" (\z -> maybe "" (\t -> maybe "none" show (resolve r z t)) (LocalDateTime.parse "2024-03-10T02:30:00")) (DateTimeZone.fromPosix "EST5EDT,M3.2.0,M11.1.0")) [{ skipped = Earlier, ambiguous = Fail }, { skipped = Later, ambiguous = Fail }, lenient, strict]
["2024-03-10T01:59:59.999999999-05:00[EST5EDT,M3.2.0,M11.1.0]", "2024-03-10T03:00:00-04:00[EST5EDT,M3.2.0,M11.1.0]", "2024-03-10T03:30:00-04:00[EST5EDT,M3.2.0,M11.1.0]", "none"]
>>> List.map (\r -> maybe "" (\z -> maybe "" (\t -> maybe "none" show (resolve r z t)) (LocalDateTime.parse "2024-11-03T01:30:00")) (DateTimeZone.fromPosix "EST5EDT,M3.2.0,M11.1.0")) [{ skipped = Fail, ambiguous = Earlier }, { skipped = Fail, ambiguous = Later }, strict]
["2024-11-03T01:30:00-04:00[EST5EDT,M3.2.0,M11.1.0]", "2024-11-03T01:30:00-05:00[EST5EDT,M3.2.0,M11.1.0]", "none"]
>>> maybe "" (\t -> maybe "none" show (resolve strict DateTimeZone.utc t)) (LocalDateTime.parse "2024-03-10T02:30:00")
"2024-03-10T02:30:00Z[UTC]"