[ANN] Hodatime - Batteries included Date/time library

Announcements
1

Hodatime is a date and time library for Haskell, inspired by Noda Time (itself, inspired by Joda Time) and Erik Naggum’s “The Long, Painful History of Time”.

This library is intended to be batteries included, which is in contrast to most of the existing Haskell date time work (elegant as they are). It continues the work of Jodatime and Nodatime, distinguishing between civil and physical time but, just as Nodatime tightened the type safety of Jodatime, Hodatime excludes even more incorrect code due to Haskell’s type system.

Highlights:

* Multiple calendars — Gregorian, ISO, Julian, Coptic, Persian (astronomical Solar Hijri), Islamic (parameterised over the leap-year rule), and Hebrew — with lossless conversion between them.

* Time zones read from the operating system (the IANA/Olson database on Unix, the registry on Windows), with explicit handling of skipped/ambiguous local times.

* A composable pattern system where one field definition yields both a parser and a formatter, so the two can’t drift apart.

* Locale-aware formatting driven by the host’s own locale data.

Internally an instant is counted from 1 March 2000, not the Unix epoch. The reasons, as discussed in Naggum’s work are: starting the year in March pushes February — and its awkward leap day — to the end of the year, so the leap day never shifts the offsets of any other month and the date arithmetic stays uniform. And anchoring at 2000, a leap year that begins a fresh 400-year Gregorian cycle, makes the internal cycle/century/day-in-century breakdown fall out cleanly. Each calendar is free to use whatever epoch is most natural for its own math; the shift onto the shared timeline happens only at the boundary.

It’s BSD-3-licensed, builds across GHC 9.4–9.10 on Linux/macOS/Windows, and has quietly been in development for years — 1.0 is the first release I’ve actually announced. Feedback very welcome.

22 Likes
2

Links:

5 Likes
3

Interesting! I note you don’t have a (physical) Day type, to represent some day without reference to any particular calendar?

My approach in time was (mostly) to use types for physical things, and constructors/patterns for civil interpretations of physical things. For example, pattern YearMonthDay :: Integer -> Int -> Int -> Day interprets physical days into the Gregorian calendar.

Also, if you have a single type that contains both parser and formatter, it has some interesting composability properties if you get it right. I made a library for this. For example:

(<***>) :: f a -> f b -> f (a, b)  -- for concatenation
(<+++>) :: f a -> f b -> f (Either a b)  -- for alternation
4 Likes
4

Hi, it’s an honour to get noticed by the author of `time`! :slight_smile:

For me, time is extremely well thought out and correct but very “skinny”. Anything and everything can be built on it but most related functionality in an application would come from including additional libraries, or writing custom code for most of the applications I write. For example, I noticed that doing work in time zones actually requires two additional libraries, neither of which seem to do anything on their own (I should mention, this is from memory from when I first started this library years ago so it might not be accurate anymore). This is definitely consistent with how libraries seem to generally be done within the Haskell ecosystem.

Hodatime is a purposeful departure from some established Haskell conventions: one library that tries to do everything related to the subject (i.e. “batteries included”). It also purposely uses full encapsulation/information hiding; we don’t expose “Internal” modules (it looks like time does as well) as a design goal.

I could have probably just used time as a base and build some “gather everything in one place” type library and added e.g. extra calendars as separate libraries but I also wanted to play around with the epochs because I was quite taken with Erik Naggum’s work and was interested if there were other mathematically interesting epochs in other calendars. Hodatime itself just iterates on the concepts established originally with Java’s famous JodaTime, that was made a bit more type safe in C#'s NodaTime. At the moment, I’m exploring an implementation in Idris as well to make it even more type safe (e.g. calenderDate 29 February 2001 shouldn’t compile).

As for the formats, this was also stolen and adapted from NodaTime. I don’t know if they’re correct enough but it’s definitely worth looking at. Thanks for the tip.

EDIT: I guess the analogue to your Day concept, in Hodatime would be Instant. An Instant is a physical component of an exact instant in time with no regard to any calendar. There are functions to convert between an Instant and a Calendar system. ZonedDateTime being one such which keeps the nature of Instant being unambiguous across the entire timeline.

6 Likes
5

Yeah, there’s actually an issue to fix this, when I get around to it…

1 Like
6

Ah ok. I wasn’t really considering it a defect per se. It makes sense in a fast moving, research aspect to make decisions granular so pieces can be mixed and matched and swapped out until a solid consensus is found. My library was going more for the other end of the spectrum.

One thing I was just thinking about is, from a design perspective, a big difference is Hodatime wants everything to be in a type and stay there. Like time has Day and there are e.g. functions when render Day into a Gregorian interpretation but, as far as I can see, they don’t hold that shape, they’re just numbers afterwards. Which means one has to be sure that any “civil” or calendar type work is done with matching calendars (e.g. do all the work in one function so you can see it’s always Gregorian). In Hodatime, you would need to convert to a ZonedDateTime or CalendarDate to do this kind of math and then the calendar is part of the type so you can never accidentally mix e.g. Julian with Gregorian.

1 Like
8

