Domain Driven Design, meet Dependent Types

This article aims to be the first post in a series exploring connection between Domain Driven Design and Dependent types as implemented in Idris. I plan to go through all the examples scattered across Eric Evan’s seminal book, revisiting them in the light of functional programming with dependent types. My intuition is that using DT languages will allow us to produce better and safer designs.

Let’s go first through some ceremonies in order to please the Gods of programming:

> module Cargo
> import Data.List
> %default total

We will go through the first example Eric Evans gives, p.17 of his book: A simple model describing booking of Cargo for Voyages. We have some very simple data structure describing cargos and voyages. A cargo is described by its identification string and a size.

> record Cargo where
>   constructor MkCargo
>   cargo_id : String
>   size : Int

And a Voyage is a list of cargos, a total capacity and a confirmation order¹

> record Voyage where
>   constructor MkVoyage
>   capacity : Int
>   orderConfirmation : Int
>   cargos : List Cargo

Given a voyage, it is simple matter to compute the total booked cargo size for this voyage:

> bookedCargoSize : Voyage -> Int
> bookedCargoSize = sum . map size . cargos

Then booking a Cargo for a Voyage checks the voyage can accomodate the given cargo’s size before adding it to its load:

> makeBooking : Cargo -> Voyage -> Voyage
> makeBooking cargo voyage =
>   if bookedCargoSize voyage + size cargo < capacity voyage
>   then record { cargos = cargo :: cargos voyage } voyage
>   else voyage

However, it is customary for shipping company to accept overbooking, say 10%. Our booking function then becomes:

> makeBooking' : Cargo -> Voyage -> Voyage
> makeBooking' cargo@(MkCargo _ size) voyage@(MkVoyage capacity orderConfirmation cargos) 
>              =  if cast (bookedCargoSize voyage + size) > 1.1 * cast capacity
>                    then  voyage
>                    else record { cargos = cargo :: cargos } voyage 

Obviously, this has the huge drawback of mixing different concerns: Updating the voyage with the cargo and computing the overbooking rule. What we want to do is to make this overbooking policy more explicit, say in a type:

> OverbookingPolicy : Type 
> OverbookingPolicy = Cargo -> Voyage -> Bool

Then our standard 10% overbooking policy is reified in its own function:

> tenPercentOverbooking : OverbookingPolicy
> tenPercentOverbooking cargo@(MkCargo _ size) voyage@(MkVoyage capacity orderConfirmation cargos) = 
>   cast (bookedCargoSize voyage + size) > 1.1 * cast capacity

and later on used to compute booking:

> makeBooking'' : Cargo -> Voyage -> OverbookingPolicy -> Voyage
> makeBooking'' cargo voyage isAllowed
>              =  if isAllowed cargo voyage
>                    then voyage
>                    else record { cargos = cargo :: cargos } voyage 

Simple and efficient.

However, this function is somewhat lacking with respect to how much information it provides in its type: We know nothing about the transformed voyage that it produces and in particular we don’t know if the OverbookingPolicy has been applied or not and if the cargo is part of the load. Having this information around in the type system would be handy to clients that need to take more decisions from this booking…

Enters dependent types: We will use a type to express the proposition that some Voyage contains some Cargo load which will be part of the outcome of the makeBooking function. This means we would like our makeBooking function to have the following signature:

makeBooking'' : (cargo : Cargo) -> Voyage 
              -> OverbookingPolicy 
              -> (voyage' : Voyage ** Dec (HasCargo cargo voyage'))

The return type is a dependent pair which associates an instance of Voyage, a value, with another value whose type depends on voyage'. Just like a standard pair this allows us to pack more information in our return type, namely the possibly updated voyage and a proof that cargo is part of voyage', or not.

In order to decide whether a voyage HasCargo or not, we need to be able to decide whethere two Cargos are equal or not which in Idris terms means implementing the interface DecEq for the Cargo type:

> mutual
>   implementation DecEq Cargo where
>     decEq (MkCargo cid _) (MkCargo cid _) = 
>       case decEq cid cid of 
>         (Yes prf)   => rewrite prf in Yes Refl
>         (No contra) => No $ contra . fst . cargoInj

