ISO Dates

Well you don’t really need dependent types to model a wellformed month,

 data Month = January
            | February
            | March
            ...
            | November
            | December

It becomes slightly more painful with the day and year, since those are rather larger. Indeed, the legal representation of a day of the month depends on month. Let’s define a function

numDays : Month -> Nat
numDays January = 31
...
numDays December = 31

Now, what we want to say is that Day is a type which takes a month and returns a new type. So

Day : Month -> Type
Day m = ...

where ... somehow says “I’m a number between 0 and numDays m“. We can represent this with a type called Fin

data Fin (n : Nat) : Type where
  FinZ : Fin n
  FinS : Fin m -> m + 1 < n -> Fin (m + 1)

In other words, Fin is all the numbers from 0 to n, excluding n.

So now we can say

Day : Month -> Type
Day m = Fin (numDays m)

As for years, those are independent of both the month and the day, leaving us with

data Date : Type where
  mkDate : (year : Nat)(month : Month)(day : Day month) -> Date

If we wanted to be precise, we could have day depend on year to take into account leap years.

If we where working in Agda and had mix-fix syntax. To get literals all we’d have to do is say

[_-_-_] : Nat -> (m : Month) -> Day m -> Date
[_-_-_] = mkDate

We could do something similar with Coq’s notations.

As a compileable mini example,

open import Data.Nat
open import Data.Fin

data Month : Set where
  January : Month
  February : Month

numDays : Month -> ℕ
numDays January  = 31
numDays February = 28

Day : Month → Set
Day m = Fin (numDays m)

record Date : Set where
  constructor mkDate
  field
    month : Month
    day   : Day month

_/_ : (m : Month)(n : ℕ){p : Data.Nat._≤_ (suc n) (numDays m)} → Date
_/_ m n {p} = mkDate m (inject≤ (fromℕ n) p)

Quotients and Building Up Times

Now another obvious way to model dates and times is to have notions like an absolute time and other notions like a duration. Then we can combine these and produce other time stamps.

So for example we might want to say “5 seconds before 1 minute after T”. The issue comes when comparing times like this for equality. We really don’t care about the precise internal structure of how we can to a point in time, just that we got there. So we have to be careful not to let our data have any structure that might distinguish to otherwise equivalent values.

This is a really subtle and thorny issue as it turns out. There isn’t really a good way to address this in Idris or Coq since they lack quotient types.