GADTs in the wild

[Manuel M T Chakravarty]

Most academic papers do use the eval example, but it is a practical example. This use of GADTs is nice for embedded languages. For example, Accelerate uses a supercharged version of it to catch as many errors as possible during Haskell host program compile-time (as opposed to Accelerate compile time, which is Haskell runtime).

Manuel


Simon Peyton-Jones <simonpj at microsoft.com>:
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120815/65c7bf58/attachment.htm>