Gaps and Overlaps in TimeZoneSeries

The Data.Time.LocalTime.TimeZone.Series module in Haskell provides the TimeZoneSeries datatype, and functions to work with it. A TimeZoneSeries describes the various clock settings that occur in a single time zone. This module is available in the timezone-series package on Hackage.

Invalid and redundant clock times

When a clock change moves the clock forward, the local times in the range between the times just before and just after the clock change cannot occur. We say that these times are "invalid".

Similarly, when a clock change moves the clock backward, the local times in the range between the times just after and just before the clock change occur twice. We say that these times are "redundant".

The functions isValidLocalTime and isRedundantLocalTime in Data.Time.LocalTime.TimeZone.Series allow you to determine whether a local time is invalid or redundant for a given TimeZoneSeries.

Jittery time change rules

Theoretically, a TimeZoneSeries could describe a very complex and jittery set of time change rules that move the clock back and forth several times across the same clock time.

Although this scenario is unlikely to occur in a real time zone, the isValidLocalTime and isRedundantLocalTime functions are designed to handle these cases correctly.

To do so, they use the following fact:

Theorem: If G is the set of individual time changes for which clock time t is invalid ("in the Gap"), and O is the set of individual time changes for which t is redundant ("in the Overlap"), then t is invalid for the full set of changes iff #G > #O, and t is redundant for the full set of changes iff #G < #O.

A proof of the Gaps and Overlap Theorem

Aristid Breitkreuz has provided the following proof for this theorem.

  1. A relevant gap followed by a relevant overlap means that the first leg of the overlap is invalidated, but the second leg remains, so it's neither redundant nor invalid.
  2. A relevant overlap followed by a relevant gap means that the second leg of the overlap is invalidated, leaving the first.
  3. There cannot be two consecutive relevant gaps, because a gap ends at a higher time than it starts, and a consecutive gap must start after the first gap has ended.

Now, let's look at the three cases of the different lengths:

  1. There are more overlaps than gaps. This means that all gaps can be ignored, because they must be paired with overlaps. Therefore, there is at least one remaining overlap, resulting in redundant times.
  2. There are more gaps than overlaps. This means that there is exactly one more gap than overlaps, and that there are no consecutive overlaps, because otherwise there would be consecutive gaps. Therefore, all overlaps can be paired with gaps, leaving exactly one gap, resulting in an invalid time.
  3. There are exactly as much gaps as overlaps. To avoid consecutive gaps, their order must be GOGOGO... or OGOGOG..., resulting in full elimination, and exactly one non-redundant valid time.

This completes the proof.