Hi Jan,

On Jul 22, 2019, at 2:49 PM, Jan van Brügge 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 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 http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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