A Dependently Typed Date

Posted on April 19, 2017

This article is the second installment of a planned series of articles exploring connection between Domain Driven Design and Dependent types as implemented in Idris, revisiting examples and patterns from Eric Evan’s book.

I was planning to work on the Specification pattern from chapter 9, pp.224 seq. of the book which is something that fits nicely, along with other patterns from this chapter, in a strongly typed purely functional framework. But I was sent off-track and ended up shaving a yak, or more precisely defining a Date type along with an addDays function, because this is something that was needed to define a proper DelinquentInvoice specification. This was a challenging exercise for me to undertake and I learnt a things or two in the process that might be worthwhile to share.

Code

So let’s start defining our module. We will require all our functions to be total and export everything as public (probably something we want to restrict later on…).

> module Date 
> 
> import Decidable.Order
> 
> %default total
> %access public export

Our first important type will be the Month which is straightforwardly implemented as an enumeration of months’ names1.

> data Month : Type where
>   January    : Month
>   February   : Month
>   March      : Month
>   April      : Month
>   May        : Month
>   June       : Month
>   July       : Month
>   August     : Month
>   September  : Month
>   October    : Month
>   November   : Month
>   December   : Month

There is an Enum typeclass/interface in Idris but it requires quite a lot of functions to be defined, so let’s do something simpler and define only a toNat function which will be handy to compare months:

> toNat : Month -> Nat
> toNat January    = 1
> toNat February   = 2
> toNat March      = 3
> toNat April      = 4
> toNat May        = 5
> toNat June       = 6
> toNat July       = 7
> toNat August     = 8
> toNat September  = 9
> toNat October    = 10
> toNat November   = 11
> toNat December   = 12

It is then easy to compare months, providing implementations for Eq and Ord interfaces:

> implementation Eq Month where
>   m1 == m2 = toNat m1 == toNat m2
> 
> implementation Ord Month where
>   compare m1  m2 = compare (toNat m1) (toNat m2)

Now, let’s tackle Years. Easy enough, we will stick to simply representing years as a natural number, which of course will prevent us at this stage to represent dates B.C. idris > Year : Type > Year = Nat

An important thing to know about a year is whether or not it is a leap year: This will be critical to know what’s the duration of the year and the number of days of February. There is a simple algorithm for that: A year which is dividible by 4 is a leap year, except when it is dividible by 100 and not dividible by 400 (1900 is not a leap year but 2000 is).

> isLeapYear : Year -> Bool
> isLeapYear y = check4 && check100 || check400
>   where

Because we are working with Nats (underlying representation for years) we need to use some special functions to compute modulus, namely modNatNZ which requires us to provide a proof the divisor is not 0.

>     check4 : Bool
>     check4 = modNatNZ y 4 SIsNotZ == 0
> 
>     check100 : Bool
>     check100 = modNatNZ y 100 SIsNotZ /= 0
> 
>     check400 : Bool
>     check400 = modNatNZ y 400 SIsNotZ == 0

Equipped with this predicate we can compute the duration of a month:

> monthDuration : Month -> Year -> (days: Nat ** LTE 1 days) 

Note the return type of monthDuration is a dependent pair associating the number of days of the month (a Nat) with a proof this number of days is always greater than 1. This will become important later on when we want to add days to dates…

Defining the function is a simple matter of case analysis over the constructors of Month:

> monthDuration January _      = (31 ** LTESucc LTEZero)
> monthDuration February year  = if isLeapYear year 
>                                then (29  ** LTESucc LTEZero)
>                                else (28 ** LTESucc LTEZero)
> monthDuration March _        = (31 ** LTESucc LTEZero)
> monthDuration April _        = (30 ** LTESucc LTEZero)
> monthDuration May _          = (31 ** LTESucc LTEZero)
> monthDuration June _         = (30 ** LTESucc LTEZero)
> monthDuration July _         = (31 ** LTESucc LTEZero)
> monthDuration August _       = (31 ** LTESucc LTEZero)
> monthDuration September _    = (30 ** LTESucc LTEZero)
> monthDuration October _      = (31 ** LTESucc LTEZero)
> monthDuration November _     = (30 ** LTESucc LTEZero)
> monthDuration December _     = (31 ** LTESucc LTEZero)

Because having to pattern match on pair is not very handy, let’s provide some helpers functions to get only the relevant part of the pair:

> daysInMonth : Month -> Year -> Nat
> daysInMonth month year with (monthDuration month year) 
>   | (days ** _) = days
> 
> aMonthHasOneDay : (month : Month) -> (year : Year) -> LTE 1 (daysInMonth month year)
> aMonthHasOneDay month year with (monthDuration month year) 
>   | (_ ** prf) = prf

