Stream: Miscellaneous

Topic: Progress and preservation proofs for dependent types


view this post on Zulip walker (Oct 03 2022 at 15:55):

I am trying to formalize preservation proofs for dependent type lambda calculus in Coq, and I am stuck at the preservation proof, I wanted to know if there is already public resouces (paper/.v files) on how to do deal wit the tricks

I will try to describe where I am stuck

Γ is used to represent global variables declarations (variable & type), while the Ψ is for local variables (I separated between them in my implementation) and Δ is used for global variable definition (variable and content) The reason for the separation is that I have global variables as well and they are represented as strings.

The typing rule (part of it) looks like this

Inductive SyntaticallyTypes: stringmap Term -> gmap nat Term -> Term -> Term -> Prop :=
| SyntaticallyTypes_pi: forall Γ Ψ A B l (L: gset nat),
        Γ, Ψ  A: univ l ->
        (forall x, x  L -> Γ, Ψ  {[ x := A ]}  open B (fvar x) : univ l ) ->
        Γ, Ψ  pi A B : univ l
| SyntaticallyTypes_lam: forall Γ Ψ A y B l (L: gset nat),
        Γ, Ψ  A: univ l ->
        (forall x, x  L -> Γ, Ψ  {[ x := A ]}  open y (fvar x) : open B (fvar x) ) ->
        Γ, Ψ  lam A y : pi A B
| SyntaticallyTypes_appl: forall Γ Ψ A B m n,
            Γ, Ψ  m : pi A B ->
            Γ, Ψ  n : A ->
            Γ, Ψ  appl m n : open B n
where "Γ ',' Ψ '⊢' t : T" := (SyntaticallyTypes Γ Ψ t T).

The main difference is the part where we say Γ, Ψ ⊢ appl m n : open B n we just don't type function application as return value:

Then there is the stepping rules:

Reserved Notation "Δ '⊢' t '--->' t'" (at level 20).
Inductive Step: stringmap Term -> Term -> Term -> Prop :=
| Step_appl: forall (Δ: stringmap Term) (T y m: Term),
                    Δ  (lam T y) ->
                    Δ  m ->
                    Δ  (appl (lam T y) m) ---> (open y m)
