Gave a Talk on Types in Programming

Posted on February 12, 2018 by Marko Dimjašević
Courtesy of Ivica Dimjašević
Courtesy of Ivica Dimjašević

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:

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:

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.