Questions about System F and data types

[Jan van Brügge]

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 <jan at vanbruegge.de
>> <mailto:jan at vanbruegge.de>> 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
>> ghc-devs at haskell.org <mailto:ghc-devs at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20201124/2ad96166/attachment.html>