Had we defined a proper Enum implementation, we would be able to use pred and succ to navigate between months… But we only need at the moment to compute nextMonth which is definitely simple:

> nextMonth : Month -> Month
> nextMonth January   = February
> nextMonth February  = March    
> nextMonth March     = April    
> nextMonth April     = May      
> nextMonth May       = June     
> nextMonth June      = July     
> nextMonth July      = August   
> nextMonth August    = September
> nextMonth September = October  
> nextMonth October   = November 
> nextMonth November  = December 
> nextMonth December  = January

We are at last equipped to define a Date type that will prevent us to define invalid dates:

> data Date : Type where
>   MkDate : (year  : Year) -> (month : Month ) -> (day : Nat) 

So a Date is built from a Year, a Month and Nat for the day, with the additional constraints that day should be between 1 and the length of the month, a property which is easily defined as implicit dependent types:

>          -> { auto dayFitInMonth : LTE day (daysInMonth month year) } 
>          -> { auto dayGreaterThanOne : LTE 1 day } 

To build a Date, one will then need to provide proofs the day respects the given constraints.

>          -> Date

Here are some examples of buildiing valid and invalid dates at the REPL:

Let’s try to build a date with 0 as day number:

λΠ> :let d = MkDate 2017 February 0
(input):1:17:When checking argument gtOne to constructor Date.MkDate:
        Can't find a value of type 
                LTE 1 0

And what about the 29th of February, 2017 ?

λΠ> :let d = MkDate 2017 February 29
(input):1:17:When checking argument dayFitInMonth to constructor Date.MkDate:
        Can't find a value of type 
                LTE 29 28

However, 29th of February, 2016 is fine:

λΠ> :let d = MkDate 2016 February 29
defined
λΠ> d
MkDate 2016 February 29 : Date

We can now tackle the problem which triggered that development: Adding some days to a Date to compute a new Date… The general definition follows the classical inductive principle over the number of days in order to guarantee totality of the function.

> mutual   
>   addDays : Date -> Nat -> Date
>   addDays d Z     = d
>   addDays d (S k) = addDays (addOneDay d) k

The grunt of the job is delegated to the addOneDay function which is the most interesting one:

>   addOneDay : Date -> Date
>   addOneDay (MkDate year month day) = 

We do a case analysis to using the order function from the Ordered interface that, given a total relation (LTE in our case) and two elements states which one is greater than other, providing a proof packed in an Either union:

>     case order {to=LTE} (S day) (daysInMonth month year) of

The Left case is easy. Simply increment the number of days by one while keeping everything the same. The dayFitInMonth property is satisfied by the (anonymous) value provided in the Either:

>       Left _  => 
>         MkDate year month (S day)

The Right case (meaning the day is the last day of the month) requires another case analysis on the month:

>       Right _ => 
>             case month of 

If we are at the end of the year, increment year and set the day to 1st of January:

>                     December => MkDate (year + 1) January 1

Otherwise, move to first day of next month. The firstDayOfMonth variables provides the necessary proof that 1 is indeed within the limits of the allowed number of days for next month. This proof is provided by the monthDuration function and allows us to build the required Date in a typesafe way.

>                     _        => let firstDayOfMonth = aMonthHasOneDay (nextMonth month) year
>                                 in MkDate year (nextMonth month) 1

Discussion

It took me a while and help from Stack Overflow and the #idris channel at irc.freenode.net to figure out how to implement addDays. One dead end was trying to use a Fin n as a representation for days, believing it would already provide some guarantees that would simplify definition of other types and functions. It proved a mistake for at least 2 reasons:

Moving to representing days as a Nat with explicit constraints in the constructor’s type for Date made everything simpler.

I also struggled a lot with making addDays total:

The last difficult piece, and something that remains a little bit puzzling to me, was the need for a proof that LTE 1 (monthDuration $ nextMonth month) that arose from the last branch of the cases. Apparently, an explicit proof is needed because Idris does not reduce the expression appearing in types unless the expression is used in a with xxx | lhs = rhs view or is part of the definition of some value2. This bit me also when defining daysInMonth and aMonthHasOneDay.

Something that I tried to do but could not manage to complete quickly is defining the LeapYear year type to expose the leapyearness as a proposition that could then be carried around in types and would remove the need for explicit if/then/else. As a general rule of thumb and a piece of advice that was given to me on SO, it is a good idea to use functions and types that provide richer information than Bool or Maybe a: You usually want and need a proof that some property holds or does not hold to build richer and more accurate types.


  1. Note we are defining a simple version of dates within the Gregorian calendar. For a lot of ugly and painful details on how to properly handle dates, one can have a look at this Ocaml library FAQ

  2. Idris is strict by default: Arguments to functions are evaluated before the right-hand side and I assume this also applies to let x = y in z blocks which are traditionally translated to (\ x -> z) y.