newtype coercion wrapping status

classic Classic list List threaded Threaded
19 messages Options
Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Joachim Breitner-2
Hi,

after following SPJ?s latest advise and implementing the newtype
coercion classes directly and ad-hoc in the type checker (in TcInteract,
similarly to the SingI), this rewrite of the code is now working (for
some value of working):

What works now
==============

The setup:
Prelude> :info GHC.NT.castNT
castNT :: NT a b => a -> b     -- Defined in ?GHC.NT?

Simple cases:

Prelude> newtype Age = Age Int deriving Show
Prelude> GHC.NT.castNT (Age 1) :: Int
1
Prelude> GHC.NT.castNT (1::Int) :: Age
Age 1

Unrolling several newtypes at the same time:

Prelude> newtype Bar = Bar Age deriving Show
Prelude> newtype Baz = Baz Int deriving Show
Prelude> GHC.NT.castNT (Baz 1) :: Bar
Bar (Age 1)

Unrolling newtypes with type arguments, even polymorphically:

Prelude> newtype MyMB a = MyMB (Maybe a) deriving Show
Prelude> GHC.NT.castNT (Just ()) :: MyMB ()
MyMB (Just ())
Prelude> let f1 = (\x -> GHC.NT.castNT (Just x)) :: a -> MyMB a
Prelude> f1 True
MyMB (Just True)
Prelude> let f2 = (\x -> GHC.NT.castNT (Just x)) :: GHC.NT.NT a b => a -> MyMB b
Prelude> f2 (Baz 1) :: MyMB Bar
MyMB (Just (Bar (Age 1)))


Unrolling inside type constructor arguments, including functions and
tuples:

Prelude> GHC.NT.castNT (Just (Age 1)) :: Maybe Int
Just 1
Prelude> (GHC.NT.castNT Age :: (Baz -> Bar)) (Baz 1)
Bar (Age 1)
Prelude> GHC.NT.castNT (Age 1, Baz 1) :: (Bar, Int)
(Bar (Age 1),1)


Arbitrary changing of Phantom types:

Prelude> data Proxy a = Proxy deriving Show
Prelude> GHC.NT.castNT (Proxy :: Proxy Int) :: Proxy Bool
Proxy

Unwanted casting can be prevented by role annotations:

Prelude> :set -XRoleAnnotations
Prelude> data Map a at N b = Map a b deriving Show
Prelude> GHC.NT.castNT (Map () (1::Int)) :: Map () Bar
Map () (Bar (Age 1))
Prelude> GHC.NT.castNT (Map (1::Int) ()) :: Map Bar ()

<interactive>:24:1:
    No instance for (GHC.NT.NT (Map Int ()) (Map Bar ()))
      arising from a use of ?GHC.NT.castNT?
    In the expression: GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()
    In an equation for ?it?:
        it = GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()

GADTs have the roles set automatically, so this does not work either, as
expected:

Prelude> :set -XGADTs -XStandaloneDeriving
Prelude> data GADT a where GADT :: GADT Int
Prelude> deriving instance Show (GADT a)
Prelude> GHC.NT.castNT GADT :: GADT Age

<interactive>:37:1:
    No instance for (GHC.NT.NT (GADT Int) (GADT Age))
      arising from a use of ?GHC.NT.castNT?
    In the expression: GHC.NT.castNT GADT :: GADT Age
    In an equation for ?it?: it = GHC.NT.castNT GADT :: GADT Age


What is still missing
=====================

 * Good error messages (see above)
 * Checking if all involved data constructors are in scope
 * Marking these data constructors as used (to avoid unused import
   warnings)
 * Prevent the user from writing NT instances himself.
 * Code documentation
 * User documentation
 * Tests.
 * More testing, especially with weird types and advanced type system
   features, e.g. type families.

What needs more thought
=======================

 * How to handle recursive newtypes, such as
   newtype Void = Void Void
   or worse
   newtype Foo a = Foo (Foo (a,a))?
   With the current setup, which is equivalent to an instance
   instance NT (Foo (a,a)) b => NT (Foo a) b
   it will cause constraint checking to loop.
   
   I?m inclined to simply not create instances for recursive newtypes,
   or alternatively only in modules with UndecidableInstances turned on.

The code
========

