<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Thank you for those answers! Back to proving again :)<br>
</p>
<div class="moz-cite-prefix">On 23.11.20 04:48, Richard Eisenberg
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:010f0175f33781e8-6bada229-fdb1-46fe-9fb6-029a6178f470-000000@us-east-2.amazonses.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Nov 22, 2020, at 6:49 AM, Jan van Brügge <<a
href="mailto:jan@vanbruegge.de" class=""
moz-do-not-send="true">jan@vanbruegge.de</a>> wrote:</div>
</blockquote>
<blockquote type="cite" class="">
<div class="">
<div class="">
<p class="">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
moz-do-not-send="true"
href="https://github.com/jvanbruegge/isabelle-lambda-calculus"
class="">a complete proof for System F</a> (without
coercions and data types yet). I mainly used the <a
moz-do-not-send="true"
href="https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf"
class="">System Fc paper</a> as reference, ignoring
all the parts about coercions.</p>
<div class=""><br class="">
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
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.<br class="">
<blockquote type="cite" class="">
<div class="">
<div class="">
<p class="">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?</p>
<div class=""><br class="">
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>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.</div>
<br class="">
<blockquote type="cite" class="">
<div class="">
<div class="">
<p class="">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?</p>
<div class=""><br class="">
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
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):</div>
<div><br class="">
</div>
<div>Lemma (Regularity). If G |e- e : s, then G |TY- s : *.</div>
<div><br class="">
</div>
<div>(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.<br class="">
<blockquote type="cite" class="">
<div class="">
<div class="">
<p class="">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 <a moz-do-not-send="true"
href="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"
class="">System Fc pro paper</a> (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?</p>
<div class=""><br class="">
</div>
</div>
</div>
</blockquote>
<div><br class="">
</div>
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.</div>
<div><br class="">
</div>
<div>I would encourage you to take a look also at the proof of
type safety in <a
href="https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf"
class="" moz-do-not-send="true">https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf</a>.
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.</div>
<div><br class="">
</div>
<div>I hope this helps!</div>
<div>Richard<br class="">
<blockquote type="cite" class="">
<div class="">
<div class="">
<p class="">Thank you all<br class="">
Jan<br class="">
</p>
</div>
_______________________________________________<br class="">
ghc-devs mailing list<br class="">
<a href="mailto:ghc-devs@haskell.org" class=""
moz-do-not-send="true">ghc-devs@haskell.org</a><br
class="">
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br
class="">
</div>
</blockquote>
</div>
<br class="">
</blockquote>
</body>
</html>