Re: How do Coercions work

22 Jul 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  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  mailto:jan@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  mailto:jan@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@haskell.org mailto:ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs