Hi, Am Montag, den 02.09.2013, 12:07 -0400 schrieb Richard Eisenberg:

Here are some specific thoughts, upon reviewing your (surprisingly short!) patch:

well, note the long list of thing that remain to be done. Also, the code went through several iterations already; I guess that helps as well :-)

- I strongly dislike the name NT (and derivatives), for at least two reasons: 1) Someone new to this work won't know what it means, and 2) it's useful for things unrelated to newtypes (because of phantoms). How about "safeCoerce"? The class could have the name "Coercible". Neither of these names conflict on a default search at Hoogle.

The name is a working title, and your suggestions are good. I might prefer something that also hints as to why things are coercible and hints that it is somehow related to representation.

- Why box ~R#? Couldn't castEqR just take an unboxed R equality?

I guesst castEqR could, but it seems I still need a TyCon that boxes ~R# so that it can be used as the type of a class method. (As mentioned, this TyCon could also be the TyCon of the class itself, I just need to find out how to wire that up.)

- If keeping boxed ~R#, you might want to add an ASSERT in mkEqReprBox ensuring that the coercion passed in has role R. (Use coercionRole.)

Will do.

- It looks like you plan to make the NT class more wired in (line 507 of TcEvidence). Would this get rid of the Class parameter to EvNT and then simplify mkNT?

Correct. The Class parameter is just a work-around for now, and mkNT and mkUnNT can simple be removed.

- getEqRolePredTys never seems to care about its Role return value. I'm happy about this, because the type-checker doesn't really know about roles. (It assumes everything is Nominal, which is how users would expect type-checking to behave, I think.)

That part of the patch is in the “I had to do this to make it work” because in some cases getRolePredTys would have thrown assertions about Representational roles appearing. If you think this is fine, the easiest would be to simply have getPredTys work with the different kinds of equalities. Also, that it currently works with NT should probably not be the final word.

- The changes in Coercion are correct -- the use of Nominal that you removed harkened to the days when all CoVars were Nominal.

Would you prefer to apply these changes to HEAD independently of the coercion feature? It would keep my patch cleaner.