Many examples of this kind of thing, but I prefer doing them as profunctors so you get one contravariant and one covariant type parameter, rather than an invariant type parameter. That gives you a wider range of choices for how you compose them.

See

2 Likes
9

I’ve already had to release 1.1.0.0: the “lens like” interface I was providing was actually not valid lenses since no fields can be changed in “date” based types or “time” based types without potentially affecting other fields. So I’ve introduced the “Periods” interface used in Nodatime but with tighter type safety.

10

Time is a vast subject. One of the aspects I personally have had much headache with is converting LocalTime to Instant (via ZonedDateTime) within some calendar/time zone context. This problem will pop up each time you import timed data from a source that does not provide explicit TZ info (Excel, databases). timezone-series attempts to do this but in my opinion its guarantees are too weak.
Would anyone be interested in writing and proving correctness of a time-zone-guessing library that properly round-trips? Perhaps as part of Hodatime-1.2? It seems the foundations are laid in resolve.
The global basic assumption for a time series is that whatever representation is given, it stems from a series of non-descending Instants. I have some heuristic code to start with, but it is currently specialized to my particular locale.

11

What do you mean by “time-zone-guessing”? How would the guessing be accomplished? If it would require some heuristic over multiple entries then that’s for sure outside the scope here, though this library can definitely provide the tools to do it. Also, keep in mind that you don’t have to use a time zone, you can also use UTC or just pick a specific Offset for the time zone part.

12

There is a forgetful mapping ZonedDateTime -> LocalTime. Given a locale context, e.g. a time zone with daylight savings time, we can construct a partial inverse LocalTime -> [ZonedDateTime]. (EDIT: See fromCalendarDateTimeAll.) Most of the time the result will be a singleton list, except when

  • the local clock jumps forward, resulting in illegal local time values: []
  • the local clock jumps backward, resulting in ambiguous values: (_:_:_)

Algorithm: Given a series of LocalTime, apply the partial inverse. If any value maps to [] then the assumption of locale must have been false. Abort. For any time values that are ambiguous, make a choice so that the final series [ZonedDateTime] maps to a non-descending list [Instant]. There may be more than one such choice, whence the algrorithm is a heuristic. However, the library should make the choice so that the round-trip [ZonedDateTime] -> [LocalTime] -> [ZonedDateTime] is the identity. To my knowledge that is something that timezone-series does not guarantee.

Yes, unlike resolve you can’t operate on isolated elements of the series. If you don’t want to go down that route with Hodatime, that’s fine with me.

In practice that is not up to the data scientist to decide. I have to work with whatever local time mapping the external source chose. Processing time series represented by LocalTime instead of something unambigous like UTCTime is asking for trouble and bugs that are hard to spot.

13

Can’t you then have something like

guessZdt :: [LocalTime] -> (LocalTime -> CalendarDateTime) -> Maybe [ZonedDateTime]
guessZdt lts f = mapM process lts
  where
    process :: LocalTime -> Maybe ZonedDateTime
    process lt = case fromCalendarDateTimeAll (f lt) of
      []       -> Nothing           -- 0 entries: Fail the whole process
      [zdt]    -> Just zdt
      (zdt:_)  -> Just zdt          -- 2 entries: Pick the first one

?

14

That is pretty much what timezone-series does. However, just picking an arbitrary (e.g. the first) entry from the list of possible ZonedDateTime is not good enough, at least when there is no guarantee on which possibility comes first. I suppose that

Data.Set.fromList (map toInstant (fromCalendarDateTimeAll zone cdt))

is not always a singleton, meaning that the choice matters for the semantics of the time series. Unless you can guarantee

(fromCalendarDateTimeAll  . toCalendarDateTime) z == (z : _)

your algorithm won’t round-trip.

What is the role of TimeZone in Hodatime versus time? In time,

(LocalTime, TimeZone) ~ ZonedTime ~ (UTCTime, TimeZone)

The type signature of fromCalendarDateTimeAll indicates that in Hodatime this is not the case. I guess that localZone returns information such as “Europe/Amsterdam, which could be UTC+1 or UTC+2 depending on DST”? The Hodatime ZonedDateTime has a hidden field of type TransitionInfo which the heuristic must guess.

(BTW, there seems to be no public function to extract the zdtTimeZone from a ZonedDateTime. Is that on purpose?)

15

Oh, sorry, the actual signature is fromCalendarDateTimeAll:: IsCalendarDateTime cal =>CalendarDateTimecal ->TimeZone -> [ZonedDateTime cal] And it will return 1 entry nearly always. 0 for missing times and two entries when a time happened twice, the first one always the first one that occurred.

You can ask the ZonedDateTime if it’s in DST. TransitionInfo is a private structure used by the time zones to figure out the Instant for any given ZonedDateTime. It wouldn’t make sense to make that public. We return the time zone ID but I see that there’s no obvious way to get the active Offset directly. There are certainly more changes needed that I’ll be doing in the coming days (e.g. fromInstant isn’t actually total: currently it would be possible to use it to construct invalid dates, like 1200 in Gregorian).

1 Like