[Haskell-cafe] Enforcing data structures invariant in the type system

Nicola Gigante nicola.gigante at gmail.com
Mon Mar 30 17:00:39 UTC 2015

Hi all.

I’m very interested in what can be done with Haskell’s type system regarding
the enforcing of algorithms and data structures invariants.

For example, I remember I saw a paper about an implementation of a red-black
tree in Haskell where the types guaranteed the invariant about the alternation of
rad and black nodes.

I would like to learn those techniques, in particular the use of language features that
enable this kind of things and then how to do them in practice. 
In the past tried hacking something with GADTs and Data Kinds but I've always 
got stuck with GHC errors that I could not understand, so I think I’m missing something.

Where could I start from? Are there simple walk-through examples and/or fundational
material? For example is it possible to write a sorting function that guarantees in the types 
that the output is sorted? I don’t need this specific example but you got the point.

Thank you very much,

More information about the Haskell-Cafe mailing list