The code can be reviewed at
https://github.com/nomeata/ghc/compare/ntclass-clean
with the corresponding ghc-prim changes at
https://github.com/nomeata/packages-ghc-prim/compare/ntclass-clean

I followed the example of SingI and created a new constructor in data
EvTerm for NT evidences. There are three kinds of evidence for NT t1 t2:
One for t1 == t2, one for unfolding a newtype (at t1 or t2), and one if
t1 and t2 have the same type constructor at the head. This corresponds
to the the shapes of NT instances one would write by hand.

The evidence is created in TcInteract, in a function called by
matchClassInst, and turned into Core by dsEvTerm in DsBinds.

Currently there is both a type constructor GHC.Types.EqR that boxes EqR#
and is built-in, and a type class GHC.NT.NT, which has just one method
of type EqR. This is because it seems to be quite tricky to create a
built-in class in GHC.Prim, but also causes a bit of extra bookkeeping.
I guess the final patch will somehow avoid this indirection.

Richard, can you have a look at my changes to
compiler/types/Coercion.lhs, if they are sound? I found that there was a
hardcoded role of Nominal where, with my code, also Representational
could occur.


Is this going in the right direction, both design and
implementation-wise?


Thanks,
Joachim
--
Joachim ?nomeata? Breitner
  mail at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130902/246dcd0d/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Richard Eisenberg-2
Yay! I'm really excited to see this coming along so nicely, especially as it has such a nice interaction with roles.

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

- 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.

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

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

- 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?

- 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.)

- Without more comments, I get a little lost in the desugaring of EvNT and friends. But, I was able to trace the use of roles, and it looks sensible. In particular, it looks like mkTyConAppCo's preconditions around roles are satisfied, which can be tricky.

- It looks like you left some old code on line 1860 of TcInteract.

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

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?

Thanks,
Richard

On Sep 2, 2013, at 10:42 AM, Joachim Breitner <mail at joachim-breitner.de> wrote:

