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