| Step_appl_left: forall (Δ: stringmap Term) (f f' m: Term),
                    LC m ->
                    Δ  f ---> f' ->
                    Δ  (appl f m) ---> (appl f' m)
| Step_appl_right: forall (Δ: stringmap Term) (f m m': Term),
                    LC m ->
                    Δ  f ->
                    Δ  m ---> m' ->
                    Δ  (appl f m) ---> (appl f m')
where "Δ '⊢' t '--->' t'" := (Step Δ t t').

LC is for locally closed terms, and Δ ↛ f means f is value (or if it is global variable than the data stored in Δ is also a value

Here is where I am stuck

H': Δ  appl m n ---> t'
------------------------------
Goal: Γ,   t' : open B n

I would just invert H' to get the three cases of application. First case (Γ, ∅ ⊢ open y n : open B n) is solved by substitution lemma,

Second case is trivial,

The problem is with Step_appl_right case:

The goal is to solve he following

H7: Δ  n ---> m'
-----------------------
Γ,   appl m m' : open B n

substitution lemma, and transitivity of Typing assumes that m' and n are the same, If I don't do so, I end up creating a more complex version of the preservation lemma itself.

I can share additional information as needed, but I wanted to avoid copy pasting the whole implementation here, and thought it might be better to put effort into explaining the problem.

view this post on Zulip walker (Oct 03 2022 at 15:57):

P.S, I think it might be important to mention that I am doing the cofinite quantifications and nameless representations from enginering formal metatheory paper, this case I am stuck at is one of the core differences between dependent lambda calculus and normal typed lambda calculus.

view this post on Zulip walker (Oct 03 2022 at 15:57):

also I can share the transitivity and substitution lemma (transitivitiy implmented, substitution admitted).

view this post on Zulip walker (Oct 03 2022 at 15:58):

Lemma trans_SyntaticallyTypes: forall Γ Ψ A B a f,
    Γ, Ψ  f : pi A B ->
    Γ, Ψ  a: A ->
    Γ, Ψ  appl f a : open B a.

Lemma substitution_lemma: forall Γ Ψ A B a y,
    Γ, Ψ  lam A y : pi A B ->
    Γ, Ψ  a: A ->
    Γ, Ψ  open y a : open B a.

view this post on Zulip Karl Palmskog (Oct 03 2022 at 16:04):

I think a lot of the stuff from the Engineering Formal Metatheory paper is now maintained here: https://github.com/plclub

Specifically: https://github.com/plclub/metalib

view this post on Zulip walker (Oct 03 2022 at 16:07):

yes, that is true, and I am following their tutorial but without the library, but that is not the current problem, my problem is unfornately with the one thing they don't show how to do :(

view this post on Zulip walker (Oct 03 2022 at 16:24):

I realized that I wrote lots of stuff, so let me summarize, i am stuck trying to prove preservation for f x where f is lambda abstraction with arbitrary pi type.

view this post on Zulip Li-yao (Oct 03 2022 at 16:31):

That doesn't seem provable with only that one typing rule for application. You should either weaken the preservation theorem to allow the type to change through reduction, or add that flexibility in typing rules to allow types in typing derivations to differ up to convertibility.

view this post on Zulip walker (Oct 03 2022 at 16:34):

I am listening, does this have a name or is it described somewhere?

view this post on Zulip walker (Oct 03 2022 at 16:35):

most text book formalization only offers one application rule, so I assumed this is the way to go.

view this post on Zulip walker (Oct 03 2022 at 16:37):

I am worried that If I did it the way you described, that will be just just cheating the system.

view this post on Zulip Li-yao (Oct 03 2022 at 16:37):

The second option I mentioned is to add a "conversion rule", for example there's one in this paper (Figure 3, rule E-Conv) https://dl.acm.org/doi/pdf/10.1145/3110275

view this post on Zulip walker (Oct 03 2022 at 16:38):

thank you so much! I will read it and hopefully breakthought his issue.

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:41):

I don't know the terminology for dependent types, but analogy with subtyping would give standard names to @Li-yao 's suggestions: adding conversion gives a declarative type system, while embedding conversion in the application rule gives an algorithmic type system.

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:42):

(and I don't know if you need conversion just in application)

view this post on Zulip walker (Oct 03 2022 at 19:48):

I am not sure I understand what that means "adding conversion gives a declarative type system, while embedding conversion in the application rule gives an algorithmic type system."

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:49):

TAPL explains the distinction for subtyping in chapter 16 or 17, I forget... but TLDR:

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:50):

rules for STLC are syntax-directed — from the term you know which typing rule could apply

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:50):

even more strongly, each term constructor has only one typing rule

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:52):

Therefore, writing a typechecker is pretty mechanic. If this is the case, we call the type system "algorithmic". However, the conversion rule is not like that!

view this post on Zulip walker (Oct 03 2022 at 19:53):

I see, all those details are glossed over in most lecture materials.

view this post on Zulip walker (Oct 03 2022 at 19:54):

It is funny because I thought conversion rule is something deducable :(

view this post on Zulip walker (Oct 03 2022 at 19:54):

anyways thanks a lot for explaination and pointing to the book,

view this post on Zulip walker (Oct 03 2022 at 19:57):

one last question:

if we add or embed the type conversion rule, that is basically saying that type conversion is our denominational equality, right ?

view this post on Zulip walker (Oct 03 2022 at 19:58):

The rule I had in mind looked like something like this as an addition to the typing rules (or embedding it in every rule):

| SyntaticallyTypes_conv: forall Γ Ψ t T T',
            Γ, Ψ  t: T ->
            (forall Δ, Δ  T --->* T') -> (*T can be reduced to T' via zero or more steps *)
            Γ, Ψ  t: T'

view this post on Zulip walker (Oct 03 2022 at 19:59):

also never mind the Δ ⊢ part, that is the global definitions. but you get the idea.

view this post on Zulip walker (Oct 03 2022 at 20:00):

so this rule basically says --->* is our equality, right ?

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 21:33):

it seems you're looking at material on simply-typed lambda calculus — extending to dependent types is _not_ an exercise for the reader

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 21:35):

It is funny because I thought conversion rule is something deducable :(

conversion _is_ decidable, the question is when to use it. One can rephrase things to "embed" conversion only where needed, that is in elimination rules — in your case, in SyntaticallyTypes_appl you'd replace Γ, Ψ ⊢ m : pi A B with Γ, Ψ ⊢ m : T and T ~= pi A B

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 21:36):

