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

Hi Stefan On 18 Jul 2009, at 09:42, Stefan Holdermans wrote:

Conor,

...

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.

Now, I am scared. This should be regarded as a bug in generalised newtype deriving, shouldn't it? I would expect newtype deriving to be unable to come up with instances that cannot be written by hand.

I think the latter is a useful general principle for "deriving". The trouble here is that somewhere along the line (GADTs? earlier?) it became possible to construct candidates for p :: * -> * which don't respect isomorphism. These tend to be somewhat intensional in nature, and they mess up the transfer of functionality. If we could be sure that all such a p would do with its parameter (x, say) is trade in values of x (as opposed to trading in the identity of x), then we could be sure that p respects isomorphisms. I'm hoping that a category theorist will say something about dinaturality at this point, because I'd like to understand that stuff. I wonder if there's a potential refinement of the kind system lurking here, distinguishing *, types-up-to-iso, from |*|, types-up-to-identity. That might help us to detect classes for which newtype deriving is inappropriate: GADTs get indexed over |*|, not *; classes of *s are derivable, but classes of |*|s are not. I certainly don't have a clear proposal just now. It looks like an important distinction: recognizing it somehow might buy us something.

I would have expected people out on the streets marching to GHC headquarters by now; how can you stay so calm?

GHC HQ are up to their armpits in newtypes already. This distinction between type equality and (trivial) type isomorphism is something they're already facing. I don't know if they've solved this problem yet, but I suspect they're in the area. No need for a commotion. All the best Conor

| Now, I am scared. This should be regarded as a bug in generalised | newtype deriving, shouldn't it? I would expect newtype deriving to be | unable to come up with instances that cannot be written by hand. | | I would have expected people out on the streets marching to GHC | headquarters by now; how can you stay so calm? Indeed, it's a known problem: http://hackage.haskell.org/trac/ghc/ticket/1496 It's a serious problem too, because it affects type soundness. But I have been moving slowly on fixing it, because I want a proper fix not a hack. Dimitrios and I have a variety of solutions now, some of which have the flavour of what's suggested below: | > I wonder if there's a potential refinement of the kind system lurking | > here, distinguishing *, types-up-to-iso, from |*|, types-up-to- | > identity. | > That might help us to detect classes for which newtype deriving is | > inappropriate: GADTs get indexed over |*|, not *; classes of *s are | > derivable, but classes of |*|s are not. I certainly don't have a clear | > proposal just now. It looks like an important distinction: recognizing | > it somehow might buy us something. Stay tuned. Simon

Hi Wolfgang On 18 Jul 2009, at 13:42, Wolfgang Jeltsch wrote:

Am Samstag, 18. Juli 2009 11:43 schrieb Conor McBride:

...

The trouble here is that somewhere along the line (GADTs? earlier?) it became possible to construct candidates for p :: * -> * which don't respect isomorphism.

Hello Conor,

I’m not sure whether I exactly understand what you mean here. I think, it’s the following:

Say, you have a type A and define a type B as follows:

newtype B = B A

Then, for any p :: * -> *, the type p A should be isomorphic to p B, i.e., it should basically contain the same values. This is no longer true with GADTs since you can define something like this:

data GADT a where

GADT :: GADT A

Now, GADT :: GADT A but not GADT :: GADT B.

Is this what you mean?

Yes, that's what I mean.

...

These tend to be somewhat intensional in nature, and they mess up the transfer of functionality.

Could you maybe elaborate on this?

Just as you've shown, we can use GADTs to express a p such that p A is inhabited but p B is not(*) Moreover, we can write type families which make TF A = IO String TF B = String so it'd be better not to get A and B confused. But all of these nasties rely on taking an intensional view of types as pieces of syntax, rather than the extensional view of types as sets of values. Predicates (to use a Curry-Howardism) which rely only on the extensional properties of types can be relied upon to respect isomorphism, and indeed to respect trivial isomorphisms trivially. (You can refine this to *inclusion* if you pay attention to co/contra-variance. This would give us inflate :: Functor f => f Void -> f x as a no-op.) Your GADT is an intensional predicate --- "being A", rather than "having the values of A" --- so it respects fewer equations. Consider a type expression t[x], over a free type variable x. Suppose you have some f :: a -> b and g :: b -> a. For the most part, you can use these to construct t[f,g> :: t[a] -> t[b] and hence t[g,f> :: t[b] -> t[a] by recursion on the structure of t. E.g,, x[f, g> = f Bool[f, g> = id (s -> t)[f, g> = \ h -> t[f,g> . h . s[g,f> ... You'll find that t[id,id> = id. But you'll get stuck at GADTs and type families. Functions both ways don't give you enough information: you need equality (same objects, different morphisms). Type classes are predicates: "supporting a dictionary". If they happen to be extensional predicates, then they should support newtype deriving. Can we draw out this distinction somehow? Interesting place to go... Cheers Conor (*) usual caveats for bottom spotters

On 18 Jul 2009, at 16:49, Wolfgang Jeltsch wrote:

Am Samstag, 18. Juli 2009 08:58 schrieb Miguel Mitrofanov:

...

Oops... Sorry, wrong line. Should be

isAB :: forall p. p A -> p B -> p x

Is this a well-known approach for closing classes?

I have an impression that this is kinda folklore. But I can't provide any references; I don't even remember if I invented it myself or not.