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 <j...@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 <j...@vanbruegge.de> >>> <mailto:j...@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 <j...@vanbruegge.de> <mailto:j...@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>
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs