RE: D2038: [WIP] TysPrim: Generalize kind of (->)
Replying by email because I'm on a train. Simon Huh. Put otherwise, your point is this. Suppose we have the following kind for `(->)`: (->) :: forall v1 v2 r1 r2. TYPE v1 r1 -> TYPE v2 r2 -> Type To coerce from (C a -> Int) to (a -> Int) we'd have to cough up a coercion `g`: g : (->) Vanilla Vanilla Ptr Ptr (C a) Int ~R (->) Constraint Vanilla Ptr Ptr a Int And now (Nth 1 g :: Vanilla ~R Constraint). Nothing about `KindCo` there; it's just that `(->)` takes some kind arguments. But that can only happen if `(->)` has suitable roles. What if it doesn't? What if we just had an axiom axArrow v :: (->) Vanilla v ~R (->) Constraint v or something like that. Then we get [W] g : (->) Vanilla Vanilla Ptr Ptr (C a) Int ~R (->) Constraint Vanilla Ptr Ptr a Int We decompose partly and solve thus g = (axArrow Vanilla) <Ptr> <Ptr> axC <Int> Simon From: noreply@phabricator.haskell.org [mailto:noreply@phabricator.haskell.org] Sent: 31 January 2017 12:51 To: Simon Peyton Jones <simonpj@microsoft.com> Subject: [Differential] [Commented On] D2038: [WIP] TysPrim: Generalize kind of (->) goldfire added a comment. View Revision<https://phabricator.haskell.org/D2038> In D2038#89360<https://phabricator.haskell.org/D2038#89360>, @simonpj<https://phabricator.haskell.org/p/simonpj/> wrote: To avoid being able to extract ContraintRep ~R LiftedPtrRep we decided to weaken one of the coercion constructors, the one that gets a kind coercion from a type coercion. We don't need it, and it's awkward here. The problem is that we need it with this patch. I was able to weaken this coercion constructor (KindCo) in my patch D3023<https://phabricator.haskell.org/D3023>, but this patch uses it in a fundamental way that we can't get around. To wit: class C a where meth :: a axC :: (C a :: Constraint) ~R (a :: Type) Now, we wish to cast C a -> a to a -> a.. This cast will look like (->) ?? <LiftedRep> axC <a>. What goes in the ??? It's got to be something involving KindCo axC, which is disallowed as per our earlier decision. Therein lies the problem. As for reify: Yes, I'm agreed with that email. But is that implemented yet? Is a design settled on? I don't see a ghc-proposal. Are we wiling to take a dependency on that work in order to get this done? To be clear, my chief worry isn't that these problems cannot be solved by any means -- I'm just worried about the timing of this all and our desire to get 8.2 out the door. REPOSITORY rGHC Glasgow Haskell Compiler REVISION DETAIL https://phabricator.haskell.org/D2038 EMAIL PREFERENCES https://phabricator.haskell.org/settings/panel/emailpreferences/ To: bgamari, goldfire, austin Cc: simonpj, RyanGlScott, thomie
On Jan 31, 2017, at 5:41 PM, Simon Peyton Jones <simonpj@microsoft.com> wrote:
But that can only happen if `(->)` has suitable roles. What if it doesn’t?
The “correct” roles for (->) of the kind you gave is `nominal nominal nominal nominal representational representational`. That is, the dependent arguments are nominal, and the others are representational. This is because all kind-level coercions are nominal. You seem to be suggesting giving (->) different roles. I honestly don’t know what that would mean -- normally, GHC prevents you from specifying a weaker role than it would infer. It smells pretty foul to me, but I can’t quite put my finger on what would go wrong at the moment.
What if we just had an axiom
axArrow v :: (->) Vanilla v ~R (->) Constraint v
I think we’d also need one for results... but maybe not.
or something like that. Then we get
[W] g : (->) Vanilla Vanilla Ptr Ptr (C a) Int ~R (->) Constraint Vanilla Ptr Ptr a Int
We decompose partly and solve thus
g = (axArrow Vanilla) <Ptr> <Ptr> axC <Int>
And this works only if we weaken (->)’s roles. This whole road just feels like the wrong way, as soon as we started contemplating a heterogeneous axiom, which are ruled out in the literature, even when we have kind equalities. I think the Right Answer is to get rid of newtype-classes & fix reify, and I’m worried that anything short of that will fail catastrophically at some point. Otherwise, it’s patches on top of patches. I don’t think there is disagreement here, but there is the question about what to do for 8.2.... and unless we’re ready to roll out the new reify, I think the best course of action is to delay the new Typeable and all this Constraint v Type stuff until 8.4. (The new levity polymorphism stuff already committed is hunky-dory.) Richard
Simon <> From: noreply@phabricator.haskell.org <mailto:noreply@phabricator.haskell.org> [mailto:noreply@phabricator.haskell.org <mailto:noreply@phabricator.haskell.org>] Sent: 31 January 2017 12:51 To: Simon Peyton Jones <simonpj@microsoft.com <mailto:simonpj@microsoft.com>> Subject: [Differential] [Commented On] D2038: [WIP] TysPrim: Generalize kind of (->)
goldfire added a comment.
View Revision <https://phabricator.haskell.org/D2038>
In D2038#89360 <https://phabricator.haskell.org/D2038#89360>, @simonpj <https://phabricator.haskell.org/p/simonpj/> wrote:
To avoid being able to extract ContraintRep ~R LiftedPtrRep we decided to weaken one of the coercion constructors, the one that gets a kind coercion from a type coercion. We don't need it, and it's awkward here.
The problem is that we need it with this patch. I was able to weaken this coercion constructor (KindCo) in my patchD3023 <https://phabricator.haskell.org/D3023>, but this patch uses it in a fundamental way that we can't get around. To wit:
class C a where meth :: a
axC :: (C a :: Constraint) ~R (a :: Type) Now, we wish to cast C a -> a to a -> a.. This cast will look like (->) ?? <LiftedRep> axC <a>. What goes in the??? It's got to be something involving KindCo axC, which is disallowed as per our earlier decision. Therein lies the problem.
As for reify: Yes, I'm agreed with that email. But is that implemented yet? Is a design settled on? I don't see a ghc-proposal. Are we wiling to take a dependency on that work in order to get this done?
To be clear, my chief worry isn't that these problems cannot be solved by any means -- I'm just worried about the timing of this all and our desire to get 8.2 out the door.
REPOSITORY rGHC Glasgow Haskell Compiler
REVISION DETAIL https://phabricator.haskell.org/D2038 <https://phabricator.haskell.org/D2038>
EMAIL PREFERENCES https://phabricator.haskell.org/settings/panel/emailpreferences/ <https://phabricator.haskell.org/settings/panel/emailpreferences/>
To: bgamari, goldfire, austin Cc: simonpj, RyanGlScott, thomie
Richard Eisenberg <rae@cs.brynmawr.edu> writes: snip
I think the Right Answer is to get rid of newtype-classes & fix reify, and I’m worried that anything short of that will fail catastrophically at some point. Otherwise, it’s patches on top of patches.
I don’t think there is disagreement here, but there is the question about what to do for 8.2.... and unless we’re ready to roll out the new reify, I think the best course of action is to delay the new Typeable and all this Constraint v Type stuff until 8.4. (The new levity polymorphism stuff already committed is hunky-dory.)
I am going to let you and Simon decide on this. While I would certainly like to get the Typeable stuff off my plate (it's not terribly easy to rebase), I am also acutely aware of the pressure to keep the release cycle moving. In particular, I would like to avoid another drawn out release like 8.0 if at all possible. Of course, I would be happy to help with the implementation of whatever plan we decide upon. Cheers, - Ben
I had another thought on my drive home: why do we need to sort out Constraint v Type for 8.2? I have the patch, and it's essentially all set. But it weakens equality in a way that's troublesome for D2038 and introduces heterogeneous axioms, which are strange, ill-understood beasts. And I don't think we need it. On the other hand, D2038 is essential for the new Typeable, because it's the only way we can give (->) a proper kind. So, I propose: 1. Hold off on Constraint v Type until after the branch is cut. 2. Do what we can to mitigate Constraint v Type confusion vis-a-vis Typeable. (For example, make sure that there aren't Typeable instances for both, and have TcTypeable provide the Type instance whenever the Constraint instance is requested.) 3. Advertise that GHC will be a little confused on this point, and that, as far as Typeable is concerned, Constraint and Type are synonymous. 4. On the Constraint v Type patch, restore the full power of KindCo. This makes the type system broken, but I don't think the sky will come crashing down. 5. Merge Constraint v Type after the branch is cut. This will make GHC HEAD unsound in a new way, but no one will notice unless they try. 6. File a priority-highest bug to eliminate newtype-classes (which beget heterogeneous axioms in the Constraint/=Type world). 7. Finish the first-class reification design and implement before 8.4. 8. Remove newtype-classes, thus eliminating heterogeneous axioms and the unsoundness mentioned in (5). This route seems, to me, far preferable to monkeying around with roles and such in ways that we have no assurances are sound. (Remember, roles are there to keep the type system safe and sound. They were not added simply to annoy everyone, though they accomplish that goal quite nicely.) What do we think? It's not ideal, but I think it's the best of suboptimal alternatives. And it's no worse than 8.0 w.r.t. Constraint v Type. Richard
On Jan 31, 2017, at 5:56 PM, Richard Eisenberg <rae@cs.brynmawr.edu> wrote:
On Jan 31, 2017, at 5:41 PM, Simon Peyton Jones <simonpj@microsoft.com <mailto:simonpj@microsoft.com>> wrote:
But that can only happen if `(->)` has suitable roles. What if it doesn’t?
The “correct” roles for (->) of the kind you gave is `nominal nominal nominal nominal representational representational`. That is, the dependent arguments are nominal, and the others are representational. This is because all kind-level coercions are nominal. You seem to be suggesting giving (->) different roles. I honestly don’t know what that would mean -- normally, GHC prevents you from specifying a weaker role than it would infer. It smells pretty foul to me, but I can’t quite put my finger on what would go wrong at the moment.
What if we just had an axiom
axArrow v :: (->) Vanilla v ~R (->) Constraint v
I think we’d also need one for results... but maybe not.
or something like that. Then we get
[W] g : (->) Vanilla Vanilla Ptr Ptr (C a) Int ~R (->) Constraint Vanilla Ptr Ptr a Int
We decompose partly and solve thus
g = (axArrow Vanilla) <Ptr> <Ptr> axC <Int>
And this works only if we weaken (->)’s roles.
This whole road just feels like the wrong way, as soon as we started contemplating a heterogeneous axiom, which are ruled out in the literature, even when we have kind equalities.
I think the Right Answer is to get rid of newtype-classes & fix reify, and I’m worried that anything short of that will fail catastrophically at some point. Otherwise, it’s patches on top of patches.
I don’t think there is disagreement here, but there is the question about what to do for 8.2.... and unless we’re ready to roll out the new reify, I think the best course of action is to delay the new Typeable and all this Constraint v Type stuff until 8.4. (The new levity polymorphism stuff already committed is hunky-dory.)
Richard
Simon <> From: noreply@phabricator.haskell.org <mailto:noreply@phabricator.haskell.org> [mailto:noreply@phabricator.haskell.org <mailto:noreply@phabricator.haskell.org>] Sent: 31 January 2017 12:51 To: Simon Peyton Jones <simonpj@microsoft.com <mailto:simonpj@microsoft.com>> Subject: [Differential] [Commented On] D2038: [WIP] TysPrim: Generalize kind of (->)
goldfire added a comment.
View Revision <https://phabricator.haskell.org/D2038>
In D2038#89360 <https://phabricator.haskell.org/D2038#89360>, @simonpj <https://phabricator.haskell.org/p/simonpj/> wrote:
To avoid being able to extract ContraintRep ~R LiftedPtrRep we decided to weaken one of the coercion constructors, the one that gets a kind coercion from a type coercion. We don't need it, and it's awkward here.
The problem is that we need it with this patch. I was able to weaken this coercion constructor (KindCo) in my patchD3023 <https://phabricator.haskell.org/D3023>, but this patch uses it in a fundamental way that we can't get around. To wit:
class C a where meth :: a
axC :: (C a :: Constraint) ~R (a :: Type) Now, we wish to cast C a -> a to a -> a.. This cast will look like (->) ?? <LiftedRep> axC <a>. What goes in the??? It's got to be something involving KindCo axC, which is disallowed as per our earlier decision. Therein lies the problem.
As for reify: Yes, I'm agreed with that email. But is that implemented yet? Is a design settled on? I don't see a ghc-proposal. Are we wiling to take a dependency on that work in order to get this done?
To be clear, my chief worry isn't that these problems cannot be solved by any means -- I'm just worried about the timing of this all and our desire to get 8.2 out the door.
REPOSITORY rGHC Glasgow Haskell Compiler
REVISION DETAIL https://phabricator.haskell.org/D2038 <https://phabricator.haskell.org/D2038>
EMAIL PREFERENCES https://phabricator.haskell.org/settings/panel/emailpreferences/ <https://phabricator.haskell.org/settings/panel/emailpreferences/>
To: bgamari, goldfire, austin Cc: simonpj, RyanGlScott, thomie
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org <mailto:ghc-devs@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs <http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs>
Richard Eisenberg <rae@cs.brynmawr.edu> writes:
I had another thought on my drive home: why do we need to sort out Constraint v Type for 8.2? I have the patch, and it's essentially all set. But it weakens equality in a way that's troublesome for D2038 and introduces heterogeneous axioms, which are strange, ill-understood beasts. And I don't think we need it.
On the other hand, D2038 is essential for the new Typeable, because it's the only way we can give (->) a proper kind.
Snipped well-considered plan for proceeding.
This route seems, to me, far preferable to monkeying around with roles and such in ways that we have no assurances are sound. (Remember, roles are there to keep the type system safe and sound. They were not added simply to annoy everyone, though they accomplish that goal quite nicely.)
:)
What do we think? It's not ideal, but I think it's the best of suboptimal alternatives. And it's no worse than 8.0 w.r.t. Constraint v Type.
This sounds quite reasonable to me. I will need to fix up the remaining issues in D2038 surrounding Constraint, but I think this shouldn't be so difficult. The only reason I haven't tried already was my belief that Constraint/Type would be resolved soon. I'll try to push another version of D2038 tonight. Cheers, - Ben
1. Hold off on Constraint v Type until after the branch is cut. Good idea. I think that’d be OK. It’s no worse than the status quo. I’m MUCH more keen to get the TypeRep stuff in, because it has been in the works for nearly two years!! So let’s do 1-3 pronto. Who is acting there. Just Ben? Or are there bits Richard needs to help with? As to 4 onwards I still want to talk to you about roles. Simon From: Richard Eisenberg [mailto:rae@cs.brynmawr.edu] Sent: 01 February 2017 01:19 To: Simon Peyton Jones <simonpj@microsoft.com> Cc: ghc-devs@haskell.org Subject: Re: D2038: [WIP] TysPrim: Generalize kind of (->) I had another thought on my drive home: why do we need to sort out Constraint v Type for 8.2? I have the patch, and it's essentially all set. But it weakens equality in a way that's troublesome for D2038 and introduces heterogeneous axioms, which are strange, ill-understood beasts. And I don't think we need it. On the other hand, D2038 is essential for the new Typeable, because it's the only way we can give (->) a proper kind. So, I propose: 1. Hold off on Constraint v Type until after the branch is cut. 2. Do what we can to mitigate Constraint v Type confusion vis-a-vis Typeable. (For example, make sure that there aren't Typeable instances for both, and have TcTypeable provide the Type instance whenever the Constraint instance is requested.) 3. Advertise that GHC will be a little confused on this point, and that, as far as Typeable is concerned, Constraint and Type are synonymous. 4. On the Constraint v Type patch, restore the full power of KindCo. This makes the type system broken, but I don't think the sky will come crashing down. 5. Merge Constraint v Type after the branch is cut. This will make GHC HEAD unsound in a new way, but no one will notice unless they try. 6. File a priority-highest bug to eliminate newtype-classes (which beget heterogeneous axioms in the Constraint/=Type world). 7. Finish the first-class reification design and implement before 8.4. 8. Remove newtype-classes, thus eliminating heterogeneous axioms and the unsoundness mentioned in (5). This route seems, to me, far preferable to monkeying around with roles and such in ways that we have no assurances are sound. (Remember, roles are there to keep the type system safe and sound. They were not added simply to annoy everyone, though they accomplish that goal quite nicely.) What do we think? It's not ideal, but I think it's the best of suboptimal alternatives. And it's no worse than 8.0 w.r.t. Constraint v Type. Richard On Jan 31, 2017, at 5:56 PM, Richard Eisenberg <rae@cs.brynmawr.edu<mailto:rae@cs.brynmawr.edu>> wrote: On Jan 31, 2017, at 5:41 PM, Simon Peyton Jones <simonpj@microsoft.com<mailto:simonpj@microsoft.com>> wrote: But that can only happen if `(->)` has suitable roles. What if it doesn’t? The “correct” roles for (->) of the kind you gave is `nominal nominal nominal nominal representational representational`. That is, the dependent arguments are nominal, and the others are representational. This is because all kind-level coercions are nominal. You seem to be suggesting giving (->) different roles. I honestly don’t know what that would mean -- normally, GHC prevents you from specifying a weaker role than it would infer. It smells pretty foul to me, but I can’t quite put my finger on what would go wrong at the moment. What if we just had an axiom axArrow v :: (->) Vanilla v ~R (->) Constraint v I think we’d also need one for results... but maybe not. or something like that. Then we get [W] g : (->) Vanilla Vanilla Ptr Ptr (C a) Int ~R (->) Constraint Vanilla Ptr Ptr a Int We decompose partly and solve thus g = (axArrow Vanilla) <Ptr> <Ptr> axC <Int> And this works only if we weaken (->)’s roles. This whole road just feels like the wrong way, as soon as we started contemplating a heterogeneous axiom, which are ruled out in the literature, even when we have kind equalities. I think the Right Answer is to get rid of newtype-classes & fix reify, and I’m worried that anything short of that will fail catastrophically at some point. Otherwise, it’s patches on top of patches. I don’t think there is disagreement here, but there is the question about what to do for 8.2.... and unless we’re ready to roll out the new reify, I think the best course of action is to delay the new Typeable and all this Constraint v Type stuff until 8.4. (The new levity polymorphism stuff already committed is hunky-dory.) Richard Simon From: noreply@phabricator.haskell.org<mailto:noreply@phabricator.haskell.org> [mailto:noreply@phabricator.haskell.org] Sent: 31 January 2017 12:51 To: Simon Peyton Jones <simonpj@microsoft.com<mailto:simonpj@microsoft.com>> Subject: [Differential] [Commented On] D2038: [WIP] TysPrim: Generalize kind of (->) goldfire added a comment. View Revision<https://phabricator.haskell.org/D2038> In D2038#89360<https://phabricator.haskell.org/D2038#89360>, @simonpj<https://phabricator.haskell.org/p/simonpj/> wrote: To avoid being able to extract ContraintRep ~R LiftedPtrRep we decided to weaken one of the coercion constructors, the one that gets a kind coercion from a type coercion. We don't need it, and it's awkward here. The problem is that we need it with this patch. I was able to weaken this coercion constructor (KindCo) in my patchD3023<https://phabricator.haskell.org/D3023>, but this patch uses it in a fundamental way that we can't get around. To wit: class C a where meth :: a axC :: (C a :: Constraint) ~R (a :: Type) Now, we wish to cast C a -> a to a -> a.. This cast will look like (->) ?? <LiftedRep> axC <a>. What goes in the??? It's got to be something involving KindCo axC, which is disallowed as per our earlier decision. Therein lies the problem. As for reify: Yes, I'm agreed with that email. But is that implemented yet? Is a design settled on? I don't see a ghc-proposal. Are we wiling to take a dependency on that work in order to get this done? To be clear, my chief worry isn't that these problems cannot be solved by any means -- I'm just worried about the timing of this all and our desire to get 8.2 out the door. REPOSITORY rGHC Glasgow Haskell Compiler REVISION DETAIL https://phabricator.haskell.org/D2038 EMAIL PREFERENCES https://phabricator.haskell.org/settings/panel/emailpreferences/ To: bgamari, goldfire, austin Cc: simonpj, RyanGlScott, thomie _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org<mailto:ghc-devs@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7Cc12ab76d325e4aa0cde508d44a40542a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636215087550191649&sdata=rvOH21xQNco4LLYDg36DkhhPTmpXzQqhEfHKPb%2BqPj8%3D&reserved=0>
On Feb 1, 2017, at 3:34 AM, Simon Peyton Jones <simonpj@microsoft.com> wrote:
Who is acting there. Just Ben? Or are there bits Richard needs to help with?
Ben has done the real heavy lifting, with me opining on this bit or that. From what Ben says, it's very close. There is a small bit of new work to be done to prefer Type over Constraint when solving for Typeable (my step 2), but that can't be hard. If I'm released (for now) from #11715, what's the next priority for me? Richard
Check out https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.2.1 There are several tickets you own in highest or high prio. Notably #12919 (an outright bug). And #12670, #13160, #13202 BEN: yell for whatever help you need with (->) and Typable Simon From: Richard Eisenberg [mailto:rae@cs.brynmawr.edu] Sent: 01 February 2017 13:54 To: Simon Peyton Jones <simonpj@microsoft.com> Cc: ghc-devs@haskell.org Subject: Re: D2038: [WIP] TysPrim: Generalize kind of (->) On Feb 1, 2017, at 3:34 AM, Simon Peyton Jones <simonpj@microsoft.com<mailto:simonpj@microsoft.com>> wrote: Who is acting there. Just Ben? Or are there bits Richard needs to help with? Ben has done the real heavy lifting, with me opining on this bit or that. From what Ben says, it's very close. There is a small bit of new work to be done to prefer Type over Constraint when solving for Typeable (my step 2), but that can't be hard. If I'm released (for now) from #11715, what's the next priority for me? Richard
Simon Peyton Jones via ghc-devs <ghc-devs@haskell.org> writes:
Check out https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.2.1
There are several tickets you own in highest or high prio. Notably #12919 (an outright bug). And #12670, #13160, #13202
BEN: yell for whatever help you need with (->) and Typable
Thanks Simon! I think I probably have it from here. Cheers, - Ben Richard says,
If I'm released (for now) from #11715, what's the next priority for me?
I would say #12919 is the most important. Cheers, - Ben
participants (3)
-
Ben Gamari -
Richard Eisenberg -
Simon Peyton Jones