[Haskell-cafe] is closing a class this easy?

[Conor McBride]

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