s/denominational equality/definitional equality/, but yes

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 21:37):

re Δ ⊢ T --->* T', I don't think that's enough. You need T and T' to be convertible, but that might require reduction in either direction. And in modern formulations of dependent types, convertibility is not restricted to reduction

view this post on Zulip Pierre-Marie Pédrot (Oct 03 2022 at 21:40):

Even without dependent types, you may need arbitrary equational reasoning (e.g. for Fω that's already the case)

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 21:40):

also not an exercise for the reader from STLC — chapters 11 vs 3X in TAPL

view this post on Zulip walker (Oct 03 2022 at 22:05):

yes I admit, I underestimated, how complex it is, and thought it is an exercise to just free style it.

view this post on Zulip walker (Oct 03 2022 at 22:06):

pi types + universes look deceivingly simple, I thought I can do it in a week.

view this post on Zulip walker (Oct 03 2022 at 22:07):

I will look at book description of the language and try to follow it.

view this post on Zulip Meven Lennon-Bertrand (Oct 04 2022 at 12:33):

I do not know if you are aware of it, but you might want to look at MetaCoq which does this kind of things for a realistic type system (as close as possible to Coq's). Although quite some difficulties come from "advanced" Coq features (patterrn-matching, complicated universes, etc.), even for the "λ-Π-universes" fragment preservation is not trivial. In particular, you need to show what is usually called injectivity of product types with respect to conversion, which requires a non-trivial proof (MetaCoq uses that conversion can be characterized in term of reduction, and that said reduction is confluent). For paper details on this, you can go look at this paper.

view this post on Zulip Meven Lennon-Bertrand (Oct 04 2022 at 12:35):

Regarding algorithmic vs declarative type system, this is also something we encountered in this project, and we actually have both kinds of systems around. But, again, showing their equivalence is not trivial. For more on this, you might want to give a look at my PhD thesis, which talks quite a lot about these issues :)

view this post on Zulip Karl Palmskog (Oct 04 2022 at 13:10):

aren't there all these (machine-checked) formalizations of "pure type systems" as well? aren't they also close to these kinds of calculi?

view this post on Zulip Meven Lennon-Bertrand (Oct 04 2022 at 13:14):

Yes, indeed, the fragment we are talking about looks a lot like a PTS (maybe with added constants, but these do not change too much), and most of these questions have been studied in that setting a while ago. I can't give the relevant citations on the top of my head, though…

view this post on Zulip Meven Lennon-Bertrand (Oct 04 2022 at 13:17):

But imho PTS formulations tend to be oldish, meaning some things are harder than they should be, making it sometimes difficult to distinguish between what is actually a hard question and will only become harder in more complex systems, and what is mostly a presentation issue.

view this post on Zulip Karl Palmskog (Oct 04 2022 at 13:20):

if we believe Larry Paulson, a lot of type theory was basically motivated by presentational issues: https://lawrencecpaulson.github.io/2022/03/16/Types_vs_Sets.html

types are syntax, not semantics.

A view from I tend to think of the syntactic rules of type theory as giving a “presentation of an algebraic theory”.

view this post on Zulip Meven Lennon-Bertrand (Oct 04 2022 at 13:27):

Yes, indeed, and this is precisely my critic of PTS: they got some things right, but I think we now know how to do better presentations (of very similar systems)

view this post on Zulip walker (Oct 04 2022 at 14:49):

@Meven Lennon-Bertrand I think your phd thesis is the thing I was literally looking for, and the idea to check how metacoq do it, thanks a lot!

view this post on Zulip Meven Lennon-Bertrand (Oct 04 2022 at 14:49):

Hope you have a nice read, then :) Don't hesitate to ask if you have questions!

view this post on Zulip walker (Oct 04 2022 at 14:52):

I have one actually, do you think it is good idea to implement the type system the way you describe it in the phd ? or is there a better approach to tackle this problem ?

view this post on Zulip Meven Lennon-Bertrand (Oct 04 2022 at 15:01):

I'm not sure I get what you mean: what "implementation" are you talking about?

view this post on Zulip Karl Palmskog (Oct 04 2022 at 15:14):

