[Haskell-cafe] Estonia and GADT

[David Roundy]

On Sat, Oct 15, 2005 at 10:46:11AM +0400, Bulat Ziganshin wrote:
>   2) they all say that GADT is great, but i personally don't "feel"
>   GADTs. can anyone write a paper about it for beginners like me,
>   or may be just collect examples of using GADT in real programs?

If you want a somewhat brain-twisting example, you could check out

darcs get http://abridgegame.org/darcs-patch-theory

which uses GADTs and phantom types to verify the correctness of patch
commutation code.  It's not a simple example by any stretch of the
imagination, but I believe it's practical, allowing us to catch many
very-easy-to-introduce bugs.  You'd want to start reading the code with
Patchy, and then maybe move to PrimPatch.  Note that we pretty *only* use
GADTs with phantom and existential types.  The plan is to move all of darcs
code over to use this scheme (perhaps with cpp macros to allow darcs to
compile on older versions of ghc).

As we've worked on this code, it seems like the solution to almost every
problem we've run into has been "define a new GADT".
-- 
David Roundy
http://www.darcs.net