3

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?

  • 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. – Telastyn Sep 28 '14 at 17:49
  • 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. ☺ – Michael Le Barbier Grünewald Sep 28 '14 at 19:14
2

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.