translating bidirectional fundeps to TFs
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.
On Friday 17 September 2010 4:04:26 pm Gábor Lehel wrote:
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*?
What about: class (Thawed frozen ~ thawed, Frozen thawed ~ frozen) => TwoPhase thawed frozen where type Thawed frozen :: * type Frozen thawed :: * thaw :: frozen -> thawed freeze :: thawed -> frozen This is the translation I'd expect for the fundep. And ideally, in the future, you could use the original class with fundeps as sugar for the above, because fundeps are a nice way of expressing mutual dependency like this (just as associated types are nicer than making the associated type a class parameter as is required by fundeps). -- Dan
On Fri, Sep 17, 2010 at 10:19 PM, Dan Doel
On Friday 17 September 2010 4:04:26 pm Gábor Lehel wrote:
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*?
What about:
class (Thawed frozen ~ thawed, Frozen thawed ~ frozen) => TwoPhase thawed frozen where type Thawed frozen :: * type Frozen thawed :: * thaw :: frozen -> thawed freeze :: thawed -> frozen
This is the translation I'd expect for the fundep. And ideally, in the future, you could use the original class with fundeps as sugar for the above, because fundeps are a nice way of expressing mutual dependency like this (just as associated types are nicer than making the associated type a class parameter as is required by fundeps).
Hmm. I had a similar thought, but dismissed it because I was under the impression that you needed to use all the parameters of the class as parameters of its associated types. But apparently that was mistaken -- or, at least, your example compiles. :) The redundancy is sort of annoying ('thawed' and 'Thawed frozen' both being necessary and necessarily equivalent). This is a case where associated type defaults would be helpful, to eliminate at least some of it (namely, having to define Thawed and Frozen in every instance, even though only one definition is possible). Anyway, it's a shame you can't really decouple the two halves as in my nonworking example, but this is nicer than the other alternative I had. Thanks!
-- Dan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Work is punishment for failing to procrastinate effectively.
On Saturday 18 September 2010 8:27:45 am Gábor Lehel wrote:
Hmm. I had a similar thought, but dismissed it because I was under the impression that you needed to use all the parameters of the class as parameters of its associated types. But apparently that was mistaken -- or, at least, your example compiles. :)
Classes of the form I sent: class (T1 b ~ a, T2 a ~ b) => C a b where type T1 b :: * type T2 a :: * ... actually desugar into the following: type family T1 b :: * type family T2 a :: * class (T1 b ~ a, T2 a ~ b) => C a b where ... So the parameters of the families needn't match the parameters of the class. It does impose some additional constraint on your making instances of the families whenever you make an instance of the class, which wouldn't be there if you wrote them separately, but I think that's it. This is also important when translating classes like the following: class Closed a | -> a where ... You can only write a single instance of that class (although, I'd guess that GHC currently accepts 'instance Closed a where ...', which should be illegal). To translate it to type families, you write: class Closed a where type T :: * ... a family with no parameters. The compiler will only allow you to write one instance for that family, but you must provide an instance for each instance of the Closed class. Hence, you can only write a single instance of the Closed class. -- Dan
participants (2)
-
Dan Doel -
Gábor Lehel