GADTs in the wild

Michael Snoyman michael at snoyman.com
Tue Aug 14 13:44:38 CEST 2012


On Tue, Aug 14, 2012 at 2:32 PM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

>  Friends****
>
>
> I’m giving a series of five lectures at the Laser Summer School<http://laser.inf.ethz.ch/2012/>(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
>
>
Hi Simon,

In the webcast I gave last week, I used a dumbed-down version of how we do
safe queries in Persistent. The example is on slides 20-22 of [1].
Persistent works mostly the same way (and was inspired in this usage by
groundhog[2]). If you want a more thorough explanation of how Persistent
uses GADTs, let me know.

An example that came up at work (with Yitzchak Gale, he probably has more
details) was essentially two different types of documents that shared a lot
of the same kinds of elements (tables, lists, paragraphs, etc) but some
elements only appeared in one of the document types. We needed to render to
(for sake of argument) two different XML formats, and wanted to be certain
we didn't put in elements from type 1 in type 2. The solution looked
something like this (using data kinds and GADTs):

data DocType = Doc1 | Doc2

data Element (doctype :: DocType) where
    Paragraph :: Text -> Element doctype
    Table :: [Element doctype] -> Element doctype
    ...
    BulletList :: [[Element doctype]] -> Element Doc1

renderDoc1 :: Element Doc1 -> XML
renderDoc2 :: Element Doc2 -> XML

Michael

[1]
https://docs.google.com/presentation/d/1c6pkskue6WbTlONFTpFhYqzSlQe_sxO7LfP5SW7InVE/edit
[2] http://hackage.haskell.org/package/groundhog
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120814/72f4330c/attachment.htm>


More information about the Glasgow-haskell-users mailing list