After looking at it all, I wonder if shoehorning this feature into the class / instance mechanism is the right way to go. How much is that buying us? The instance lookup mechanism for NT is totally customized (as it should be, it seems). So, how much harder would it be to make this a free-floating feature, separate from classes? This would mean adding a new thing with kind (* -> * -> Constraint) to replace "NT". (In a perfect world, this could be spelled ≈, but I'm not a huge fan of Unicode syntax in reality.) But, there would be no need to worry about user-defined instances, and all the wired-in class stuff could be gotten rid of. It's not that I think the class/instance approach is that bad, but we've had to wander so far away from using GHC's built-in features around instance lookup that I think we should re-examine.

Thoughts?

This would move it closer to Eq and Eq#, right? I still don’t understand all of the code involved in constraint handling, especially with constraints that are not classes. I believe that it buys us the infrastructure of requesting new constraints, of solving constraints only once, and of getting an error message that looks familiar to the user. OTOH this infrastructure is not fully suited, e.g. for "newtype Void = Void Void" it creates looping EqR values. I’ll read through more of the code and see if we can do without classes alltogether. Thanks for your review, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org

Hi, Am Mittwoch, den 04.09.2013, 11:55 +0000 schrieb Simon Peyton-Jones:

Joachim,

How do I get your code?

bash$ git clone https://github.com/nomeata/ghc/compare/ntclass-clean newtype-wrappers Cloning into 'newtype-wrappers'... fatal: https://github.com/nomeata/ghc/compare/ntclass-clean/info/refs not found: did you run git update-server-info on the server?

The command $ git clone -b ntclass-clean https://github.com/nomeata/ghc/ should work, or alternatively $ git fetch https://github.com/nomeata/ghc/ ntclass-clean:ntclass-clean inside a working copy to just add this branch (without adding an explicit remote). Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org

Sounds amazing Joachim -- great work. | Consider | data Foo a = MkFoo (a,a). | The (virtual) instance | instance Coercible a b => Coercible (Foo a) (Foo b) | can only be used when MkFoo is in scope, as otherwise the user could | break abstraction barriers. This is enforced. Whoa! Where did this instance come from? I thought that we generated precisely two (virtual) instances for Foo: instance Coercible a (b,b) => Coercible a (Foo b) instance Coercible (a,b) b => Coercible (Foo a) b and no others. That it. Done. That was precisely the payload of my message of 2 August, attached. Each of the two is valid if the data constructor MkFoo is in scope. No other checks are needed. | Assume MkFoo is not in scope. Then the user could | define | data Hack a = MkHack (Foo a) | and use the (virtual) instance | instance Coercible a b => Coercible (Hack a) (Hack b) No no no! The virtual instances are instance Coercible (Foo a) b => Coercible (Hack a) b instance Coercible a (Foo b) => Coercible a (Hack b) and now the difficulty you describe disappears. | But it might, in corner cases, be too strict. Consider | data D a b = MkD (a, Foo b) | now the programmer might expect that, even without MkFoo in scope, that | instance Coercible a b => Coercible (D a c) (D b c) The two instances are instance Coercible (a, Foo b) x => Coercible (D a b) x instance Coercible x (a, Foo b) => Coercible x (D a b) Now can I prove (Coercible (D a c) (D b c))? Use the above rules twice; I then need Coercible (a, Foo c) (b, Foo c) and yes I can prove that if I have (Coerciable a b). In short, I think that if you use the approach I outlined, all these problems go away. Am I wrong? Simon

| Well, that is the case when we want to unwrap a newtype. But this is not | the case here: We have a data type and we want to cast one of its type | arguments. Clearly, we want to have | instance Coercible a b => Coercible [a] [b] | right? The instance above is just an other instance (heh) of that form. Bother. You are right. I was thinking of newtypes, and your point was about data types. Sorry. Re-reading, your message makes perfect sense. But I hate it. And hang on! One of our poster-child examples is module Map ( Map, insert, lookup, ... ) where data Map a b = MkMap [(a,b)] So Map is abstract. But we ABSOLUTELY DO want to allow people to coerce (Map a b) to (Map a c) if a,c are coercible. We were going to do that by role annotations. The exact syntax is still under debate (http://ghc.haskell.org/trac/ghc/ticket/8185), but you say something like data Map a@N b = MkMap [(a,b)] and now the instance should look like instance Coercible b1 b2 => Coercible (Map a b1) (Map a b2) Nothing to do with the visibility of Map's data constructors! So * for newtypes newtype N a = MkN <rep-ty> the coercion is between (N a) and its representation type . The coercion is allowed if the data constructor MkN is in scope * for data types (T a), the coercion is between (T a) and (T b), The coercion is allowed if the roles allow it. The two are handled quite differently. OK? This is far from obvious (since I was very confused about it), so worth writing up on the design page. As well as implementing. Roles are in HEAD so you can use them right now. Simon | | The two virtual instances that you mention only make sense for newtype, | _in addition_ to the usual “cast something inside this type”. | | > [..] | > | > In short, I think that if you use the approach I outlined, all these | problems go away. Am I wrong? | | I believe so; I hope I just clarified it. | | Greetings, | Joachim | | -- | Joachim “nomeata” Breitner | mail@joachim-breitner.de • http://www.joachim-breitner.de/ | Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C | Debian Developer: nomeata@debian.org

On Sep 6, 2013, at 12:47 PM, Simon Peyton-Jones wrote:

So

* for newtypes newtype N a = MkN <rep-ty> the coercion is between (N a) and its representation type . The coercion is allowed if the data constructor MkN is in scope

* for data types (T a), the coercion is between (T a) and (T b), The coercion is allowed if the roles allow it.

The two are handled quite differently.

This makes me say "Yikes!" I've always lived under the impression that changing the word "newtype" to "data" should have exactly 0 effect on the compile-time behavior of Haskell programs. Yet, you're proposing that

module Foo (T) where -- MkT is *not* exported

newtype T a = MkT [a]

is different from the same with "newtype" replaced with "data". To wit, in the "data" version, the instance (Coercible a b => Coercible (T a) (T b)) would exist, but this would not be derivable in the "newtype" version. Right? A related issue is that, even with roles, I don't think GeneralizedNewtypeDeriving (GND) is in the Safe Haskell subset because it can break abstraction barriers -- you can use GND even when a newtype's constructor is not in scope. The above proposal for coercions will have the same problem. What to do? Map should certainly not export its constructor(s). Yet, we want (Coercible a b => Coercible (Map x a) (Map x b)). It seems that the writer of Map would have to explicitly export this instance. This goes at odds with the idea of "there aren't any instances of Coercible, really", but otherwise I have a hard time seeing how this would all work. Am I missing something here? Richard

| In the current code, the | instance Coercible a b => Coercible (T a) (T b) | is available for both data and newtypes, if T’s type argument has | Representational role, but independent of any constructor presence. See | the note at | https://github.com/nomeata/ghc/compare/ntclass-clean#L9R1902 | for a concise and complete list of the conditions for a Coercible | instance. Right! I explained that badly the first time; thanks for clarifying Joachim. So newtype and data behave alike, except that newtype has the *additional* property that if its constructor is available you can coerce to the representation type. | If I understood Simon’s last suggestion correctly than exporting a type | constructor with a non-Nominal role means “I am fine if you cast this | argument”. If this is not desired (e.g. maybe Ptr a is an example here), | then the library author has to annotate the type argument as Nominal. Yes, that's right. In theory someone could want the coercible instance *plus* the nominal role, or vice versa, but I think we can jump that bridge if we come to it. Simon

The reason it's not safe in Safe Haskell is precisely #1496, the newtpye deriving bug. Now that's fixed, Safe Haskell can remove the safety check. Probably. This is another question that could usefully be articulated on the design page, Joachim. Simon | -----Original Message----- | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | Sent: 07 September 2013 18:46 | To: Simon Peyton-Jones | Cc: Joachim Breitner; ghc-devs@haskell.org | Subject: Re: newtype coercion wrapping status | | OK -- thanks for clarifying. This all sits better with me. | | But, I'm still a little concerned about the "Safe Haskell" implications. | My understanding is that allowing coercions when the constructor is not | exported will not be considered "Safe". Here's a way forward: | | Currently: a type is considered abstract when its constructors are not | exported. | | Future proposal: a type is considered abstract when its constructors are | not exported AND its type parameters are all at role Nominal. | | Under this new definition of "abstract", a library writer that remembers | not to export a constructor but neglects to use a role annotation should | consider a type *not* to be abstract. Is this what we want? | | Richard | | On Sep 7, 2013, at 1:16 PM, Simon Peyton-Jones | wrote: | | > | > | In the current code, the | > | instance Coercible a b => Coercible (T a) (T b) | > | is available for both data and newtypes, if T's type argument has | > | Representational role, but independent of any constructor presence. | See | > | the note at | > | https://github.com/nomeata/ghc/compare/ntclass-clean#L9R1902 | > | for a concise and complete list of the conditions for a Coercible | > | instance. | > | > Right! I explained that badly the first time; thanks for clarifying | Joachim. | > | > So newtype and data behave alike, except that newtype has the | *additional* property that if its constructor is available you can coerce | to the representation type. | > | > | If I understood Simon's last suggestion correctly than exporting a | type | > | constructor with a non-Nominal role means "I am fine if you cast this | > | argument". If this is not desired (e.g. maybe Ptr a is an example | here), | > | then the library author has to annotate the type argument as Nominal. | > | > Yes, that's right. In theory someone could want the coercible instance | *plus* the nominal role, or vice versa, but I think we can jump that | bridge if we come to it. | > | > Simon | >

Hi, Am Montag, den 09.09.2013, 13:25 -0400 schrieb Richard Eisenberg:

According to the original post and the comments on #5498 (http://ghc.haskell.org/trac/ghc/ticket/5498), breaking through abstraction is another reason for keeping GND outside of Safe Haskell. I'm worried that the same concern would affect newtype coercions given the current proposal.

an easy fix would be to disallow coerce in Safe Haskell. A similarly easy fix would be to add the requirements that constructors have to be in scope when generating the instance Coercible a b => Coercible (D a) (D b) rule in Safe Haskell code. Although that might cripple the feature too much, but not more than not having the feature at all. I think the latter is a good compromise for the non-advertised release. Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org