Is there a way to define a consistent date in a dependent type language?

Question

I am looking for an example (if exists at all) of a definition of a date in a programming language (Idris, Coq, etc) that features dependent types where such definition is consistent and type safe by which I mean that invalid date expression or literal would give a compile time error. If the complete definition isn't possible what would be the best one you can think of?

• Telastyn: The simplest would be to represent the "dependent" part of the type as ticks (or days if you just want dates) since some epoch. It would then be up to the actual code to convert that into month day year, etc.
• Michaël Le Barbier: It will not help you much, but I cannot refrain to quote the FAQ of the OCaml calendar library. If you read it carefully, you will not be able any more to describe what a "valid date" is. ☺

Answer 1

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 -> N
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 : N){p : Data.Nat._≤_ (suc n) (numDays m)} → Date
_/_ m n {p} = mkDate m (inject≤ (fromN 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.