Join Newsletter

Getting Data Structures Right with GADTs and nested types

YOW! Lambda Jam 2013

Learn about GADTs and nested data types, and how you can use them to encode structural invariants in your Haskell types. You’ll also gain some insight into the inner workings of efficient functional data structures.

In the talk, I’ll show a B-tree, using a GADT to maintain balance. We’ll see that types not only guard against errors, but help us find the right implementation.

Matthew Brecknell

Proof Engineer



Matthew began programming in C++, but became curious about functional programming when he realised that template metaprogramming was probably a rudimentary form of FP. Via Haskell, he became interested in type theory, and then via Coq, in theorem proving. He now has his dream job working with some of the world leaders in formal verification, where he uses Isabelle/HOL to prove things about the C implementation of the seL4 microkernel.