Gave a Talk on Types in Programming

As announced, I gave a talk last Tuesday at Mama, Zagreb on the role of types in programming as part of the Lamda Zagreb Meetup group. I enjoyed giving the talk and discussing types and programming in general after the talk over a beer. Later on we had a follow-up discussion in the comments section on the event page, which made me happy to see what can be done in Haskell.

The talk was on types and how they can help us write programs with fewer bugs. I had examples mostly in Idris, but also some in Haskell and Scala. If you are interested, slides from the talk (versions in Croatian and English) along with code examples are available in a Git repository.

[Me explaining a state machine encoded at the type level. The photo is courtesy of Ivica Dimjašević.](state-machine-in-idris.jpg “Me explaining a state machine encoded at the type level. The photo is courtesy of Ivica Dimjašević”.){ width=100% }

To illustrate how useful and fun types can be, I had several examples with dependent types. First, I showed how types can be useful in interactive development where I gave a signature of a zip function that zips two lists (vectors) together and Idris implemented the whole function for me based on the type signature only. The audience loved it. In the follow-up discussion I provided a few variants of that example and all are available in the Git repository.

Then I moved onto the next example with dependent types: a state machine that is encoded at the type level. If you try to make an illegal state transition in such a machine, your compiler will give you an error. Here is the state machine and a few programs that make transitions in it:

data Grade' = A | B | C | D | E

data EssayS = Unassigned
            | Assigned
            | Writing
            | Reviewing
            | Done

data EssayCmd : Type -> EssayS -> EssayS -> Type where
  Assign   : EssayCmd () Unassigned Assigned
  Start    : EssayCmd () Assigned Writing
  Consult  : EssayCmd () state state
  Review   : EssayCmd () Writing Reviewing
  SendBack : EssayCmd () Reviewing Writing
  Grade    : Grade' -> EssayCmd Grade' Reviewing Done
  
  (>>=)    : EssayCmd a state1 state2 ->
             (a -> EssayCmd b state2 state3) ->
             EssayCmd b state1 state3

essayProg1 : EssayCmd () Unassigned Assigned
essayProg1 = do
  Consult
  Assign

essayProg2 : EssayCmd () Writing Writing
essayProg2 = Review >>= const SendBack

essayProg3 : EssayCmd Grade' Reviewing Done
essayProg3 = do
  SendBack
  Review
  Grade C

As you can see, the example is about a state an essay can be in and how an essay can transition from one state to the next state.

There were a few Haskellers in the audience and they hinted that this could also be implemented in Haskell, albeit with a not as nice syntax. To that I said it’d be great if someone implemented the state machine in Haskell. Tomislav Grospić accepted the challenge and implemented it:

{-# LANGUAGE GADTs, TypeInType, TypeFamilies, TypeOperators #-}
{-# LANGUAGE UndecidableInstances, PolyKinds #-}

module SampleStateMachine () where

import Data.Kind (Type)

data Grade' = A | B | C | D | E

data EssayS = Unassigned
            | Assigned
            | Writing
            | Reviewing
            | Done

data EssayCmd :: Type -> EssayS -> EssayS -> Type where
  Assign   :: EssayCmd () Unassigned Assigned
  Start    :: EssayCmd () Assigned Writing
  Consult  :: EssayCmd () state state
  Review   :: EssayCmd () Writing Reviewing
  SendBack :: EssayCmd () Reviewing Writing
  Grade    :: Grade' -> EssayCmd Grade' Reviewing Done

type family (>>=) (x :: EssayCmd a state1 state2)
  (y :: ay -> EssayCmd b state2 state3) :: EssayCmd b state1 state3

type family Const (x :: a) :: b -> a

type family EssayProg1 :: EssayCmd () Unassigned Assigned where
  EssayProg1 = Consult >>= Const Assign

type family EssayProg2 :: EssayCmd () Writing Writing where
  EssayProg2 = Review >>= Const SendBack

type family EssayProg3 :: EssayCmd Grade' Reviewing Done where
  EssayProg3 = SendBack >>= Const Review >>= Const Grade C

type family EssayTy (x :: EssayCmd a s1 s2) :: Type where
  EssayTy (Grade x) = (String, Int)
  EssayTy Consult   = ()
  EssayTy _         = String

r1 :: EssayTy Start
r1 = "Essay is started"

r2 :: EssayTy (Grade A)
r2 = ("Essay is done", 1)

r3 :: EssayTy Consult
r3 = ()

He used several GHC extensions that I am yet to learn — notably, type families — and I’m thrilled to see this can be done in Haskell!

I concluded with refinement types, although I didn’t spend much time talking about them.