[Haskell-cafe] translating bidirectional fundeps to TFs

[Gábor Lehel]

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.