The cargoInj is a utility function that allows us to relate a proof that the two cargo’s ids differ (contra) to actual Cargo inhabitants.²

>   private
>   cargoInj : (MkCargo cid s = MkCargo cid' s') -> (cid = cid', s = s')
>   cargoInj Refl = (Refl, Refl)

We can now define HasCargo type:

> data HasCargo : (cargo : Cargo) -> (voyage : Voyage) -> Type where
>   CargoConfirmed : { auto prf : Elem cargo cargos } 
                   -> HasCargo cargo (MkVoyage cap order cargos)

HasCargo’s only constructor, CargoConfirmed, given a proof that cargo is an element of voyage’s cargos, yields a proof that cargo is confirmed to be part of voyage. This is a convoluted way to assert the fact a cargo is inside the list of cargos carried by a voyage. Note that we expect the compiler to be able to provide the proof autoatically from the environment and so it is left implicit.

To be useful in our makeBooking function, we need to equip this type with a decision procedure, e.g. a function that produces a DecEq (HasCargo ...) instance given some cargo and some voyage:

> mutual
>   hasCargo : (cargo : Cargo) -> (voyage : Voyage) -> Dec (HasCargo cargo voyage)
>   hasCargo cargo (MkVoyage capacity orderConfirmation []) = No voyageIsEmpty

The case where the list of cargos of a voyage is empty is easy: Simply return a No with a contradiction voyageIsEmpty (see later). The non-empty case is a little bit trickier:

>   hasCargo cargo (MkVoyage capacity orderConfirmation cargos) = 

First we pattern-match to check whether or not the cargo is in the list which gives us a DecEq (Elem cargo cargos) instance:

>     case isElem cargo cargos of

In the Yes case, we simply produce CargoConfirmed and the compiler can use the prf proof of membership in scope to satisfy the requirements of the constructor:

>       (Yes prf)   => Yes CargoConfirmed

In the No case, we need to transform our proof by contradiction an element is not present in a proof by contradiction HasCargo does not hold, which means (again) composing functions to extract the proof from a CargoConfirmed instance and pass it to contra:

>       (No contra) => No (contra . cargoConfirmed)

This code makes use of the following utility functions as contradictions:

> 
>   voyageIsEmpty : HasCargo cargo (MkVoyage capacity orderConfirmation []) 
>                 -> Void
>   voyageIsEmpty CargoConfirmed impossible
> 
>   cargoConfirmed : HasCargo cargo (MkVoyage capacity orderConfirmation cargos)
>                  -> Elem cargo cargos
>   cargoConfirmed (CargoConfirmed {prf}) = prf

We are now fully armed to define makeBooking''' function which is just our makeBooking'' function augmented with an actual proof telling us whether or not the cargo has been actually confirmed.

> makeBooking''' : (cargo : Cargo) -> Voyage 
>                -> OverbookingPolicy
>                -> (voyage' : Voyage ** Dec (HasCargo cargo voyage'))
> makeBooking''' cargo voyage@(MkVoyage capacity orderConfirmation cargos) isAllowed = 
>   let voyage' = if isAllowed cargo voyage
>                   then MkVoyage capacity orderConfirmation (cargo :: cargos)
>                   else voyage
>   in (voyage' ** hasCargo cargo voyage') 

In the original function (or method) defined in the book, makeBooking returned an integer which was supposed to be booking confirmation order, or -1 if the booking could not be confirmed. It seems to me the above formulation improves over this simple but potentially obscure coding of return type, explicitly embodying the success or failure to add the cargo to the voyage in the return type while concurrently updating the voyage. What I found really interesting is that while we are not only improving the cohesion/coupling through the separation of concerns OverbookingPolicy yields, we are also opening the function to other use thanks to the more precise return type.

Dependent types (or even non-obviously-dependent-yet-sophisticated type systems like Haskell’s or OCaml’s) really allows (or forces) us to reason in two stages: Things we can reason about at compile time and things we can reason about at run-time, with the added value of being able to express the two using the same expressions. I suspect these capabilities could be useful to provide more robust and expressive designs for real-world problems, and not only as a tool for automated theorem proving, and this is what I intend to explore in the next installments of this series.

Thanks to Rui Carvalho for the feedback and to Crafting Software Meetup to give me the incentive to explore these topics