[Haskell-cafe] Fun with type functions

[Ryan Ingram]

My work on lightweight session types (modeled after this year's ICFP
paper on the same subject) used type and data families extensively for
an elegant way of connecting communicating coroutines:

Empty types are used for sessions:

> data Eps  -- empty session
> data a :?: s -- read an "a" followed by session "s"
> data a :!: s -- write an "a" followed by session "s"
> -- etc.

These have kind *, which makes them easy to use in other type-level
code; my first formulation had the session types as functors directly,
but that led to needing kind signatures elsewhere and made working
with these types much more difficult..

Type families are used to represent the dual of a session; that is, a
session that reads an Int can connect with a session that writes an
Int.

> type family Dual s
> type instance Dual Eps = Eps
> type instance Dual (a :?: s) = a :!: Dual s
> type instance Dual (a :!: s) = a :?: Dual s
> -- etc.

Then data families give structure to the session:

> data family Rep s a
> newtype instance Rep Eps a = Done a
> data instance Rep (x :!: s) a = Send x (Rep s a)
> newtype instance Rep (x :?: s) a = Receive (x -> Rep s a)
> -- etc.

Rep s converts a sessions (kind *) into a functor (kind * -> *).  It
also allows easy experimentation with alternate formulations of the
problem that potentially have different kinds.

Finally, a typeclass allows interpretation of these types, connecting
two sessions together to run as coroutines:

> class Coroutine s where
>    connect :: (Dual s ~ c, Dual c ~ s) => Rep s a -> Rep c b -> (a,b)
>
> instance Coroutine Eps where
>    connect (Done a) (Done b) = (a,b)
> instance Coroutine s => Coroutine (x :!: s) where
>    connect (Send x s) (Receive k) = connect s (k x)
> instance Coroutine s => Coroutine (x :?: s) where
>    connect (Receive k) (Send x c) = connect (k x) c

The proof that two routines can safely connect is done entirely at
compile time; the connection routine just takes care of routing data
between the two processes.

  -- ryan

On Thu, Nov 27, 2008 at 1:29 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> Friends
>
> GHC has embodied data type families since 6.8, and now type synonym families (aka type functions) in 6.10.  However, apart from our initial papers there isn't much published material about how to *use* type families.  But that hasn't stopped you: quite a few people are using them already, and of course there is a rich seam of work on using functional dependencies to express type-level computation.
>
> Ken Shan and Oleg Kiselyov and I are collaborating to write a paper for an upcoming workshop, under the general rubric of "Fun with type functions" (in homage to Thomas Hallgren's paper "Fun with functional dependencies" and Ralf Hinze's paper "Fun with phantom types").
>
> So this message is to ask you:
>
>        can you tell us about the most persuasive, fun application
>        you've encountered, for type families or functional dependencies?
>
> Simple is good.  It doesn't have to be elaborate: just something that does something useful you could not have done otherwise.  Pointers to email threads are fine.  Don't assume we already know about them (even if we participated in the thread :-)  Part of what we're interested in is that *you* found the example compelling.
>
> Many thanks
>
> Simon, Ken, Oleg
>
> PS: I'm broadcasting this message to GHC-users and Haskell-cafe, but to avoid deluging ghc-users, please reply just to us and Haskell cafe.  (Interested ghc-users can follow the threads there from the archives if they want.)
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>