Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Totally Typed Domain

martinsson
June 07, 2018
55

Totally Typed Domain

Where Dependent types meets domain driven design

Using the power of types to encode domain constraints into code.

As presented at ITAKE

martinsson

June 07, 2018
Tweet

Transcript

  1. Why? Type driven development and Dependent types look cool! Model

    the domain closely ! Make impossible states impossible ! Some guarantees
  2. Unit tests It compiles so it's obviously correct right? YES

    Unit tests implemented in the type system
  3. Ok fancy types, but all inputs are string Validate user

    input => Strong typing Strong typing => enforces validation A type can be a permission to do something
  4. Tic Tac Toe placeMark : (freePos: List Pos) -> Pos->

    List Pos vs
 
 placeMark : (freePos: Vect (S n) Pos) // available positions, (S n) means n+1 
 -> (p: Pos) // position to be marked
 -> (Elem p freePos) // proof that position p is in freePos
 -> Vect n Pos // remaining positions, 1 less than input
  5. Conclusions ! Types are proofs ! Compilers ~ tests !

    Small types ! Qualified types <=> encoded knowledge ! Feedback ! Compilers will evolve