
2011/7/23 Edward Kmett
2011/7/23 Gábor Lehel
2011/7/22 Dan Doel
: 2011/7/22 Gábor Lehel
: Yeah, this is pretty much what I ended up doing. As I said, I don't think I lose anything in expressiveness by going the MPTC route, I just think the two separate but linked classes way reads better. So it's just a "would be nice" thing. Do recursive equality superclasses make sense / would they be within the realm of the possible to implement?
Those equality superclasses are not recursive in the same way, as far as I can tell. The specifications for classes require that there is no chain:
C ... => D ... => E ... => ... => C ...
However, your example just had (~) as a context for C, but C is not required by (~). And the families involved make no reference to C, either. A fully desugared version looks like:
type family Frozen a :: * type family Thawed a :: *
class (..., Thawed (Frozen t) ~ t) => Mutable t where ...
I think this will be handled if you use a version where equality superclasses are allowed.
To be completely explicit, I had:
class (Immutable (Frozen t), Thawed (Frozen t) ~ t) => Mutable t where type Frozen t ... class (Mutable (Thawed t), Frozen (Thawed t) ~ t) => Immutable t where type Thawed t ...
I had a similar issue in my representable-tries package.
I believe we actually discussed this on IRC. :-)
In there I had type family Key (f :: * -> *) :: * class Indexable f where index :: f a -> Key f -> a class Indexable f => Representable f where tabulate :: (Key f -> a) -> f a such that tabulate and index witness the isomorphism from f a to (Key f -> a). So far no problem. But then to provide a Trie type that was transparent I wanted. class (Representable (BaseTrie e), Traversable (BaseTrie e), Key (BaseTrie e) ~ e) => HasTrie e where type BaseTrie e :: * -> * type (:->:) e = BaseTrie e which I couldn't use prior to the new class constraints patch. The reason I mention this is that my work around was to weaken matters a bit class (Representable (BaseTrie e)) => HasTrie e where type BaseTrie e :: * -> * embedKey :: e -> Key (BaseTrie e) projectKey :: Key (BaseTrie e) -> e
This dodged the need for superclass equality constraints by just requiring me to supply the two witnesses to the isomorphism between e and Key (BaseTrie e). Moreover, in my case it helped me produce instances, because the actual signatures involved about 20 more superclasses, and this way I could make new HasTrie instances for newtype wrappers just by defining an embedding and projection pair for some type I'd already defined. But, it did require me to pay for a newtype wrapper which managed the embedding and projection pairs. newtype e :->: a = Trie (BaseTrie e a) In your setting, perhaps something like:
type family Frozen t type family Thawed t class Immutable (Frozen t) => Mutable t where thawedFrozen :: t -> Thawed (Frozen t) unthawedFrozen :: Thawed (Frozen t) -> t
class Mutable (Thawed t) => Immutable t where frozenThawed :: t -> Frozen (Thawed t) unfrozenThawed :: Frozen (Thawed t) -> t
would enable you to explicitly program with the two isomorphisms, while avoiding superclass constraints.
Hmm, that's an interesting thought. If I'm guesstimating correctly, defining instances would be more cumbersome than with the MPTC method, but using them would be nicer, provided I write helper functions to hide the use of the isomorphism witnesses. I'll give it a try. Thanks! I seem to recall that in one of your packages, you had a typeclass method returning a GADT wrapping the evidence for the equality of two types, as a workaround for the lack of superclass equality constraints -- what makes you prefer that workaround in one case and this one in another? -- Work is punishment for failing to procrastinate effectively.