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

[Nicola Gigante]

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,
Nicola