<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Glad to know you're unstuck.<div class=""><br class=""></div><div class="">If you're trying to follow along with a proof of type safety, I recommend the JFP version of the Coercible paper (<a href="http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1010&context=compsci_pubs" class="">http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1010&context=compsci_pubs</a>). While roles aren't important for you, it's probably the cleanest presentation of the proof. Unfortunately, it doesn't include Type :: Type, but I can't point you to a great proof there. :(</div><div class=""><br class=""></div><div class="">Let me know if you need further assistance. This stuff is hard!</div><div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jul 22, 2019, at 5:23 PM, Jan van Brügge <<a href="mailto:jan@vanbruegge.de" class="">jan@vanbruegge.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class="">
<div text="#000000" bgcolor="#FFFFFF" class=""><p class="">Hi Richard,</p><p class="">> In Core, however (which is where normalise_type works), F
Int and Bool are *not* definitionally equal. Instead, they are
"propositionally equal", which means that they are distinct <br class="">
</p><p class="">Thanks, this was the piece of information that was missing. Now
it makes sense why there is always a coercion returned. The
explanation was really helpful.<br class="">
</p><p class="">> My strong hunch is that you will need a new constructor of
Coercion.</p><p class="">Yeah, I think so too.</p><p class="">> if you're fiddling with Core, you will need to make a Strong
Argument (preferably in the form of a proof) that your changes are
type-safe</p><p class="">Yeah, I know. I wanted to try to adapt the proof once I have <i class="">something
</i>working. No idea how that will work out, I am actually reading
a lot of your papers following the proofs in there, but I have to
read a lot more to be able to do this on my own.<br class="">
</p><p class="">Thanks again for the help, I think I can dig deeper now :)<br class="">
Jan<br class="">
</p>
<div class="moz-cite-prefix">Am 22.07.19 um 21:15 schrieb Richard
Eisenberg:<br class="">
</div>
<blockquote type="cite" cite="mid:6471FF8C-BE89-4158-8639-A99C94BBE2A0@richarde.dev" class="">
<pre class="moz-quote-pre" wrap="">Hi Jan,
</pre>
<blockquote type="cite" class="">
<pre class="moz-quote-pre" wrap="">On Jul 22, 2019, at 2:49 PM, Jan van Brügge <a class="moz-txt-link-rfc2396E" href="mailto:jan@vanbruegge.de"><jan@vanbruegge.de></a> wrote:
This also hints that my code there is
utter garbage, as I already suspected.
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">Sorry, but I'm afraid it is. At least about the coercions.
</pre>
<blockquote type="cite" class="">
<pre class="moz-quote-pre" wrap="">So I guess my actual question is: What does the coercion returned by
normalize_type represent?
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">normalise_type simplifies a type down to one where all type families are evaluated as far as possible. Suppose we have `type instance F Int = Bool`. In Haskell, we use `F Int` and `Bool` interchangeably: we say they are "definitionally equal" in Haskell. By "definitionally equal", I mean that there is no code one could write that can tell the difference between them, and they can be arbitrarily substituted for each other anywhere.
In Core, however (which is where normalise_type works), F Int and Bool are *not* definitionally equal. Instead, they are "propositionally equal", which means that they are distinct, but if we have something of type F Int, we can produce something of type Bool without any runtime action. A cast does this conversion. If you look at the Expr type (in CoreSyn), you'll see `Cast :: Expr -> Coercion -> Expr` (somewhat simplified). A cast (sometimes written `e |> co`) changes the type of an expression. It has typing rule
e : ty1
co : ty1 ~ ty2
-------------------
e |> co : ty2
That is, if expression e has type ty1 and a coercion co has type ty1 ~ ty2, then e |> co has type ty2. Casts are erased later on in the compilation pipeline.
Propositional equality in Core has two sub-varieties: nominal equality and representational equality. Only nominal equality is in play here, and so we can basically ignore this distinction here.
The definitional equality of type family reduction in Haskell is compiled into nominal propositional equality in Core. So everywhere the compiler has to replace F Int with Bool during compilation, a cast (or other construct) is introduced in Core.
normalise_type performs type family reductions, and it returns a coercion that witnesses the equality between its input type and its output type. The flattener does the same.
So the real question is: suppose I have a RowType ty1 that mentions F Int. Normalizing will get me a RowType ty2 that mentions Bool in place of F Int. How can I get a coercion of type ty1 ~ ty2? You have to answer that question to be able to complete this clause of normalise_type.
My strong hunch is that you will need a new constructor of Coercion. Note that most type forms have corresponding Coercion forms. So you will probably need a RowCo. The relationship between RowType and RowCo will be very like the one between AppTy and AppCo, so you can use that as a guide, perhaps.
Also, I hate to say it, but if you're fiddling with Core, you will need to make a Strong Argument (preferably in the form of a proof) that your changes are type-safe. That is, the new Core language needs to respect the Progress and Preservation theorems. Fiddling with Core is not to be done lightly.
I hope this helps!
Richard
</pre>
<blockquote type="cite" class="">
<pre class="moz-quote-pre" wrap="">Same with flatten_one in TcFlatten.hs. I have
problems visualizing what is going on there and what is expected of me
to do with the returned coercion from a recursive call.
Cheers,
Jan
Am 22.07.19 um 15:58 schrieb Ben Gamari:
</pre>
<blockquote type="cite" class="">
<pre class="moz-quote-pre" wrap="">Jan van Brügge <a class="moz-txt-link-rfc2396E" href="mailto:jan@vanbruegge.de"><jan@vanbruegge.de></a> writes:
</pre>
<blockquote type="cite" class="">
<pre class="moz-quote-pre" wrap="">Hi,
currently I have some problems understanding how the coercions are
threaded through the compiler. In particular the function
`normalise_type`. With guessing and looking at the other cases, I came
to this solution, but I have no idea if I am on the right track:
normalise_type ty
= go ty
where
go (RowTy k v flds)
= do { (co_k, nty_k) <- go k
; (co_v, nty_v) <- go v
; let (a, b) = unzip flds
; (co_a, ntys_a) <- foldM foldCo (co_k, []) a
; (co_b, ntys_b) <- foldM foldCo (co_v, []) b
; return (co_a `mkTransCo` co_b, mkRowTy nty_k nty_v $ zip
ntys_a ntys_b) }
where
foldCo (co, tys) t = go t >>= \(c, nt) -> return (co
`mkTransCo` c, nt:tys)
RowTy has type Type -> Type -> [(Type, Type)]
What I am not sure at all is how to treat the coecions. From looking at
the go_app_tys code I guessed that I can just combine them like that,
but what does that mean from a semantic standpoint? The core spec was
not that helpful either in that regard.
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">Perhaps others are quicker than me but I'll admit I'm having a hard time
following this. What is the specification for normalise_type's desired
behavior? What equality is the coercion you are trying to build supposed
to witness?
In short, TransCo (short for "transitivity") represents a "chain" of
coercions. That is, if I have,
co1 :: a ~ b
co2 :: b ~ c
then I can construct
co3 :: a ~ c
co3 = TransCo co1 co2
Does this help?
Cheers,
- Ben
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap="">_______________________________________________
ghc-devs mailing list
<a class="moz-txt-link-abbreviated" href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a>
</pre>
</blockquote>
<pre class="moz-quote-pre" wrap=""></pre>
</blockquote>
</div>
</div></blockquote></div><br class=""></div></body></html>