> Hi,
>
> after following SPJ?s latest advise and implementing the newtype
> coercion classes directly and ad-hoc in the type checker (in TcInteract,
> similarly to the SingI), this rewrite of the code is now working (for
> some value of working):
>
> What works now
> ==============
>
> The setup:
> Prelude> :info GHC.NT.castNT
> castNT :: NT a b => a -> b     -- Defined in ?GHC.NT?
>
> Simple cases:
>
> Prelude> newtype Age = Age Int deriving Show
> Prelude> GHC.NT.castNT (Age 1) :: Int
> 1
> Prelude> GHC.NT.castNT (1::Int) :: Age
> Age 1
>
> Unrolling several newtypes at the same time:
>
> Prelude> newtype Bar = Bar Age deriving Show
> Prelude> newtype Baz = Baz Int deriving Show
> Prelude> GHC.NT.castNT (Baz 1) :: Bar
> Bar (Age 1)
>
> Unrolling newtypes with type arguments, even polymorphically:
>
> Prelude> newtype MyMB a = MyMB (Maybe a) deriving Show
> Prelude> GHC.NT.castNT (Just ()) :: MyMB ()
> MyMB (Just ())
> Prelude> let f1 = (\x -> GHC.NT.castNT (Just x)) :: a -> MyMB a
> Prelude> f1 True
> MyMB (Just True)
> Prelude> let f2 = (\x -> GHC.NT.castNT (Just x)) :: GHC.NT.NT a b => a -> MyMB b
> Prelude> f2 (Baz 1) :: MyMB Bar
> MyMB (Just (Bar (Age 1)))
>
>
> Unrolling inside type constructor arguments, including functions and
> tuples:
>
> Prelude> GHC.NT.castNT (Just (Age 1)) :: Maybe Int
> Just 1
> Prelude> (GHC.NT.castNT Age :: (Baz -> Bar)) (Baz 1)
> Bar (Age 1)
> Prelude> GHC.NT.castNT (Age 1, Baz 1) :: (Bar, Int)
> (Bar (Age 1),1)
>
>
> Arbitrary changing of Phantom types:
>
> Prelude> data Proxy a = Proxy deriving Show
> Prelude> GHC.NT.castNT (Proxy :: Proxy Int) :: Proxy Bool
> Proxy
>
> Unwanted casting can be prevented by role annotations:
>
> Prelude> :set -XRoleAnnotations
> Prelude> data Map a at N b = Map a b deriving Show
> Prelude> GHC.NT.castNT (Map () (1::Int)) :: Map () Bar
> Map () (Bar (Age 1))
> Prelude> GHC.NT.castNT (Map (1::Int) ()) :: Map Bar ()
>
> <interactive>:24:1:
>    No instance for (GHC.NT.NT (Map Int ()) (Map Bar ()))
>      arising from a use of ?GHC.NT.castNT?
>    In the expression: GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()
>    In an equation for ?it?:
>        it = GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()
>
> GADTs have the roles set automatically, so this does not work either, as
> expected:
>
> Prelude> :set -XGADTs -XStandaloneDeriving
> Prelude> data GADT a where GADT :: GADT Int
> Prelude> deriving instance Show (GADT a)
> Prelude> GHC.NT.castNT GADT :: GADT Age
>
> <interactive>:37:1:
>    No instance for (GHC.NT.NT (GADT Int) (GADT Age))
>      arising from a use of ?GHC.NT.castNT?
>    In the expression: GHC.NT.castNT GADT :: GADT Age
>    In an equation for ?it?: it = GHC.NT.castNT GADT :: GADT Age
>
>
> What is still missing
> =====================
>
> * Good error messages (see above)
> * Checking if all involved data constructors are in scope
> * Marking these data constructors as used (to avoid unused import
>   warnings)
> * Prevent the user from writing NT instances himself.
> * Code documentation
> * User documentation
> * Tests.
> * More testing, especially with weird types and advanced type system
>   features, e.g. type families.
>
> What needs more thought
> =======================
>
> * How to handle recursive newtypes, such as
>   newtype Void = Void Void
>   or worse
>   newtype Foo a = Foo (Foo (a,a))?
>   With the current setup, which is equivalent to an instance
>   instance NT (Foo (a,a)) b => NT (Foo a) b
>   it will cause constraint checking to loop.
>
>   I?m inclined to simply not create instances for recursive newtypes,
>   or alternatively only in modules with UndecidableInstances turned on.
>
> The code
> ========
>
> The code can be reviewed at
> https://github.com/nomeata/ghc/compare/ntclass-clean
> with the corresponding ghc-prim changes at
> https://github.com/nomeata/packages-ghc-prim/compare/ntclass-clean
>
> I followed the example of SingI and created a new constructor in data
> EvTerm for NT evidences. There are three kinds of evidence for NT t1 t2:
> One for t1 == t2, one for unfolding a newtype (at t1 or t2), and one if
> t1 and t2 have the same type constructor at the head. This corresponds
> to the the shapes of NT instances one would write by hand.
>
> The evidence is created in TcInteract, in a function called by
> matchClassInst, and turned into Core by dsEvTerm in DsBinds.
>
> Currently there is both a type constructor GHC.Types.EqR that boxes EqR#
> and is built-in, and a type class GHC.NT.NT, which has just one method
> of type EqR. This is because it seems to be quite tricky to create a
> built-in class in GHC.Prim, but also causes a bit of extra bookkeeping.
> I guess the final patch will somehow avoid this indirection.
>
> Richard, can you have a look at my changes to
> compiler/types/Coercion.lhs, if they are sound? I found that there was a
> hardcoded role of Nominal where, with my code, also Representational
> could occur.
>
>
> Is this going in the right direction, both design and
> implementation-wise?
>
>
> Thanks,
> Joachim
> --
> Joachim ?nomeata? Breitner
>  mail at joachim-breitner.de ? http://www.joachim-breitner.de/
>  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
>  Debian Developer: nomeata at debian.org
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs




Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Joachim Breitner-2
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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130902/e7ea86cb/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Richard Eisenberg-2

On Sep 2, 2013, at 5:33 PM, Joachim Breitner wrote:
>
>> - 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.
>

Done, and pushed. Thanks for bringing this to my attention.

Richard




Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Simon Peyton Jones
In reply to this post by Joachim Breitner-2
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?



| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
| Joachim Breitner
| Sent: 02 September 2013 15:43
| To: ghc-devs at haskell.org
| Subject: newtype coercion wrapping status
|
| Hi,
|
| after following SPJ?s latest advise and implementing the newtype
| coercion classes directly and ad-hoc in the type checker (in TcInteract,
| similarly to the SingI), this rewrite of the code is now working (for
| some value of working):
|
| What works now
| ==============
|
| The setup:
| Prelude> :info GHC.NT.castNT
| castNT :: NT a b => a -> b     -- Defined in ?GHC.NT?
|
| Simple cases:
|
| Prelude> newtype Age = Age Int deriving Show
| Prelude> GHC.NT.castNT (Age 1) :: Int
| 1
| Prelude> GHC.NT.castNT (1::Int) :: Age
| Age 1
|
| Unrolling several newtypes at the same time:
|
| Prelude> newtype Bar = Bar Age deriving Show
| Prelude> newtype Baz = Baz Int deriving Show
| Prelude> GHC.NT.castNT (Baz 1) :: Bar
| Bar (Age 1)
|
| Unrolling newtypes with type arguments, even polymorphically:
|
| Prelude> newtype MyMB a = MyMB (Maybe a) deriving Show
| Prelude> GHC.NT.castNT (Just ()) :: MyMB ()
| MyMB (Just ())
| Prelude> let f1 = (\x -> GHC.NT.castNT (Just x)) :: a -> MyMB a
| Prelude> f1 True
| MyMB (Just True)
| Prelude> let f2 = (\x -> GHC.NT.castNT (Just x)) :: GHC.NT.NT a b => a -
| > MyMB b
| Prelude> f2 (Baz 1) :: MyMB Bar
| MyMB (Just (Bar (Age 1)))
|
|
| Unrolling inside type constructor arguments, including functions and
| tuples:
|
| Prelude> GHC.NT.castNT (Just (Age 1)) :: Maybe Int
| Just 1
| Prelude> (GHC.NT.castNT Age :: (Baz -> Bar)) (Baz 1)
| Bar (Age 1)
| Prelude> GHC.NT.castNT (Age 1, Baz 1) :: (Bar, Int)
| (Bar (Age 1),1)
|
|
| Arbitrary changing of Phantom types:
|
| Prelude> data Proxy a = Proxy deriving Show
| Prelude> GHC.NT.castNT (Proxy :: Proxy Int) :: Proxy Bool
| Proxy
|
| Unwanted casting can be prevented by role annotations:
|
| Prelude> :set -XRoleAnnotations
| Prelude> data Map a at N b = Map a b deriving Show
| Prelude> GHC.NT.castNT (Map () (1::Int)) :: Map () Bar
| Map () (Bar (Age 1))
| Prelude> GHC.NT.castNT (Map (1::Int) ()) :: Map Bar ()
|
| <interactive>:24:1:
|     No instance for (GHC.NT.NT (Map Int ()) (Map Bar ()))
|       arising from a use of ?GHC.NT.castNT?
|     In the expression: GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()
|     In an equation for ?it?:
|         it = GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()
|
| GADTs have the roles set automatically, so this does not work either, as
| expected:
|
| Prelude> :set -XGADTs -XStandaloneDeriving
| Prelude> data GADT a where GADT :: GADT Int
| Prelude> deriving instance Show (GADT a)
| Prelude> GHC.NT.castNT GADT :: GADT Age
|
| <interactive>:37:1:
|     No instance for (GHC.NT.NT (GADT Int) (GADT Age))
|       arising from a use of ?GHC.NT.castNT?
|     In the expression: GHC.NT.castNT GADT :: GADT Age
|     In an equation for ?it?: it = GHC.NT.castNT GADT :: GADT Age
|
|
| What is still missing
| =====================
|
|  * Good error messages (see above)
|  * Checking if all involved data constructors are in scope
|  * Marking these data constructors as used (to avoid unused import
|    warnings)
|  * Prevent the user from writing NT instances himself.
|  * Code documentation
|  * User documentation
|  * Tests.
|  * More testing, especially with weird types and advanced type system
|    features, e.g. type families.
|
| What needs more thought
| =======================
|
|  * How to handle recursive newtypes, such as
|    newtype Void = Void Void
|    or worse
|    newtype Foo a = Foo (Foo (a,a))?
|    With the current setup, which is equivalent to an instance
|    instance NT (Foo (a,a)) b => NT (Foo a) b
|    it will cause constraint checking to loop.
|
|    I?m inclined to simply not create instances for recursive newtypes,
|    or alternatively only in modules with UndecidableInstances turned on.
|
| The code
| ========
|
| The code can be reviewed at
| https://github.com/nomeata/ghc/compare/ntclass-clean
| with the corresponding ghc-prim changes at
| https://github.com/nomeata/packages-ghc-prim/compare/ntclass-clean
|
| I followed the example of SingI and created a new constructor in data
| EvTerm for NT evidences. There are three kinds of evidence for NT t1 t2:
| One for t1 == t2, one for unfolding a newtype (at t1 or t2), and one if
| t1 and t2 have the same type constructor at the head. This corresponds
| to the the shapes of NT instances one would write by hand.
|
| The evidence is created in TcInteract, in a function called by
| matchClassInst, and turned into Core by dsEvTerm in DsBinds.
|
| Currently there is both a type constructor GHC.Types.EqR that boxes EqR#
| and is built-in, and a type class GHC.NT.NT, which has just one method
| of type EqR. This is because it seems to be quite tricky to create a
| built-in class in GHC.Prim, but also causes a bit of extra bookkeeping.
| I guess the final patch will somehow avoid this indirection.
|
| Richard, can you have a look at my changes to
| compiler/types/Coercion.lhs, if they are sound? I found that there was a
| hardcoded role of Nominal where, with my code, also Representational
| could occur.
|
|
| Is this going in the right direction, both design and
| implementation-wise?
|
|
| Thanks,
| Joachim
| --
| Joachim ?nomeata? Breitner
|   mail at joachim-breitner.de ? http://www.joachim-breitner.de/
|   Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
|   Debian Developer: nomeata at debian.org

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Nicolas Trangez
On Wed, 2013-09-04 at 11:55 +0000, Simon Peyton-Jones wrote:
> 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?

