<div dir="ltr">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.<div><br></div><div>I think some of the best work to learn the latest techniques is described here: <a href="https://github.com/jstolarek/dep-typed-wbl-heaps-hs">https://github.com/jstolarek/dep-typed-wbl-heaps-hs</a></div><div><br></div><div>-- ocharles</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Mar 30, 2015 at 6:00 PM, Nicola Gigante <span dir="ltr"><<a href="mailto:nicola.gigante@gmail.com" target="_blank">nicola.gigante@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all.<br>
<br>
I’m very interested in what can be done with Haskell’s type system regarding<br>
the enforcing of algorithms and data structures invariants.<br>
<br>
For example, I remember I saw a paper about an implementation of a red-black<br>
tree in Haskell where the types guaranteed the invariant about the alternation of<br>
rad and black nodes.<br>
<br>
I would like to learn those techniques, in particular the use of language features that<br>
enable this kind of things and then how to do them in practice.<br>
In the past tried hacking something with GADTs and Data Kinds but I've always<br>
got stuck with GHC errors that I could not understand, so I think I’m missing something.<br>
<br>
Where could I start from? Are there simple walk-through examples and/or fundational<br>
material? For example is it possible to write a sorting function that guarantees in the types<br>
that the output is sorted? I don’t need this specific example but you got the point.<br>
<br>
Thank you very much,<br>
Nicola<br>
<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div>