GADTs in the wild

[Gábor Lehel]

Lennart Augustsson has a really interesting example of using GADTs and
the Maybe monad to validate an untyped AST into a typed,
(mostly-)correct-by-construction AST here:

http://augustss.blogspot.com/2009/06/more-llvm-recently-someone-asked-me-on.html

This was one of my first exposures to GADTs and it set my mind racing.
I wrote a small compiler for simple scalar/vector/matrix arithmetic
expressions with variables as my first nontrivial Haskell project, and
it was heavily inspired by Lennart's article. (I can put it up online
if anyone's interested, but I'm not relishing the thought of updating
LLVM on my system and the various packages and possibly the code to
make it all work again.)

On Tue, Aug 14, 2012 at 1:32 PM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> Friends
>
>
> I’m giving a series of five lectures at the Laser Summer School (2-8 Sept),
> on “Adventures with types in Haskell”.  My plan is:
>
> 1.   Type classes
>
> 2.   Type families [examples including Repa type tags]
>
> 3.   GADTs
>
> 4.   Kind polymorphism
>
> 5.   System FC and deferred type errors
>
>
>
> This message is to invite you to send me your favourite example of using a
> GADT to get the job done.  Ideally I’d like to use examples that are (a)
> realistic, drawn from practice (b) compelling and (c) easy to present
> without a lot of background.  Most academic papers only have rather limited
> examples, usually eval :: Term t -> t, but I know that GADTs are widely used
> in practice.
>
>
>
> Any ideas from your experience, satisfying (a-c)?  If so, and you can spare
> the time, do send me a short write-up. Copy the list, so that we can all
> benefit.
>
>
>
> Many thanks
>
>
> Simon
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>



-- 
Your ship was destroyed in a monadic eruption.