Could you explain why you think it's a language feature? We have plenty of "magic" stuff like unsafePerformIO, unsafeCoerce, or StableNames, which are not documented in the manual. Just curious. Roman * Richard Eisenberg [2013-09-15 16:48:16-0400]

Very cool!

In the feature as pushed, is it possible to use coerce on any old newtype? If so, then it really is a language feature and probably should go into the manual, if `coerce` is exposed.

What was the end result of the discussion on abstraction? Can a library control how its types are coerced?

Richard

On Sep 13, 2013, at 6:13 PM, Joachim Breitner wrote:

...

Hi,

Am Montag, den 09.09.2013, 11:26 -0500 schrieb Austin Seipp:

...

It sounds like Simon thinks your work is good to go, so when your tree is clean, feel free to push.

done!

Given that in the final form the feature, to the user, looks like a library and not a language extension, I decided to put the documentation not in the users guide, but only in the haddock for coerce and Coercible.

So far they only live in GHC.Prim. Should we expose them in GHC.Prim for 7.8, or only in 7.10?

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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Hi, Am Sonntag, den 15.09.2013, 17:24 -0400 schrieb Richard Eisenberg:

Because, from a user's point of view, defining

...

newtype Age = MkAge Int

automatically creates Coercible instances

...

instance Coercible Age Int instance Coercible Int Age

and defining datatypes also creates instances. This looks like a user-visible language feature to me, and I think it should be documented in the manual.

not really; if you type ":info Coercible" you see that there are no instances created. Just the type-checking of uses of coerce is a bit special. I think the question is rather: Where would the user search for documentation. And given that there are identifiers related to the feature (Coercible, coercion), the haddocks for that are the natural place to search. And as I’d like to avoid duplication, I’d not put the docs somewhere else again. I don’t mind adding a pointer from the “Special built-in functions” section to the haddock docs, though, if you think it would be helpful. Greetings, Joachim -- Joachim Breitner e-Mail: mail@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata@joachim-breitner.de

Hi, Am Sonntag, den 15.09.2013, 17:49 -0400 schrieb Richard Eisenberg:

To be clear, I'm not asking for an explanation for me -- I think I know what's going on here.

Sorry if you got that impression; I have no doubt that you understand the feature (possibly better than me!)

I just think that this behavior requires a small section in the user manual, because it's a user-visible change to the language that GHC compiles. I would say the haddock docs could point to the user manual, to avoid the duplication (which I similarly dislike, for sure!)

Well, the question of which location points to which one is close to bikeshedding, so I’ll just pull the “I did it” card here (until shouted down by a larger crowd). But a mention in the user manual will not hurt: Can you suggest a section? Then I’ll put in a small paragraph with an reference to the haddocks. Greetings, Joachim -- Joachim Breitner e-Mail: mail@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata@joachim-breitner.de

Hi, Am Sonntag, den 15.09.2013, 16:48 -0400 schrieb Richard Eisenberg:

What was the end result of the discussion on abstraction? Can a library control how its types are coerced?

there is no end result, as this is just a language feature. But the current state of affairs is that: * A newtype can be casted only if its constructor is visible. * Casting below a type constructor (instance Coercible a b => Coercible (Maybe a) (Maybe b)) is possible if the roles allow it; the constructor does not have to be visible or exposed, except that * in Safe Haskell code, the constructor or the typecon (and all constructors of all typecons used in the definition of the typecon) has to be visible. So once you know your syntax for role annotations it would make sense to annotate the arguments of Set and Map (first one only) in base before we release 7.8. Greetings, Joachim PS: Do we have regular builds of master, including users’ guide and haddock, somewhere that I can link to in such a mail? -- Joachim Breitner e-Mail: mail@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata@joachim-breitner.de

a) A newtype can be casted only if its constructor is visible. b) Casting below a type constructor (instance Coercible a b => Coercible (Maybe a) (Maybe b)) is possible if the roles allow it; the constructor does not have to be visible or exposed, except that c) in Safe Haskell code, the constructor or the typecon (and all constructors of all typecons used in the definition of the typecon) has to be visible.