from above, I think the intended meaning of "implement" is: make a deep embedding of the system in a proof assistant and prove its metatheory correct there

view this post on Zulip Karl Palmskog (Oct 04 2022 at 15:15):

in the PhD thesis, I presume a number of results are already formalized/"implemented" as part of MetaCoq on GitHub

view this post on Zulip Meven Lennon-Bertrand (Oct 04 2022 at 15:17):

If this is the question, yes indeed, many parts of the PhD are not only formalized in MetaCoq, but needed to complete the proof of completeness of the implemented type-checker that is part of the project. I give an overview of this in the second part.

view this post on Zulip walker (Oct 04 2022 at 17:51):

Yes this partially the qeustion, but then I am interested in useful extraction, that is a problem for another day.

view this post on Zulip walker (Oct 04 2022 at 17:52):

thanks a lot everyone for clarifications. I will use the thesis as my main guide when impelementing the dependent parts of my language.

view this post on Zulip Meven Lennon-Bertrand (Oct 05 2022 at 08:30):

walker said:

Yes this partially the qeustion, but then I am interested in useful extraction, that is a problem for another day.

The aim of our type-checker is to yield a reasonable program when erased, so in that sense, yes. However, the main point is that I present bidirectional/algorithmic typing as an inductive relation, which it does not make much sense to extract. Only after the fact do we write a type-checker, which is proven correct wrt. the inductive relation (and this is much easier than with respect to the declarative presentation, because even when described as a relation the algorithmic presentation is closer to the implementation).

view this post on Zulip Paolo Giarrusso (Oct 05 2022 at 10:10):

Is the topic extracting the typechecker or the actual programs? From past discussions with @walker I thought the latter, but I'm not sure

view this post on Zulip walker (Oct 05 2022 at 11:15):

So What I am trying to do is designing an optimizing compiler that incorporates features from dependently typed programming languaes and CSL.

view this post on Zulip walker (Oct 05 2022 at 11:15):

Compiler that people can trust to be type safe

view this post on Zulip walker (Oct 05 2022 at 11:15):

So first I need to prove meta theoritic properties about the type system of that compiler.

view this post on Zulip walker (Oct 05 2022 at 11:16):

Then I apparently need to extract the type system so I can build the rest of the compiler around it.

view this post on Zulip walker (Oct 05 2022 at 11:17):

The type system I was trying to design was not the real langage type system but basically a dependently typed intermediate representation.

view this post on Zulip walker (Oct 05 2022 at 11:18):

That meant it doesn't have to be easy to use, or comes with inference rules or anything fancy, it just have to have all the needed features without necessarily the needed convenience.

view this post on Zulip walker (Oct 05 2022 at 12:06):

That is not to say I assumed the representation used for proofs will be suitable for extraction. I wanted to make sure that the system in question is decidable, thus I can write something that can be extracted and prove that the two implementations are equivalent.

view this post on Zulip Michael Soegtrop (Oct 05 2022 at 12:43):

@walker : are you aware of CertiCoq and/or rupicola?

As far as I understand both can't handle all of Gallina and CertiCoq (again afaik) more focusses on completeness while Rupicola focusses on generating very high performance code for a small application domain and making this domain easy to extend. Also both have different backends (CompCert for CertiCoq vs. Bedrock2 for Rupicola (afaik)).

Do I understand your project correctly that you want to design a language similar to Gallina, for which you want to create a complete compiler certified in Coq? What are your plans for the backend?

view this post on Zulip walker (Oct 05 2022 at 13:17):

My plan for the backend was using cranelift.

view this post on Zulip walker (Oct 05 2022 at 13:18):

https://github.com/bytecodealliance/wasmtime/tree/main/cranelift

view this post on Zulip walker (Oct 05 2022 at 13:19):

It is not publically advertised yet, but I know that they have workgroups trying to formally verify that cranelift SSA to assembly preserve semantics.

view this post on Zulip walker (Oct 05 2022 at 13:19):

I would hope that this stage will be complete by the time I need it.

view this post on Zulip walker (Oct 05 2022 at 13:21):

but it is good to know that there is a thing called bedrock2 and the project's goal!

view this post on Zulip walker (Oct 05 2022 at 13:22):