git clone -b ntclass-clean https://github.com/nomeata/ghc.git

should do the job.

Nicolas




Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Joachim Breitner-2
In reply to this post by Simon Peyton Jones
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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130904/30418fa2/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Joachim Breitner-2
In reply to this post by Joachim Breitner-2
Hi,

another small update on the newtype coercion stuff (which is now named
Prelude GHC.Types GHC.Prim> :info coerce
coerce :: Coercible a b => a -> b        -- Defined in ?GHC.Prim?
), diffs at:
https://github.com/nomeata/ghc/compare/ntclass-clean
https://github.com/nomeata/packages-ghc-prim/compare/ntclass-clean
https://github.com/nomeata/ghc-testsuite/compare/ntclass-clean

Am Montag, den 02.09.2013, 16:42 +0200 schrieb Joachim Breitner:
> What is still missing
> =====================
>
>  * Good error messages (see above)

Done; at a first approximation to good, see
https://github.com/nomeata/ghc-testsuite/blob/ntclass-clean/tests/typecheck/should_fail/TcCoercibleFail.stderr
for the error messages for most cases, corresponding to the code at
https://github.com/nomeata/ghc-testsuite/blob/ntclass-clean/tests/typecheck/should_fail/TcCoercibleFail.hs

>  * Checking if all involved data constructors are in scope
?

>  * Code documentation
?, Note [Coercible Instances]

>  * Tests.
?; see https://github.com/nomeata/ghc-testsuite/compare/ntclass-clean

I have also removed the previous indirection of
        data EqR a b = EqR# (a ~R# b)
        class Coercible a b where coercion :: EqR a b
and instead have only type constructor akin to EqR, which is also the
type constructor of the Coercible class. I hope it does not break any
implicit invariants somewhere.

> * Prevent the user from writing NT instances himself.
?

Left to do:

>  * Marking these data constructors as used (to avoid unused import
>    warnings)
>  * User documentation
>  * More testing, especially with weird types and advanced type system
>    features, e.g. type families.


NB, there is a wart with regard to constructor-in-scope-testing:

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.

But it is not enough: 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)
to convert "Foo Int" to "Foo Age". So not only the constructor of the
data type needs to be in scope, but also _all constructors_ of _all
typecons_ used in the definition of Hack. This is also enforced.

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)
is possible. Currently, the code is not flexible enough. Is that problem
relevant? (I?d be inclined to leave it simple for now and see if someone
complains.)

Interesting fact: If the last example would read
        newtype D a b = MkD (a, Foo b)
and the constraint to solve would be
        Coercible (D Int ()) (D Age ()),
then GHC would actually solve it; not with
        instance Coercible a a
        instance Coercible a b => Coercible a Age
        instance Coercible a b => Coercible (D a c) (D b c)