Has anyone talked to David Terei about the Safe Haskell check (c) above? It's not clear to me whether (c) is necessary. (And it would need to recursively check those tycoons, I think. Are you doing that?) As to Generalised Newtype Deriving, my earnest hope is that we can make GND safe for Safe Haskell. it was only excluded before because of #1496, which is now solved. For GND Richard proposes: | I propose that (deriving instance Class Newtype) should work when | | 1) The roles allow it (i.e., the role of the last parameter of Class is not nominal) | (as currently implemented), | 2) The constructor of Newtype is visible (as currently implemented), AND | 3) If we imagine Constraint and * to be the same, we could derive Coercible a b | => Coercible (Class a) (Class b), according to the check Joachim just elaborated. | (the new bit) But what does (3) mean? It means (a,b,c) above. Well, (a) holds because of (2), (b) holds because of (1), which leaves (c). That is, the all the class methods must be visible here. That makes sense. If you were to write the instance by hand, you'd need to be able to see the class methods. It's analogous to (c). So replace (3) by "All the class methods are visible". And think of (3) like (c); that is, only reqd for Safe Haskell. But let's see if David and David even want (c)/(3) for Safe Haskell! Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Richard | Eisenberg | Sent: 15 September 2013 22:57 | To: Joachim Breitner | Cc: ghc-devs@haskell.org | Subject: Re: Coercible class (Was: newtype wrappers) | | Great -- that makes a lot of sense to me. Sorry if you had to repeat yourself here. | | Does this mean that it is impossible to coerce a (Map String Int) to a (Map String | Age) in Safe code? I expect so. I think this is suboptimal, but there might be a | small way to patch this small weakness in the design without large changes. | | The Safe Haskell check seems a little global, but that might be the only sensible | way to do it, and I was somewhat hoping that would be your answer. Why? | Because I think GeneralizedNewtypeDeriving (GND) should piggyback on your | algorithm: | | In specific, I propose that (deriving instance Class Newtype) should work when | | 1) The roles allow it (i.e., the role of the last parameter of Class is not nominal) | (as currently implemented), | 2) The constructor of Newtype is visible (as currently implemented), AND | 3) If we imagine Constraint and * to be the same, we could derive Coercible a b | => Coercible (Class a) (Class b), according to the check Joachim just elaborated. | (the new bit) | | Clause (3) is trivially satisfied outside of Safe Haskell. In Safe Haskell, it would | require looking at all the types used in all the methods in Class. This makes good | sense to me, as it would (I think) fix #5498. Does this idea make sense? | | A question about the existing check: How does it treat constraints? For example, | say we have | | > data Foo a where -- a's role is representational; this is NOT a GADT | > MkFoo :: Ord a => a -> Foo a | > | > newtype Age = MkAge Int deriving Eq -- the Eq is to satisfy Ord's superclass | constraint | > instance Ord Age where | > (MkAge a) `compare` (MkAge b) = b `compare` a -- args are reversed | > | > fooInt :: Foo Int | > fooInt = MkFoo 5 | > | > fooAge :: Foo Age | > fooAge = coerce fooInt -- it seems this would be accepted | > | > confused :: Foo Age -> Ordering | > confused (MkFoo x) = x `compare` (MkAge 0) | | What will confused do? It has potentially two, conflicting instances for Ord to | hand: one in the global context; and one from pattern-matching MkFoo, which was | creating by coercing from Ord Int. I have a hard time seeing the solution to be | IncoherentInstances, because it's not clear which chunk of code would trigger the | need for that extension. | | Also, it's possible for there to be "abstract" classes, which don't export all of their | methods or use other tricks to prevent instances (non-exported superclasses, for | example) outside of the library. Are these checked for? | | Actually, come to think of it, the example I have above doesn't really interact with | the Safe Haskell check -- it's a problem regardless, unless I'm confused. | | Richard | | PS: If these concerns are answered in documentation you've already written, feel | free just to send a link, even just to a file on github -- I hate repeating myself | about these things, too! | | On Sep 15, 2013, at 5:13 PM, Joachim Breitner | wrote: | | > Hi, | > | > Am Sonntag, den 15.09.2013, 16:48 -0400 schrieb Richard Eisenberg: | >> What was the end result of the discussion on abstraction? Can a | >> library control how its types are coerced? | > | > there is no end result, as this is just a language feature. But the | > current state of affairs is that: | > * A newtype can be casted only if its constructor is visible. | > * Casting below a type constructor (instance Coercible a b => Coercible | > (Maybe a) (Maybe b)) is possible if the roles allow it; the constructor | > does not have to be visible or exposed, except that | > * in Safe Haskell code, the constructor or the typecon (and all | > constructors of all typecons used in the definition of the typecon) has | > to be visible. | > | > So once you know your syntax for role annotations it would make sense to | > annotate the arguments of Set and Map (first one only) in base before we | > release 7.8. | > | > Greetings, | > Joachim | > | > PS: Do we have regular builds of master, including users' guide and | > haddock, somewhere that I can link to in such a mail? | > | > -- | > Joachim Breitner | > e-Mail: mail@joachim-breitner.de | > Homepage: http://www.joachim-breitner.de | > ICQ#: 74513189 | > Jabber-ID: nomeata@joachim-breitner.de | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > http://www.haskell.org/mailman/listinfo/ghc-devs | | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-devs

Richard raises a question about coherence below. (Coherence, not soundness.) But it's a coherence problem we already have. Given his Foo type, | > data Foo a where -- a's role is representational; this is NOT a GADT | > MkFoo :: Ord a => a -> Foo a suppose we define bar :: Foo T -> Bool bar (MkFoo x) = x>x At the use of (>) we have potentially two instances of (Ord T) available - one bound by the MkFoo constructor - one top-level instance and we could easily have more; et bar2 :: Foo T -> Foo T -> Bool bar2 (MkFoo x) (MkFoo y) = x>y These instances could potentially have different implementations if the (Foo T) values were constructed in different modules, each with its own (instance Ord T). So this isn't really a new problem, and it's one that doesn't seem too bad in practice. Simon | A question about the existing check: How does it treat constraints? For example, | say we have | | > data Foo a where -- a's role is representational; this is NOT a GADT | > MkFoo :: Ord a => a -> Foo a | > | > newtype Age = MkAge Int deriving Eq -- the Eq is to satisfy Ord's superclass | constraint | > instance Ord Age where | > (MkAge a) `compare` (MkAge b) = b `compare` a -- args are reversed | > | > fooInt :: Foo Int | > fooInt = MkFoo 5 | > | > fooAge :: Foo Age | > fooAge = coerce fooInt -- it seems this would be accepted | > | > confused :: Foo Age -> Ordering | > confused (MkFoo x) = x `compare` (MkAge 0) | | What will confused do? It has potentially two, conflicting instances for Ord to | hand: one in the global context; and one from pattern-matching MkFoo, which was | creating by coercing from Ord Int. I have a hard time seeing the solution to be | IncoherentInstances, because it's not clear which chunk of code would trigger the | need for that extension. | | Also, it's possible for there to be "abstract" classes, which don't export all of their | methods or use other tricks to prevent instances (non-exported superclasses, for | example) outside of the library. Are these checked for? | | Actually, come to think of it, the example I have above doesn't really interact with | the Safe Haskell check -- it's a problem regardless, unless I'm confused.