How do Coercions work

[Jan van Brügge]

Hi Richard,

>  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

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.

> My strong hunch is that you will need a new constructor of Coercion.

Yeah, I think so too.

> 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

Yeah, I know. I wanted to try to adapt the proof once I have /something
/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.

Thanks again for the help, I think I can dig deeper now :)
Jan

Am 22.07.19 um 21:15 schrieb Richard Eisenberg:
> Hi Jan,
>
>> On Jul 22, 2019, at 2:49 PM, Jan van Brügge <jan at vanbruegge.de> wrote:
>>
>>  This also hints that my code there is
>> utter garbage, as I already suspected.
> Sorry, but I'm afraid it is. At least about the coercions.
>
>> So I guess my actual question is: What does the coercion returned by
>> normalize_type represent?
> 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
>
>> 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:
>>> Jan van Brügge <jan at vanbruegge.de> writes:
>>>
>>>> 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.
>>>>
>>> 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
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> 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/20190722/3fbb3da9/attachment.html>