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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
