Narrowing a date and time

Copy Markdown View Source

Narrowing › date and time. The names in the examples are those of section 2.

A date and time alternative is the bare kind or {:date_and_time, set}: a set of the second a value falls in, on the lines of Feel.Type.Moment (D-109, D-118). The page for time explains the lines: the clock of the values with no zone, and the instant and the zoned clock of those with one, which is needed because the order of two of them depends on their zones. any zone means the set has the clock and the instants of every zone. A date and time is not a date: they are of different kinds, so each is left only by its own.

Comparisons

With a value that has no zone the comparison is on the clock, and the set is a plain interval (any zone). With one that has a zone the values with no zone are compared by their clock, and the values with a zone by their instant, so the set has the lines:

Conditiondt when truedt when not true
dt < @"2024-01-01T00:00:00"date and time in [-999999999-01-01T00:00:00..2024-01-01T00:00:00) any zonedate and time in [2024-01-01T00:00:00..999999999-12-31T23:59:59] any zone | Null
dt >= @"2024-01-01T00:00:00Z"date and time in [2024-01-01T00:00:00..999999999-12-31T23:59:59], instants [2024-01-01T00:00:00Z..1000000000-01-01T17:59:59Z]date and time in [-999999999-01-01T00:00:00..2024-01-01T00:00:00), instants [-1000000000-12-31T06:00:00Z..2024-01-01T00:00:00Z) | Null
dt < d—date and time | Null
dt instance of date and timedate and timeNull

The instants reach past the end of the calendar (1000000000-01-01T17:59:59Z) because the last clock in an offset of −18 hours is that many hours later in UTC.

Conditiondtr when truedtr when not true
dtr < @"2024-01-15T12:00:00"date and time in [2024-01-01T00:00:00..2024-01-15T12:00:00) any zonedate and time in [2024-01-15T12:00:00..2024-01-31T23:59:59] any zone | Null
dtr = @"2024-01-15T12:00:00"date and time = 2024-01-15T12:00:00 any zonedate and time in [2024-01-01T00:00:00..2024-01-15T12:00:00), (2024-01-15T12:00:00..2024-01-31T23:59:59] any zone | Null
dtr >= @"2024-01-15T12:00:00Z"date and time in [2024-01-15T12:00:00..2024-01-31T23:59:59], zoned clock [2024-01-14T18:00:00..2024-01-31T23:59:59], instants [2024-01-15T12:00:00Z..2024-02-01T17:59:59Z]date and time in [2024-01-01T00:00:00..2024-01-15T12:00:00), zoned clock [2024-01-01T00:00:00..2024-01-16T06:00:00], instants [2023-12-31T06:00:00Z..2024-01-15T12:00:00Z) | Null

(dtr is a date and time in [2024-01-01T00:00:00..2024-01-31T23:59:59]; dt is any.) The last row has all three lines: a value with no zone is on the clock line; one with a zone has both its zoned clock and its instant in the set. The zoned clock of a value whose instant is at noon UTC is between 18:00 the day before (an offset of −18 hours) and 06:00 the day after.

Properties

A fact about year, month, day, weekday, hour, minute or second is a fact about the value: the seconds of the set that have it, on each line of clocks, the instants cut to match (D-109). It narrows only as far as the set is bounded, as for a date: the days are exact, the hours, minutes and seconds are counted from one end to the other of each interval up to a number of pieces, and beyond that number the set is left as it was.

Conditiondt when truedt when not true
dt.year = 2024date and time in [2024-01-01T00:00:00..2024-12-31T23:59:59] any zonedate and time in [-999999999-01-01T00:00:00..2023-12-31T23:59:59], [2025-01-01T00:00:00..999999999-12-31T23:59:59] any zone | Null
dt.hour >= 18date and timedate and time | Null
Conditiondtr when truedtr when not true
dtr.day = 15date and time in [2024-01-15T00:00:00..2024-01-15T23:59:59] any zonedate and time in [2024-01-01T00:00:00..2024-01-14T23:59:59], [2024-01-16T00:00:00..2024-01-31T23:59:59] any zone | Null
dtr.hour >= 18date and time in [2024-01-01T18:00:00..2024-01-31T23:59:59] any zonedate and time in [2024-01-01T00:00:00..2024-01-31T23:59:59] any zone | Null
dtr.day = 15 and dtr.hour >= 18date and time in [2024-01-15T00:00:00..2024-01-15T23:59:59] any zonedate and time in [2024-01-01T00:00:00..2024-01-31T23:59:59] any zone | Null
dtr.weekday = 1date and time in [2024-01-01T00:00:00..2024-01-29T23:59:59] any zonedate and time in [2024-01-02T00:00:00..2024-01-31T23:59:59] any zone | Null
dtr.year = 2024date and time in [2024-01-01T00:00:00..2024-01-31T23:59:59] any zoneNull
dtr.month = 2—date and time in [2024-01-01T00:00:00..2024-01-31T23:59:59] any zone | Null
  • dt.hour >= 18 on an unbounded value narrows nothing: the hours come back every day.
  • dtr.hour >= 18 is the hull, from six in the evening of the first day to the end of the last: a superset, and the best that one interval can say. dtr.day = 15 and dtr.hour >= 18 is no narrower than the day, because the hour would make a piece for each day.
  • dtr.year = 2024 is true for every value of the set, so only null is left when it is not.
  • dtr.month = 2 cannot be true for a value in January.

The properties of the zone

time offset, timezone and value exist only for a value that has a zone. A true fact about one therefore leaves the instants only:

Conditiondt when truedt when not true
dt.timezone = "Z"date and time in instants [-1000000000-12-31T06:00:00Z..1000000000-01-01T17:59:59Z]date and time | Null
dt.time offset = @"PT0S"date and time in instants [-999999999-01-01T00:00:00Z..999999999-12-31T23:59:59Z]date and time | Null

dt.value > 0 (the seconds since 1970 of the instant) leaves the instants from 1969-12-31T23:59:59Z on. They are worked out by Feel.Analysis.MomentZones (D-109).

Limits

  • The lines of the instants and the zoned clock are each within 18 hours of the other, and are cut to that.
  • A set of more than the pieces a property can keep is left as it was.
  • The fraction of the second is a line of its own, [0..1) when nothing is known. A condition on second (dtr.second < 30) narrows nothing: a second comes back in every minute.

See also: time, date, days and time duration.