ISO Dates
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.
We could do something similar with Coq's notations.
ISO Dates
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.
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.