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