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

[Oliver Charles]

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 <nicola.gigante at gmail.com>
wrote:

> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150330/bb5ad87d/attachment.html>