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
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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users