Questions about System F and data types

[Jan van Brügge]

Hi,

I know that this is probably not the correct place to ask as my question
is not directly related to GHC itself, but I thought here are the people
that can most likely answer this.

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.

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?

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?

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?

Thank you all
Jan

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20201122/61ee0a06/attachment.html>