Thank you for those answers! Back to proving again :)
On 23.11.20 04:48, Richard Eisenberg wrote: > > >> On Nov 22, 2020, at 6:49 AM, Jan van Brügge <[email protected] >> <mailto:[email protected]>> wrote: >> >> To better understand PL papers, especially those involving System Fc >> and its extensions, I started to write a formal proof of type safety >> including alpha-equivalence. Currently I have a complete proof for >> System F <https://github.com/jvanbruegge/isabelle-lambda-calculus> >> (without coercions and data types yet). I mainly used the System Fc >> paper >> <https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf> >> as reference, ignoring all the parts about coercions. >> >> > > I'm not an author of that paper (and, somewhat surprisingly, have > never taken a very deep dive into it). But I can try to answer your > questions. >> >> 1. In the Fc paper, the rule `AppT` has a judgement delta as >> assumption, which does not exist. I assumed the `ty` judgement was >> meant there by looking at the arguments. Is this correct? >> >> > > In the grammar figure (Fig. 1), we see that \delta is either TY or CO. > Both the TY and CO judgments are included in Fig. 2. So, in effect, > you're assumption is correct, but the rule covers also coercion > application, as well as type application. > >> 2. In the `Abs` rule, the type of the variable is required to be >> valid and of kind star by the judgement `ty`. In the `Let` rule, this >> assumption is missing. I tried it like that, but was not able to >> complete the proofs. Is such an assumption missing there or should I >> be able to proof it without? >> >> > > I don't think Let is missing a premise. However, I do think the paper > should explicitly state the following lemma (which I believe is true > of this system): > > Lemma (Regularity). If G |e- e : s, then G |TY- s : *. > > (You might also need to assert that the size of the resulting > derivation is strictly smaller than the input -- not sure if your > application would need that to power an induction hypothesis.) With > that lemma, you could essentially recreate the premise you were hoping > to spot on Let. >> >> 3. In the Fc paper, the types and kinds of datatype declarations are >> added to the context with a separate judgement that interprets the >> datatype declarations. In the System Fc pro paper >> <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/p53-yorgey.pdf?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople%2Fsimonpj%2Fpapers%2Fext-f%2Fpromotion.pdf> >> (from what I can tell) those types and kinds are assumed to be >> already part of the initial context. At the moment I prove progress >> against the empty context, so I guess I would have to relax that to >> an initial context that only contains types and kinds of type >> constants and nothing else. Is that correct? What is here the "best >> practice" in terms of PL research? >> >> > > The important thing in a progress proof is that there are no term > variables in the context. But types and kinds are all OK. Different > authors take different approaches. Some authors define what's called a > *signatures* (frequently written with a \Sigma) that contains > type/kind definitions (only). All judgments are then parameterized > over both a signature and a typing context. Other authors allow the > context to contain all kinds of assumptions, but then state that the > context in the progress theorem has no term-variable bindings. I don't > think one approach is necessarily better than another. > > I would encourage you to take a look also at the proof of type safety > in https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf > <https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf>. > That paper is concerned with roles (which, presumably, you are not), > but the proof is (to my knowledge) the most careful proof presented > about System FC. Other papers since have mechanized parts of the > proof, but those work with a variant of FC that is dependently typed. > > I hope this helps! > Richard >> >> Thank you all >> Jan >> >> _______________________________________________ >> ghc-devs mailing list >> [email protected] <mailto:[email protected]> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
