<div dir="ltr">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.<br><br>-- Conal </div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Mon, Apr 14, 2014 at 2:02 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word"><div class=""><div><blockquote type="cite"><div dir="ltr">So what do you think? Is there a sound coercion I can build for `co'`?<br></div></blockquote></div><div><br></div></div><div>
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:</div>
<div><br></div><div>> newtype Age = MkAge Int</div><div>> data G a where</div><div>> MkGInt :: G Int</div><div>> MkGAge :: G Age</div><div><br></div><div>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.</div>
<div><br></div><div>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.</div><div><br></div>
<div>
Of course, I would like to help you with a way forward -- let me know if there's a way I can.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Richard</div></font></span><div><div class="h5"><br><div>
<div>On Apr 14, 2014, at 4:12 PM, Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>> wrote:</div><br><blockquote type="cite"><div dir="ltr"><div>Hi Richard,<br><br>I'm working on compiling Haskell to hardware, as outlined at <a href="https://github.com/conal/lambda-ccc/blob/master/doc/notes.md" target="_blank">https://github.com/conal/lambda-ccc/blob/master/doc/notes.md</a> (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`):<br>
<br>> data E :: (* -> *) -> (* -> *) where ...<br><br>The parameter is also type-parametrized, and is for the primitives. I have such a type designed for hardware generation (in `LambdaCCC.Prim`)<br><br>> data Prim :: * -> * where ...<br>
<br>and then the combination of the two:<br><br>> type EP = E Prim<br><br>So that's what `EP` is.<br><br>With `-ddump-tc`, I get<br><br>> TYPE CONSTRUCTORS<br>> ...<br>> E :: (* -> *) -> * -> *<br>
> data E ($a::* -> *) $b<br>> No C type associated<br>> Roles: [representational, nominal]<br>> RecFlag NonRecursive, Not promotable<br>> = ...<br>> EP :: * -> *<br>> type EP = E Prim<br>
<br>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).<br><br>I'm now working on reification in the presence of casts. The rule I'm trying to implement is<br>
<br>> evalEP e |> co --> evalEP (e |> co').<br><br>Here, `evalEP :: EP a -> a` and `co :: a ~ b`, so `co' :: EP a ~ EP b`.<br><br>I'm trying to build `co'` from `co`, which led to these questions.<br>
<br>So what do you think? Is there a sound coercion I can build for `co'`?<br><br></div>-- Conal<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Apr 14, 2014 at 11:54 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>Hi Conal,</div><div><br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div>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.)</div>
<span><font color="#888888"><div><br></div><div>Richard</div></font></span><div><div><div><br></div><div><div>On Apr 14, 2014, at 2:23 PM, Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>> wrote:</div>
<br><blockquote type="cite"><div dir="ltr"><div><blockquote>
</blockquote>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:<br>
<br>> class HasIf a where<br>> ifThenElse :: Bool -> a -> a -> a<br>><br>> instance HasIf Bool where<br>> ifThenElse i t e = (i && t) || (not i && e)<br><br>With `--dump-tc`, I see<br>
<br>> TYPE SIGNATURES<br>> TYPE CONSTRUCTORS<br>> HasIf :: * -> Constraint<br>> class HasIf a<br>> Roles: [nominal]<br>> RecFlag NonRecursive<br>> ifThenElse :: Bool -> a -> a -> a<br>
> COERCION AXIOMS<br>> axiom Main.NTCo:HasIf :: HasIf a = Bool -> a -> a -> a<br>> INSTANCES<br>> instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10<br><br>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?<br>
My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then produces<br><br>> (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)))_R<br>
<br>And still I get "Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)`".<br><br>I also tried wrapping `mkSubCo` around the entire coercion (applying `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result:<br>
<br>> (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)))_R<br><br></div>-- Conal<br><div><blockquote>
</blockquote></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>I agree with Simon, but just `Sub` the `<LambdaCCC.Lambda.EP>_N`, not the whole coercion.</div>
<div><br></div><div>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.</div>
<div><br></div><div>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 [])) ...`.</div>
<div><br></div><div>In sum, here is the coercion I think you want:</div><div><br></div><div>(LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_R)))_R</div><div><br></div><div>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.</div>
<div><br></div><div>Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles and may be of help.</div><div><br></div><div>Let me know if I can help further!</div><div>Richard</div><br><div><div>
<div>On Apr 14, 2014, at 5:45 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>> wrote:</div><br></div><blockquote type="cite"><div link="#0563C1" vlink="#954F72" style="font-family:Helvetica;font-size:medium;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:-webkit-auto;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px" lang="EN-GB">
<div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)">I think you need a ‘Sub’.<u></u><u></u></span></div>
<div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)"> </span></div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif">
<span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)">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.<u></u><u></u></span></div>
<div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)"> </span></div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif">
<span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)">Simon<u></u><u></u></span></div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><span style="font-family:Calibri,sans-serif;color:rgb(31,73,125)"> </span></div>
<div style="border-style:none none none solid;border-left-width:1.5pt;border-left-color:blue;padding:0cm 0cm 0cm 4pt"><div><div style="border-style:solid none none;border-top-width:1pt;border-top-color:rgb(225,225,225);padding:3pt 0cm 0cm">
<div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><b><span style="font-size:11pt;font-family:Calibri,sans-serif" lang="EN-US">From:</span></b><span style="font-size:11pt;font-family:Calibri,sans-serif" lang="EN-US"><span> </span>Glasgow-haskell-users [mailto:<a href="mailto:glasgow-" target="_blank">glasgow-</a><a href="mailto:haskell-users-bounces@haskell.org" target="_blank">haskell-users-bounces@haskell.org</a>]<span> </span><b>On Behalf Of<span> </span></b>Conal Elliott<br>
<b>Sent:</b><span> </span>14 April 2014 06:00<br><b>To:</b><span> </span><a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a>; <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.org</a><br>
<b>Subject:</b><span> </span>Help with coercion & roles?<u></u><u></u></span></div></div></div><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif"><u></u> <u></u></div><div>
<p class="MsoNormal" style="margin:0cm 0cm 6pt;font-size:12pt;font-family:'Times New Roman',serif">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:<u></u><u></u></p>
<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'">Warning: In the expression:<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'"> </code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> LambdaCCC.Lambda.lamvP#<u></u><u></u></code></pre>
<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)<u></u><u></u></code></pre>
<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> @ (Simple.HasIf GHC.Types.Bool)<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'"> "tpl"#<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> ((LambdaCCC.Lambda.varP#<u></u><u></u></code></pre>
<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)<u></u><u></u></code></pre>
<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> "tpl"#)<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'"> `cast` (<LambdaCCC.Lambda.EP>_N (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N))<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'"> </code><code style="font-family:'Courier New'"><span style="font-family:'Cambria Math',serif">∷</span> LambdaCCC.Lambda.EP<u></u><u></u></code></pre>
<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> (GHC.Types.Bool<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'"> → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'"> ~#<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool)))<u></u><u></u></code></pre>
<pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'"><code style="font-family:'Courier New'"> <u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">Role incompatibility: expected nominal, got representational<u></u><u></u></code></pre><pre style="margin:0cm 0cm 0.0001pt 30pt;font-size:10pt;font-family:'Courier New'">
<code style="font-family:'Courier New'">in <LambdaCCC.Lambda.EP>_N (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N))</code><u></u><u></u></pre><p style="margin-right:0cm;margin-left:0cm;font-size:12pt;font-family:'Times New Roman',serif">
Do you see anything inconsistent/incompatible in the coercions or roles above? I constructed the nominal<span> </span><code style="font-family:'Courier New'"><span style="font-size:10pt">EP</span></code><span> </span><code style="font-family:'Courier New'"><span style="font-size:10pt">Refl</span></code><span> </span>coercion, and applied it (<code style="font-family:'Courier New'"><span style="font-size:10pt">AppCo</span></code>) an existing coercion of a simpler type.<u></u><u></u></p>
<p style="margin-right:0cm;margin-left:0cm;font-size:12pt;font-family:'Times New Roman',serif">Thanks,<u></u><u></u></p><div style="margin:0cm 0cm 0.0001pt;font-size:12pt;font-family:'Times New Roman',serif">
-- Conal<u></u><u></u></div></div></div></div>_______________________________________________<br>Glasgow-haskell-users mailing list<br><a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a></div></blockquote></div><br></div></blockquote></div><br></div>
</blockquote></div><br></div></div></div></blockquote></div><br></div>
</blockquote></div><br></div></div></div></blockquote></div><br></div>