GADTs in the wild

[Edward Kmett]

We use a form of stream transducer here at Capital IQ that uses GADTs, kind
polymorphism and data kinds:

data SF k a b
  = Emit b (SF k a b)
  | Receive (k a (SF k a b))

data Fork :: (*,*) -> * -> * where
  L :: (a -> c) -> Fork '(a, b) c
  R :: (b -> c) -> Fork '(a, b) c

type Pipe = SF (->)
type Tee a b = SF Fork '(a, b)

instance Category (SF (->)) where
  id = arr id
  Emit a as . sf = Emit a (as . sf)
  Receive f . Emit b bs = f b . bs
  sf . Receive g = Receive (\a -> sf . g a)

arr :: (a -> b) -> Pipe a b
arr f = z where
  loop a = Emit (f a) z
  z = Receive loop

repeat :: b -> SF k a b
repeat b = Emit b z
  where z = repeat b

filter :: (a -> Bool) -> Pipe a a
filter p = z
  where loop a | p a = Emit a z
               | otherwise = z
        z = Receive loop

You can extend the model to support non-deterministic read from whichever
input is available with

data NonDetFork :: (*,*) -> * -> * where
  NDL :: (a -> c) -> NonDetFork '(a, b) c
  NDR :: (b -> c) -> NonDetFork '(a, b) c
  NDB :: (a -> b) -> (b -> c) -> NonDetFork '(a, b) c

These could admittedly be implemented using a more traditional GADT without
poly/data kinds, by just using (a,b) instead of '(a,b), though.

-Edward Kmett

On Tue, Aug 14, 2012 at 7:32 AM, 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120814/9a8cf382/attachment-0001.htm>