D2038: [WIP] TysPrim: Generalize kind of (->)

Wed Feb 1 01:19:08 UTC 2017

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 at cs.brynmawr.edu> wrote:
> 
>> 
>> On Jan 31, 2017, at 5:41 PM, Simon Peyton Jones <simonpj at microsoft.com <mailto:simonpj at 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 at phabricator.haskell.org <mailto:noreply at phabricator.haskell.org> [mailto:noreply at phabricator.haskell.org <mailto:noreply at phabricator.haskell.org>] 
>> Sent: 31 January 2017 12:51
>> To: Simon Peyton Jones <simonpj at microsoft.com <mailto:simonpj at 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 at haskell.org <mailto:ghc-devs at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs <http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170131/ce52ce26/attachment-0001.html>