Help with coercion & roles?

Mon Apr 14 22:04:10 UTC 2014

This explanation-with-example is very helpful. Thanks, Richard! I'll noodle
some more. A fairly simple & robust solution may be to add `Cast` to my
expression GADT.

-- Conal

On Mon, Apr 14, 2014 at 2:02 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> So what do you think? Is there a sound coercion I can build for `co'`?
>
>
> In a word, "no". The problem is that E, as you describe, is a GADT.
> Therefore, it cares exactly which types it is parameterized by. We can see
> this in evidence in the dump, which labels E's second parameter as nominal.
> To draw out the problem, let's look at a simpler example:
>
> > newtype Age = MkAge Int
> > data G a where
> >   MkGInt :: G Int
> >   MkGAge :: G Age
>
> Here, `G` would similarly get a nominal role, because we can't lift
> representational coercions (such as NTCo:Age :: Age ~R Int) through the `G`
> type constructor. If we could, we could then have (MkGAge |> ...) :: G Int,
> which goes against our definition of G -- the only value inhabitant of G
> Int should be MkGInt.
>
> The best you can do here is to try to raise the inner coercion to be
> nominal, by unSubCo_maybe. If that fails, I think you've gone beyond the
> ability of GHC's type system.
>
> Of course, I would like to help you with a way forward -- let me know if
> there's a way I can.
>
> Richard
>
> On Apr 14, 2014, at 4:12 PM, Conal Elliott <conal at conal.net> wrote:
>
> Hi Richard,
>
> I'm working on compiling Haskell to hardware, as outlined at
> https://github.com/conal/lambda-ccc/blob/master/doc/notes.md (with links
> to a few recent blog posts). The first step is to convert Core into other
> Core that evaluates to a reified form, represented as a type-parametrized
> GADT. This GADT (in `LambdaCCC.Lambda`):
>
> > data E :: (* -> *) -> (* -> *) where ...
>
> The parameter is also type-parametrized, and is for the primitives. I have
> such a type designed for hardware generation (in `LambdaCCC.Prim`)
>
> > data Prim :: * -> * where ...
>
> and then the combination of the two:
>
> > type EP = E Prim
>
> So that's what `EP` is.
>
> With `-ddump-tc`, I get
>
> > TYPE CONSTRUCTORS
> >   ...
> >   E :: (* -> *) -> * -> *
> >   data E ($a::* -> *) $b
> >     No C type associated
> >     Roles: [representational, nominal]
> >     RecFlag NonRecursive, Not promotable
> >     = ...
> >   EP :: * -> *
> >   type EP = E Prim
>
> The use of `EP` rather than the more general `E` is only temporary, while
> I'm learning more details of Core (and of HERMIT which I'm using to
> manipulate Core).
>
> I'm now working on reification in the presence of casts. The rule I'm
> trying to implement is
>
> > evalEP e |> co  -->  evalEP (e |> co').
>
> Here, `evalEP :: EP a -> a` and `co :: a ~ b`, so `co' :: EP a ~ EP b`.
>
> I'm trying to build `co'` from `co`, which led to these questions.
>
> So what do you think? Is there a sound coercion I can build for `co'`?
>
> -- Conal
>
>
> On Mon, Apr 14, 2014 at 11:54 AM, Richard Eisenberg <eir at cis.upenn.edu>wrote:
>
>> Hi Conal,
>>
>> In your case, the `_N` on the argument to NTCo:HasIf[0] is correct -- the
>> `HasIf` class indeed has a nominal parameter. So, it seems that this part,
>> at least, is OK.
>>
>> What's the -ddump-tc on EP? Is EP's role nominal? (I think so, given what
>> you're saying.) If that's the case, you won't be able to pass the result of
>> NTCo:HasIf[0] to a coercion built from EP.
>>
>> Popping up a level, what are you trying to do here? If EP's role is
>> indeed nominal, then I don't believe there's a fix here, as the coercion it
>> seems you're trying to build may be unsound. (It looks to me like you want
>> something proving `EP (Bool -> Bool -> Bool -> Bool) ~R EP (HasIf Bool)`,
>> but if EP's role is nominal, then this is indeed bogus.)
>>
>> Richard
>>
>> On Apr 14, 2014, at 2:23 PM, Conal Elliott <conal at conal.net> wrote:
>>
>> Thanks for the pointers! I don't quite know how to get to the form you
>> recommend from the existing coercion, which is `Simple.NTCo:HasIf[0]
>> <GHC.Types.Bool>_N`. (Note the `_N`.) I got that coercion in GHC 7.8.2 from
>> the following code:
>>
>> > class HasIf a where
>> >   ifThenElse :: Bool -> a -> a -> a
>> >
>> > instance HasIf Bool where
>> >   ifThenElse i t e = (i && t) || (not i && e)
>>
>> With `--dump-tc`, I see
>>
>> > TYPE SIGNATURES
>> > TYPE CONSTRUCTORS
>> >   HasIf :: * -> Constraint
>> >   class HasIf a
>> >     Roles: [nominal]
>> >     RecFlag NonRecursive
>> >     ifThenElse :: Bool -> a -> a -> a
>> > COERCION AXIOMS
>> >   axiom Main.NTCo:HasIf :: HasIf a = Bool -> a -> a -> a
>> > INSTANCES
>> >   instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10
>>
>> Do I need to convert the nominal coercion I got from GHC
>> (`Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N` in this case) to a
>> representational one? If so, how?
>> My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to
>> apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which
>> then produces
>>
>> > (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)))_R
>>
>> And still I get "Role incompatibility: expected nominal, got
>> representational in `Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)`".
>>
>> I also tried wrapping `mkSubCo` around the entire coercion (applying
>> `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result:
>>
>> > (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)))_R
>>
>> -- Conal
>>
>>
>>
>> On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg <eir at cis.upenn.edu>wrote:
>>
>>> I agree with Simon, but just `Sub` the `<LambdaCCC.Lambda.EP>_N`, not
>>> the whole coercion.
>>>
>>> There are actually two problems here. The one Simon identified, and also
>>> the fact that Simple.NTCo:HasIf[0] produces a representational coercion.
>>> How do I know? Because of the `NT` -- it's a newtype axiom and must produce
>>> representational coercions. Furthermore, unless the newtype definition is
>>> inferred to require a nominal parameter, the newtype would expect a
>>> representational coercion, not the nominal one you are passing. Check the
>>> dump (using -ddump-tc) of the newtype axiom to be sure.
>>>
>>> Though putting a `Sub` on `<EP>` and changing the Refl constructor on
>>> `<Bool>` would work, you would then be violating an invariant of GHC's
>>> Coercion type: that we prefer `TyConAppCo tc ...` over `AppCo (Refl
>>> (TyConApp tc [])) ...`.
>>>
>>> In sum, here is the coercion I think you want:
>>>
>>> (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_R)))_R
>>>
>>> This is one of the problems with roles -- they are *very* fiddly within
>>> GHC, and it's hard for a non-expert in roles to get them right.
>>>
>>> Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles
>>> and may be of help.
>>>
>>> Let me know if I can help further!
>>> Richard
>>>
>>> On Apr 14, 2014, at 5:45 AM, Simon Peyton Jones <simonpj at microsoft.com>
>>> wrote:
>>>
>>> I think you need a ‘Sub’.
>>>
>>> A cast  (e `cast` g) requires a representational coercion.  I think you
>>> have given it a (stronger) nominal one.  Sub gets from one to t’other.
>>>
>>> Simon
>>>
>>>  *From:* Glasgow-haskell-users [mailto:glasgow-
>>> haskell-users-bounces at haskell.org] *On Behalf Of *Conal Elliott
>>> *Sent:* 14 April 2014 06:00
>>> *To:* ghc-devs at haskell.org; glasgow-haskell-users at haskell.org
>>> *Subject:* Help with coercion & roles?
>>>
>>>
>>> I’m working on a GHC plugin (as part of my Haskell-to-hardware work) and
>>> running into trouble with coercions & roles. Error message from Core Lint:
>>>
>>> Warning: In the expression:
>>>
>>>
>>>
>>>   LambdaCCC.Lambda.lamvP#
>>>
>>>     @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
>>>
>>>     @ (Simple.HasIf GHC.Types.Bool)
>>>
>>>     "tpl"#
>>>
>>>     ((LambdaCCC.Lambda.varP#
>>>
>>>         @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
>>>
>>>         "tpl"#)
>>>
>>>      `cast` (<LambdaCCC.Lambda.EP>_N (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N))
>>>
>>>              ∷ LambdaCCC.Lambda.EP
>>>
>>>                   (GHC.Types.Bool
>>>
>>>                    → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
>>>
>>>                   ~#
>>>
>>>                 LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool)))
>>>
>>>  Role incompatibility: expected nominal, got representational
>>>
>>> in <LambdaCCC.Lambda.EP>_N (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N))
>>>
>>> Do you see anything inconsistent/incompatible in the coercions or roles
>>> above? I constructed the nominal EP Refl coercion, and applied it (AppCo)
>>> an existing coercion of a simpler type.
>>>
>>> Thanks,
>>> -- Conal
>>> _______________________________________________
>>> Glasgow-haskell-users mailing list
>>> Glasgow-haskell-users at haskell.org
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>
>>>
>>>
>>
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140414/e7b2f7e5/attachment-0001.html>