TimeZoneSeries may produce overlapping LocalTime intervals

[olafklinke]

One of the potential use cases for TimeZoneSeries is daylight savings time (DST). (related to another issue: infinite lists of time zone changes?) While the UTC time intervals of DST and non-DST do not overlap, their mapping to ZonedTime and then to LocalTime will produce overlaps. This entails that localTimeToUTC' has more than one candidate UTCTime for a LocalTime inside the overlap. Moreover, some LocalTime values should actually be illegal for a DST/non-DST TimeZoneSeries object, because clocks jump forward. By the use of listToMaybe inside localTimeToUTC' the function currently disregards any extra candidates and by the use of fromMaybe it accepts illegal time stamps.

So either the return type of localTimeToUTC' is changed to [UTCTime] or we provide heuristics to guess the correct TimeZone from context. I actually implemented the latter, but haven't published yet. The use case is series of LocalTime stamps that are known to be ascending in UTCTime and belong to a known TimeZoneSeries. These are common. As a data scientist I deal with such time series every day. Question is whether handling of such series is within the scope of this package.

[ygale]

@olafklinke Yes, that use case is definitely in scope. This library explicitly supports series whose local time intervals overlap or have gaps. See the comments in the source code for a detailed explanation of the algorithm we use to support those, and a proof of its correctness.

The type signature of localTimeToUTC’ was chosen to be backward-compatible with the signature of the similarly named function in the time library. This makes it easier for it to be used as a drop-in replacement. However, it does force us to provide exactly one UTCTime for every LocalTime. So we need to make a somewhat arbitrary choice in the case of a redundant or invalid LocalTime. See the haddocks for a specification of what we choose. The functions isValidLocalTime and isRedundantLocalTime are provided to detect these situations.

I agree with you that it would be great to provide a variant with the more semantically correct (but non-backwards-compatible) return type of [UTCTime]. I would name it something like localTimeToUTCs. If you would like to provide such a function in a PR, it would be much appreciated.

[olafklinke]

I was trying to define an invariant for localTimeToUTC' that documents how converting a sequence of UTCTime values to LocalTime and back is the identity, but then I stumbled upon another issue.

[ygale]

Please update your invariant as noted in that issue, and let me know how it goes.

[olafklinke]

Is the following invariant desired?

Fix a TimeZoneSeries. An ascending sequence of UTCTime values is mapped to ZonedTime using utcToLocalTime' and only the LocalTime component is kept. For each LocalTime value, the TimeZone according to the series is computed by localTimeToUTC' and timeZoneFromSeries and a new ZonedTime value is constructed. Invariant: The new ZonedTime value should be identical to the original one.

Below is code demonstrating that this invariant does not hold for timezone-series-0.1.13.
Proposed solution: Add an algorithm that, for timestamps that satisfy isRedundantLocalTime, chooses the right TimeZone from the context, that is, the preceding and following LocalTime.

import Data.Time
import Data.Time.LocalTime.TimeZone.Series
import Data.List (unfoldr)
import Data.Function (on)

-- central European time: UTC+1
cet = TimeZone {
    timeZoneMinutes = 60,
    timeZoneSummerOnly = False,
    timeZoneName = "CET"}

-- central European daylight savings time: UTC+2
cest = TimeZone {
    timeZoneMinutes = 120,
    timeZoneSummerOnly = True,
    timeZoneName = "CEST"}

-- change happens at last Sunday in March and October at 1:00 UTC
centralEurope :: TimeZoneSeries
centralEurope = TimeZoneSeries {
    tzsTimeZone = cet,
    tzsTransitions = [
        (UTCTime (fromGregorian 2021 10 31) (secondsToDiffTime 3600),cet),
        (UTCTime (fromGregorian 2021  3 28) (secondsToDiffTime 3600),cest)]
    }

-- generate an ascending series
genAscendingUTC :: UTCTime -> NominalDiffTime -> UTCTime ->
    [UTCTime]
genAscendingUTC t0 step t1 = unfoldr f t0 where
    f t = if t <= t1 then Just (t,addUTCTime step t) else Nothing

utcToZonedTime' :: TimeZoneSeries -> UTCTime -> ZonedTime
utcToZonedTime' region u = ZonedTime (utcToLocalTime' region u) (timeZoneFromSeries region u)

-- * Invariants
implies :: Bool -> Bool -> Bool
implies a b = not a || b

-- Invariant: 
-- 
-- prop> all (\z -> z `asInSeries` region) (genAscendingZonedTime region t0 step t1)
genAscendingZonedTime :: TimeZoneSeries ->
    UTCTime -> NominalDiffTime -> UTCTime ->
    [ZonedTime]
genAscendingZonedTime region t0 step t1 = fmap
    (utcToZonedTime' region)
    (genAscendingUTC t0 step t1)

localTimeToZonedTime :: TimeZoneSeries -> LocalTime -> ZonedTime
localTimeToZonedTime region l = let
    u = localTimeToUTC' region l
    z = timeZoneFromSeries region u
    in ZonedTime (utcToLocalTime z u) z

-- The invariants below are only expected to hold
-- when the TimeZone is as specified by the TimeZoneSeries. 
asInSeries :: ZonedTime -> TimeZoneSeries -> Bool
t `asInSeries` region = (utcToZonedTime' region (zonedTimeToUTC t)) `identical` t

-- ZonedTime has no Eq instance
identical :: ZonedTime -> ZonedTime -> Bool
identical = (==) `on` (\z -> (zonedTimeToLocalTime z,zonedTimeZone z))

-- This invariant holds.
invariantPlusInfinity :: UTCTime -> TimeZoneSeries -> Bool
invariantPlusInfinity t tzs = (t > (fst.head.tzsTransitions) tzs) `implies` (timeZoneFromSeries tzs t ==  (snd.head.tzsTransitions) tzs)

-- This invariant implies 
-- 
-- @
-- id = zonedTimeToUTC . localTimeToZonedTime region . zonedTimeToLocalTime . utcToZonedTime' region
-- @
invariantZonedTime :: TimeZoneSeries -> ZonedTime -> Bool
invariantZonedTime region z = (z `asInSeries` region) `implies` (z `identical` (localTimeToZonedTime region . zonedTimeToLocalTime) z)

-- @all (invariantZonedTime centralEurope) counterexample == False@
counterexample :: [ZonedTime]
counterexample = let
    t0 = (addUTCTime (-4000).fst.head.tzsTransitions) centralEurope
    t1 = (addUTCTime (4000) .fst.head.tzsTransitions) centralEurope
    in genAscendingZonedTime centralEurope t0 600 t1