
Now that the new typechecking awesomeness has been committed to GHC HEAD, theoretically all of the things one can express with FunctionalDependencies (bar overlap) should now be expressible with TypeFamilies as well. This got me to thinking how this might actually be done. Here's an example of a previously-inexpressible class I might want to translate, which functional dependencies allow to be expressed fairly neatly: class TwoPhase frozen thawed | frozen -> thawed, thawed -> frozen where thaw :: frozen -> thawed freeze :: thawed -> frozen (Vaguely inspired by things I saw in the Vector API; it's an abstraction for types which have the same internal representation but can present either a pure, functional interface or a mutable, monadic one and be converted between the two. For the purposes of this message this is just an example.) As far as I can tell, the straightforward translation of this to type families and equality constraints would be like this: class (Frozen (Thawed a) ~ a) => Immutable a where type Thawed a :: * thaw :: a -> Thawed a freeze :: Thawed a -> a type family Frozen a :: * But I don't think this looks too nice. It loses the nice symmetry of the FD version. (You could take both type families outside the class to make it a bit less asymmetric, among other things, but I don't see a way to avoid the fact that you need to distinguish one end of the mapping and define the other in terms of it.) What I would *want* to write is this: class (Mutable (Thawed a), Frozen (Thawed a) ~ a) => Immutable a where type Thawed a :: * thaw :: a -> Thawed a class (Immutable (Frozen a), Thawed (Frozen a) ~ a) => Mutable a where type Frozen a :: * freeze :: a -> Frozen a This looks considerably nicer, but it's not valid -- I get a cycle in class declarations via superclasses error, on the one hand, and (if I remove that) an infinite loop in the typechecker (context reduction stack overflow) on the other (FlexibleContexts being a prerequisite for most of the interesting things you can do with TypeFamilies). So what should one, theoretically, do here? Is there a way to express this using TypeFamilies which preserves both the semantics and the symmetry of the FDs version, and is also valid? Or should one just go ahead and use the FDs because, in this case, they're simply better suited? *Or* should one just suck it up and go with the ugly TypeFamilies version because TypeFamilies are The Future*? * The abbreviation TF not being a coincidence. ~g -- Work is punishment for failing to procrastinate effectively.