Hi Miguel On 18 Jul 2009, at 07:58, Miguel Mitrofanov wrote:
Oops... Sorry, wrong line. Should be
isAB :: forall p. p A -> p B -> p x
Yep, dependent case analysis, the stuff of my thesis,...
On 18 Jul 2009, at 10:51, Miguel Mitrofanov wrote:
What is it for?
I have a different purpose in mind. I want to write localize :: (forall a. Equipment a => Abstract a) -> Concrete rather than localize :: (forall a. F1 a -> ... -> Fn a -> Abstract a) -> Concrete so I can use the type class machinery to pass around the dictionaries of equipment. I want to make sure that nobody else gets the equipment. It's possible that I don't need to be so extreme: it's enough that there's no other way to use Abstracts than via localize.
Yes, you would know that only A and B are Public, but you have no way of telling that to the compiler.
I usually prefer something like that:
class Public x where blah :: ... isAB :: forall y. (A -> y) -> (B -> y) -> x -> y
But now I can write bogus instances of Public with genuine implementations of blah and wicked lies for isAB. It is important to use the dependent version, otherwise I might have instance Public (A, B) where isAB af bf (a, b) = af a and lots more, without even lying.
Both solutions, however, allow the user to declare some new instances when GeneralizedNewtypeDeriving is enabled.
I'm scared. What about this? data EQ :: * -> * -> * where Refl :: EQ x x class Public x where blah :: EQ x Fred instance Public Fred where blah = Refl What happens when I say newtype Jim = Hide Fred deriving Public ? I tried it. I get blah :: EQ Jim Fred It's clear that GeneralizedNewtypeDeriving goes too far. I hope a class with *no* instances in public has no newtype leak! Fun stuff. Cheers Conor