You're in the right ballpark that's for sure - and your experience with
hard-to-decode error messages is not a new one either! Haskell is somewhat
"experiemental" in this domain, as its only now starting to learn the
features necessary to do what you want to do.
I think some of the best work to learn the latest techniques is described
here: https://github.com/jstolarek/dep-typed-wbl-heaps-hs
-- ocharles
On Mon, Mar 30, 2015 at 6:00 PM, 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe