Superclass Cycle via Associated Type

[Gábor Lehel]

2011/7/23 Edward Kmett <ekmett at gmail.com>:
> 2011/7/23 Gábor Lehel <illissius at gmail.com>
>>
>> 2011/7/22 Dan Doel <dan.doel at gmail.com>:
>> > 2011/7/22 Gábor Lehel <illissius at gmail.com>:
>> >> 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.