(becaue the latter instance is not allowed, as explaint above), but
using a slight detour:
        instance Coercible a a
        instance Coercible a b => Coercible a Age
        instance (Coercible a b, Coercible c d) => Coercible (a,c) (b,d)
        instance Coercible (a, Foo b) c => Coercible (D a b) c
        instance Coercible a (b, Foo c) => Coercible a (D b c)
That it works with data but not with newtype might be
counter-intuitive... but still, this is probably far to specific to
worry about.

Greetings,
Joachim  

--
Joachim ?nomeata? Breitner
  mail at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130906/1c42ebaa/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Simon Peyton Jones
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

-------------- next part --------------
An embedded message was scrubbed...
From: unknown sender
Subject: no subject
Date: no date
Size: 38
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130906/74f62c38/attachment.eml>

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Joachim Breitner-2
Hi,

Am Freitag, den 06.09.2013, 15:03 +0000 schrieb Simon Peyton-Jones:
> Sounds amazing Joachim -- great work.

Thanks!

> | 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.
       
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.

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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130906/3ffbbcb9/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Simon Peyton Jones
| 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 at 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 <rep_ty>.
  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 at joachim-breitner.de ? http://www.joachim-breitner.de/
|   Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
|   Debian Developer: nomeata at debian.org

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Joachim Breitner-2
Hi,

Am Freitag, den 06.09.2013, 16:47 +0000 schrieb Simon Peyton-Jones:

> So
>
> * for newtypes
>        newtype N a = MkN <rep-ty>
>   the coercion is between (N a) and its representation type <rep_ty>.
>   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.

Sounds reasonable. Implementation is simple, I just remove the check
that I had added:
https://github.com/nomeata/ghc/commit/46c6c7
https://github.com/nomeata/ghc-testsuite/commit/d5c13

One question which is left open, which I cannot answer: Are there
situations where the library author wants to prevent coercion, but needs
a non-Nominal role for some other reasons? But we?ll see.

> Roles are in HEAD so you can use them right now.

I know, my patch is against head and already makes use of roles:

TcCoercibleFail.hs:16:8:
    No instance for (Coercible (Map Int ()) (Map Age ()))
      because the first type argument of ?Map? has role Nominal,
      but the arguments ?Int? and ?Age? differ
      arising from a use of ?coerce?
    In the expression: coerce
    In the expression: coerce $ Map one () :: Map Age ()
    In an equation for ?foo3?: foo3 = coerce $ Map one () :: Map Age ()

Greetings,
Joachim


--
Joachim ?nomeata? Breitner
  mail at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130906/b533b142/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Richard Eisenberg-2
In reply to this post by Simon Peyton Jones

On Sep 6, 2013, at 12:47 PM, Simon Peyton-Jones <simonpj at microsoft.com> wrote:

>
> So
>
> * for newtypes
>       newtype N a = MkN <rep-ty>
>  the coercion is between (N a) and its representation type <rep_ty>.
>  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


Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Joachim Breitner-2
Hi,

Am Samstag, den 07.09.2013, 12:16 -0400 schrieb Richard Eisenberg:
> On Sep 6, 2013, at 12:47 PM, Simon Peyton-Jones <simonpj at microsoft.com> wrote:
> 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.

I agree, that is why I raised the point.

> 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?

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.

> 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.


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.

Greetings,
Joachim

--
Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130907/fa34368f/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Simon Peyton Jones

| 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

Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Richard Eisenberg-2
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 <simonpj at microsoft.com> 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
>




Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Simon Peyton Jones
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 at cis.upenn.edu]
| Sent: 07 September 2013 18:46
| To: Simon Peyton-Jones
| Cc: Joachim Breitner; ghc-devs at 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 <simonpj at microsoft.com>
| 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
| >




Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Richard Eisenberg-2
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.

Richard

On Sep 9, 2013, at 10:51 AM, Simon Peyton-Jones wrote:

> 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 at cis.upenn.edu]
> | Sent: 07 September 2013 18:46
> | To: Simon Peyton-Jones
> | Cc: Joachim Breitner; ghc-devs at 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 <simonpj at microsoft.com>
> | 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
> | >
>
>




Reply | Threaded
Open this post in threaded view
|

newtype coercion wrapping status

Joachim Breitner-2
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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130910/27788b6b/attachment.pgp>