Questions about System F and data types

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

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 (without coercions and data types yet). I mainly used the System Fc paper 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 (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


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Questions about System F and data types

Richard Eisenberg-5


On Nov 22, 2020, at 6:49 AM, Jan van Brügge <[hidden email]> 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 (without coercions and data types yet). I mainly used the System Fc paper 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 (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. 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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 (without coercions and data types yet). I mainly used the System Fc paper 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 (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. 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs