How do Coercions work
Richard Eisenberg
rae at richarde.dev
Mon Jul 22 21:32:45 UTC 2019
Glad to know you're unstuck.
If you're trying to follow along with a proof of type safety, I recommend the JFP version of the Coercible paper (http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1010&context=compsci_pubs <http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1010&context=compsci_pubs>). 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. :(
Let me know if you need further assistance. This stuff is hard!
Richard
> On Jul 22, 2019, at 5:23 PM, Jan van Brügge <jan at vanbruegge.de> wrote:
>
> 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> <mailto: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> <mailto: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 <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/20190722/915b7c5e/attachment.html>
More information about the ghc-devs
mailing list