but yes I want to create something like gallina ... only if gallina had side effects and resource managements ... I know this sounds too insane and too ambitious but this is goal, and we will see how much complexity will I get in the way.

view this post on Zulip walker (Oct 05 2022 at 13:24):

and the good thing I don't have to restrict myself to gallina, since I am doing it from scratch. and now that projects like metacoq, certicoq, rupicola exist, I might have to borrow the techniques they used to engineer the proofs.

view this post on Zulip walker (Oct 05 2022 at 13:25):

I wish I could say "I know this is not as easy as it sounds," but then it doesn't sound easy to start with anyways ....

view this post on Zulip Michael Soegtrop (Oct 05 2022 at 13:52):

Thanks for sharing the details!

I would not bet on that cranelift has ready to use Coq specs and proofs in some near future. But I guess the backend decisions are quite a bit in the future for you, and there is no need to think too much about it now. You can have a look at things when you are ready. I would just advise to not have a specific backend in mind now.

bedrock2, Rupicola and fiat-crypto are btw included in the extended level of the soon to be released Coq Platform 2022.09. I found these libraries rather hard o build before, because there were no tags and one needed a specific set of commits of all the dependencies to compile it. I hope the inclusion makes it much easier to "play" with these developments.

view this post on Zulip walker (Oct 05 2022 at 13:54):

yeah I didn't really have one in mind, my main focus was was on trying to get a good dependently typed intermedite representation. but the reality is I couldn't even prove preservation for language that contains dependent pi types with book style universes.

view this post on Zulip walker (Oct 05 2022 at 13:55):

but thanks a lot for letting me know about bedrock2, I never heard about it and it sounds like an interesting project

view this post on Zulip walker (Oct 05 2022 at 14:02):

also I honestly never used coq platform before, I build stuff by hand or opam

view this post on Zulip Michael Soegtrop (Oct 05 2022 at 14:38):

Well you might be using Coq Platform anyway. The majority of the work behind it is not the scripts or the installers, but to make people create compatible sets of opam packages in a reasonable time frame after a Coq release and test if this actually works. For bedrock2 there likely would not be an opam package without Coq Platform (see https://github.com/coq/platform/issues/178). All the "please create an opam package which works" issues linked in (https://github.com/coq/platform/issues/274) might give you an impression on the impact of Coq Platform on opam.

view this post on Zulip Paolo Giarrusso (Oct 05 2022 at 16:10):

@walker re "gallina with side effects and resources", I'd mention ATS as related work, and note it uses refinement types (not quite dependent types)

view this post on Zulip Kenji Maillard (Oct 05 2022 at 16:18):

And more recently the introduction of exceptional type theories, as well as the lines of work on dependent call-by-push-value (cf the various papers of Pédrot-Tabareau, Ahman, Vakar)

view this post on Zulip Pierre-Marie Pédrot (Oct 05 2022 at 16:28):

Dependent types with effects are quite nasty, if you want my opinion.

view this post on Zulip Pierre-Marie Pédrot (Oct 05 2022 at 16:29):

Basically you have to pick a side between call-by-name and call-by-value, and then you get two wildly different realms that are both annoying, for different reasons.

view this post on Zulip Pierre-Marie Pédrot (Oct 05 2022 at 16:30):

CBN is the most natural choice for MLTT (it's actually implicitly already the case), but it's a terrible setting for most effects.

view this post on Zulip Pierre-Marie Pédrot (Oct 05 2022 at 16:30):

CBV is better for effects but then you get into very weird crap due to dependent types, and you essentially have to always defensively turn things into values to be able to depend on them.

view this post on Zulip walker (Oct 05 2022 at 16:49):

I received this as a advice, and I actually checked it once, but will dig deeper into it soon.

view this post on Zulip Enrico Tassi (Oct 05 2022 at 20:34):

@Kenji Maillard @Pierre-Marie Pédrot could you suggest a good reference for the lazy reader? The two remarks by PMP about CBN and CBV look very interesting to me, where can I read about them? (sorry, I don't have the time to do a lot of bibliography myself)

view this post on Zulip Pierre-Marie Pédrot (Oct 06 2022 at 05:00):

I think that https://hal.inria.fr/hal-02383109 is a good start (albeit a bit dense).


Last updated: Jan 29 2023 at 19:02 UTC