Stream: MetaCoq

Topic: Non-squashed typing judgments


view this post on Zulip Jason Gross (Apr 08 2023 at 20:13):

For proving typing of Gallina Quotation, I'd like to be able to invoke the safechecker (SafeCheckerPlugin.SafeTemplateChecker.infer_template_program or SafeChecker.PCUICSafeChecker.typecheck_program, probably) on closed terms, and get out an unsquashed typing judgment. (I'd really rather not have to build all of the typing judgments by hand.)

Does anyone have thoughts on the following approaches?

  1. Make a by-hand copy of all the relevant safechecker files/definitions, without using squashing (probably has maintenance overhead?)
  2. Refactor the safechecker to separate the proofy parts from the non-proofy parts, so that we never need to squash things, and extraction will just not need to manage typing judgments at all
  3. Adapt some form of "retyping" to prove ∥ typing ... ∥ -> typing ... (not sure how feasible this is?)
  4. Try to write a template program that walks the existing safechecker and replaces "squash" with "id" (not sure if this can be done fully systematically?)
  5. Something else???

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 06:53):

I think going for option 2 is the way I want to go. This was my motivation for writing https://github.com/TheoWinterhalter/coq-partialfun in order to integrate rewrite rules without having to assume they terminate. Also it's indeed nice to separate proofs from programs, especially for something we want to extract.

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 06:55):

@Meven Lennon-Bertrand is testing its viability on another project and then we'll see if everyone is on board.

view this post on Zulip Matthieu Sozeau (Apr 11 2023 at 09:29):

How can you define the safe reduction without a typing judgment? You mean having a partial type checker then? I think option 3 retyping is the way to go in the short term, @Jason this is mostly the interface it has: from a squashed typing assumption you can recover the type. I guess recovering the typing derivation would not be too hard

view this post on Zulip Matthieu Sozeau (Apr 11 2023 at 09:29):

A typing assumption in my first question

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 11:13):

Yes, we define the checker as a partial function that is defined on its domain and we later show that all SN terms are in the domain (no need to actually assume well-typedness implies SN).

view this post on Zulip Jason Gross (Apr 11 2023 at 16:54):

@Théo Winterhalter Ah, that looks neat! And this would also solve the problem of how to get typing judgments that don't rely on an SN axiom, and it looks like the machinery is basically there to get efficient proofs, too (basically just do def x (succeeds_domain <some fuel> x (eq_refl true <: succeeds <some fuel> x = true))) ... maybe you want to make a version of autodef that takes fuel as an argument, and modify the IsTrue hint to run vm_compute?)

Any estimated timeline on all this?

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 17:38):

Yeah. The issue with my fueled version is that it doesn't do the exponential trick we do with Acc (Acc_gen) but my attempt to do so still seemed to evaluate under lambdas.
But yeah, there are clearly many ways to improve what I did I think. :)

I guess it depends how much the other MetaCoq dev are on board, but it'd be nice to have it soonish.

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 17:38):

I guess you would rather have it now right?

view this post on Zulip Théo Winterhalter (Apr 11 2023 at 17:39):

The problem we had with Meven was trying to combine monadic code for errors with the monadic code for partiality.

view this post on Zulip Meven Lennon-Bertrand (Apr 12 2023 at 14:12):

More generally, I'd say it would be nice to play a bit more with the framework to polish it before going for full-blown MetaCoq. But my experimentations with Théo's library got me convinced that we should be able to get something decent out of it within a few months

view this post on Zulip Meven Lennon-Bertrand (Apr 12 2023 at 14:13):

Currently, I agree with Matthieu that your best bet would probably be to modify the retyper

view this post on Zulip Jason Gross (Apr 13 2023 at 06:40):

I guess you would rather have it now right?

No rush. I'm almost done setting up raw quotation for PCUIC terms, though I think proving well-typedness of the quoted terms will have to wait until the partiality is integrated into MetaCoq. This is just a side-project for me, though, so I'm in no rush.

view this post on Zulip Jason Gross (Apr 13 2023 at 06:41):

he issue with my fueled version is that it doesn't do the exponential trick we do with Acc (Acc_gen) but my attempt to do so still seemed to evaluate under lambdas.

What's the issue here? When you try to do the exponential trick with something like Inductive thunked_nat := O | S (_ : unit -> thunked_nat). things still blow up?

view this post on Zulip Jason Gross (Apr 13 2023 at 06:43):

The problem we had with Meven was trying to combine monadic code for errors with the monadic code for partiality.

What's the issue? Show that fun A => Partial (WithError A) is a monad, write "raise error", etc, functions for this monad, and things should just work nicely, right?

view this post on Zulip Théo Winterhalter (Apr 13 2023 at 06:43):

Ah no I tried to do it with a continuation, like for Acc: https://github.com/TheoWinterhalter/coq-partialfun/pull/6
Maybe it works with thunked_nat, worth a try. I wasn't aware of this solution.

view this post on Zulip Théo Winterhalter (Apr 13 2023 at 06:45):

Jason Gross said:

The problem we had with Meven was trying to combine monadic code for errors with the monadic code for partiality.

What's the issue? Show that fun A => Partial (WithError A) is a monad, write "raise error", etc, functions for this monad, and things should just work nicely, right?

There is no fundamental issue, we're just not expert enough with typeclasses to have it behave the way we want (when we use bind it does not pick up the right instance, ie it uses the bind for Partial and not for the combination).

view this post on Zulip Jason Gross (Apr 13 2023 at 06:46):

Ah no I tried to do it with a continuation, like for Acc: https://github.com/TheoWinterhalter/coq-partialfun/pull/6
Maybe it works with thunked_nat, worth a try. I wasn't aware of this solution.

Ah, that looks like it should work, I don't expect thunked_nat to work any better since it relies on the same lambda trick. What goes wrong with this PR?

view this post on Zulip Jason Gross (Apr 13 2023 at 06:48):

we're just not expert enough with typeclasses to have it behave the way we want (when we use bind it does not pick up the right instance, ie it uses the bind for Partial and not for the combination).

Do Definition PartialWithError A := Partial (WithError A) and then do #[export] Typeclasses Opaque PartialWithError. And make sure that you use aliases for all the combinators (raise-error, run-with-fuel, etc) that are phrased in terms of PartialWithError instead of the underlying monad.

view this post on Zulip Théo Winterhalter (Apr 13 2023 at 06:50):

Jason Gross said:

Ah no I tried to do it with a continuation, like for Acc: https://github.com/TheoWinterhalter/coq-partialfun/pull/6
Maybe it works with thunked_nat, worth a try. I wasn't aware of this solution.

Ah, that looks like it should work, I don't expect thunked_nat to work any better since it relies on the same lambda trick. What goes wrong with this PR?

To be honest I don't know yet. I tried to it by hand and it seems to work, but here autodef takes forever.

view this post on Zulip Théo Winterhalter (Apr 13 2023 at 06:51):

Jason Gross said:

we're just not expert enough with typeclasses to have it behave the way we want (when we use bind it does not pick up the right instance, ie it uses the bind for Partial and not for the combination).

Do Definition PartialWithError A := Partial (WithError A) and then do #[export] Typeclasses Opaque PartialWithError. And make sure that you use aliases for all the combinators (raise-error, run-with-fuel, etc) that are phrased in terms of PartialWithError instead of the underlying monad.

Thanks, I will try! :smile:

view this post on Zulip Jason Gross (Apr 13 2023 at 07:47):

To be honest I don't know yet. I tried to it by hand and it seems to work, but here autodef takes forever.

What takes forever with autodef? And does it still happen if you insert vm_compute in the hint? (I tried building the exp-fuel branch locally, but got

File "./theories/PartialFun.v", line 480, characters 12-14:
Error:
In environment
A : Type
B : A  Type
f :  x, B x
pre : precond
post : postcond
x : A
n : nat
v : B x
h : funind pre post
hpre : pre x
e : fueled (S n) x = Success v
ih :  (x : A) (v : B x), pre x  fueled n x = Success v  post x v
Unable to unify
 "∀ (x : A) (v : B x), pre x → fueled n x = Success v → post x v" with
 "∀ (x : A) (w : B x),
    pre x
    → (fix fueled_gen
         (n : nat) (fumes : ∀ y : A, Fueled (B y)) (x0 : A) {struct n} :
           Fueled (B x0) :=
         match n with
         | 0 => fumes x0
         | S n0 =>
             orec_fuel_inst n0 (f x0)
               (fueled_gen n0 (λ x1 : A, fueled_gen n0 fumes x1))
         end) n
        (λ x0 : A,
           (fix fueled_gen
              (n : nat) (fumes : ∀ y : A, Fueled (B y)) (x1 : A) {struct n} :
                Fueled (B x1) :=
              match n with
              | 0 => fumes x1
              | S n0 =>
                  orec_fuel_inst n0 (f x1)
                    (fueled_gen n0 (λ x2 : A, fueled_gen n0 fumes x2))
              end) n (λ y : A, NotEnoughFuel) x0) x =
      Success w → post x w".

)

view this post on Zulip Jason Gross (Apr 13 2023 at 07:47):

(This is with Coq 8.16)

view this post on Zulip Théo Winterhalter (Apr 13 2023 at 07:51):

Ah I guess something went wrong with my apply stash. I'll try to fix i!t

view this post on Zulip Jason Gross (Apr 13 2023 at 08:02):

Btw, I think a good test case for "is the safechecker good enough for gallina quotation" is that the safechecker should be able to safecheck itself, and generate an unsquashed typing derivation which does not rely on any SN axioms. (I guess it can rely on funext, UIP, guard, and primitive int/float axioms, for now.)

view this post on Zulip Théo Winterhalter (Apr 13 2023 at 08:53):

It would be good, but for now, we cannot even use it on the standard library because we lack η\eta and template polymorphism.

view this post on Zulip Théo Winterhalter (Apr 13 2023 at 09:16):

Jason Gross said:

To be honest I don't know yet. I tried to it by hand and it seems to work, but here autodef takes forever.

What takes forever with autodef? And does it still happen if you insert vm_compute in the hint? (I tried building the exp-fuel branch locally, but got

I fixed it, it was just not up to date. So now it should build with 8.16 and still take forever in Examples.v:22 but I guess it's just normal for it to take forever since it's a looping argument. So probably all is well.

view this post on Zulip Paolo Giarrusso (Apr 13 2023 at 19:23):

and template poly isn't planned ever, right?

view this post on Zulip Jason Gross (Apr 13 2023 at 20:16):

Presumably some day @Pierre-Marie Pédrot is going to replace template polymorphism with sort polymorphism, right?

Do you think it's worth it to rework the safechecker to not rely on template poly / eta anywhere, so that it can safecheck itself?

view this post on Zulip Théo Winterhalter (Apr 13 2023 at 20:38):

Well it would mean being independent of the standard library?

view this post on Zulip Jason Gross (Apr 13 2023 at 22:51):

Maybe it's worth writing a translation (without proofs) from template poly to universe poly + duplication? Then we can just run the translation on the safechecker, mangle names, unquote the newly-independent safechecker, and then run that on itself or something?

view this post on Zulip Jason Gross (Apr 13 2023 at 22:52):

Also, what's the issue with eta?

view this post on Zulip Théo Winterhalter (Apr 14 2023 at 06:45):

Jason Gross said:

Maybe it's worth writing a translation (without proofs) from template poly to universe poly + duplication? Then we can just run the translation on the safechecker, mangle names, unquote the newly-independent safechecker, and then run that on itself or something?

I guess it could work.

view this post on Zulip Théo Winterhalter (Apr 14 2023 at 06:47):

Jason Gross said:

Also, what's the issue with eta?

The issue with η\eta is specification: since our spec for conversion is untyped it's not clear how to add it in a way that doesn't break other properties. All our attempts failed, and—at least Meven and I—believe that the right way to go is to have a typed conversion specification, but that's certainly a lot of work.

view this post on Zulip Jason Gross (Apr 14 2023 at 11:32):

What breaks if you spec it as the symmetric transitive closure of eta contraction?

view this post on Zulip Jason Gross (Apr 14 2023 at 11:34):

(This allows you to leverage the types because you have access to the function binder types/the explicit constructor)

view this post on Zulip Théo Winterhalter (Apr 14 2023 at 12:52):

I don't remember precisely, maybe @Meven Lennon-Bertrand recalls?

view this post on Zulip Théo Winterhalter (Apr 14 2023 at 12:52):

But for sure we tried.

view this post on Zulip Meven Lennon-Bertrand (Apr 17 2023 at 10:58):

In a setting with annotated binders, η-contraction breaks confluence , even on well-typed terms: fun (x : Type@{i}) ((fun y : Type@{j} => y) x β-reduces to fun x : Type@{i} => x and η-reduces to fun y : Type@{j} => y, but in general these are not equal

view this post on Zulip Meven Lennon-Bertrand (Apr 17 2023 at 11:00):

I gave a talk at last year's WITS on these issues with untyped η (the slides, abstract and video are on my webpage)

view this post on Zulip Jason Gross (Apr 17 2023 at 18:44):

Are confluence and canonicity the same? Or is confluence the algorithmic counterpart to canonicity? Or something else?

And eta-contraction gives confluence only up to cumulativity? (I feel like this fits with cubical type theory only giving canonicity up to homotopy. Is having confluence/canonicity only up to cumulativity a problem?)

view this post on Zulip Jason Gross (Apr 17 2023 at 18:45):

(btw, the link to the abstract is a 404: https://www.meven.ac/documents/22-Types-abstract.pdf)

view this post on Zulip Paolo Giarrusso (Apr 17 2023 at 20:07):

Canonicity is a weaker relative of SN while even untyped lambda calculus has confluence, also known as Church-Rosser: if a ->* b and a ->* c, then exists d, b -> d and c -> d.

view this post on Zulip Yannick Forster (Apr 17 2023 at 20:08):

I agree that confluence is about untyped things, while canonicity is about typed things. But the answer might also depend a bit on what you call canonicity (and I think not everybody calls the same thing canonicity)

view this post on Zulip Paolo Giarrusso (Apr 17 2023 at 20:10):

Are https://link.springer.com/chapter/10.1007/3-540-62688-3_35 and other works from Ghani still canonical on how eta-reduction is super-fragile (even on STLC?)

view this post on Zulip Paolo Giarrusso (Apr 17 2023 at 20:13):

Found https://www.cs.le.ac.uk/people/ng13/eta.html again

view this post on Zulip Jason Gross (Apr 18 2023 at 07:16):

Wait, even if η-contraction breaks confluence, this shouldn't matter if it's implemented only as a conversion rule, and not as a reduction rule, right?

view this post on Zulip Théo Winterhalter (Apr 18 2023 at 07:43):

Well, then we have to prove we can postpone the use of η\eta so that when comparing to Π\Pi-types we know we can simply check if they have a common reduct. Essentially we need this to prove injectivity of Π\Pi which we need to prove subject reduction.

view this post on Zulip Meven Lennon-Bertrand (Apr 18 2023 at 09:15):

I wouldn't say that confluence has to be about untyped things: there's a line of paper by Adams and then Silès and Herbelin that do confluence proofs (with parallel reduction) for a typed reduction, to obtain equivalence of typed and untyped conversion, and we are trying to revive this line of work to try and tackle η in MetaCoq

view this post on Zulip Meven Lennon-Bertrand (Apr 18 2023 at 09:17):

In my book, confluence is what Paolo said, while canonicity says that every natural number in an empty context reduces to either 0 or a successor, or something of this taste. For me, it feels like some form of SN, saying that computations always terminate, and give you the kind of values you expect

view this post on Zulip Meven Lennon-Bertrand (Apr 18 2023 at 09:18):

And yes, the issue with η is that currently we rely heavily on confluence in the metatheory of MetaCoq, in particular to establish injectivity of type constructors (which in turn get us subject reduction). So the question is how to do the same proof of injectivity, but in a setting with η

view this post on Zulip Yannick Forster (Apr 18 2023 at 09:18):

You are submitting a paper soon with a different notion of canonicity :) That's mostly because in my book, canonicity (for nat) does not imply SN (for nat). Rather, I'd say canonicity should state that (wh) normal forms of type nat are a constructor application

view this post on Zulip Yannick Forster (Apr 18 2023 at 09:19):

(there are reflexive transitive closures missing in the conclusion of Paolo's statement)

view this post on Zulip Meven Lennon-Bertrand (Apr 18 2023 at 09:25):

Yannick Forster said:

You are submitting a paper soon with a different notion of canonicity :) That's mostly because in my book, canonicity (for nat) does not imply SN (for nat). Rather, I'd say canonicity should state that (wh) normal forms of type nat are a constructor application

Argh! I think I disagree with this then ^^' And at least Loic and Nicolas seem to agree with my usage:

From there, we deduce the canonicity theorem: all integers reduce to standard integers in the empty context.
(there, it is a consequence of normalization and canonicity)

view this post on Zulip Théo Winterhalter (Apr 18 2023 at 09:25):

I think the usual definition of canonicity is state with definitional equality, because that's the thing that exists in most type theories: if nn is a closed term of type N\mathbb{N} then it is definitionally equal to a numeral.
The version with reduction I would call effective or computational canonicity.

view this post on Zulip Meven Lennon-Bertrand (Apr 18 2023 at 09:40):

Théo Winterhalter said:

I think the usual definition of canonicity is state with definitional equality, because that's the thing that exists in most type theories: if nn is a closed term of type N\mathbb{N} then it is definitionally equal to a numeral.
The version with reduction I would call effective or computational canonicity.

Indeed, and then homotopy canonicity is obtained by replacing definitionally equal to propositionally equal.

view this post on Zulip Gaëtan Gilbert (Apr 18 2023 at 11:05):

"nats in empty context weak head reduce to a constructor" implies "nats in empty context reduce to numerals" right?
For instance AFAICT nat_rect (fun _ => nat) 0 (fun _ IH => IH) n reduces to 0 iff n reduces to a numeral
and it also works if we replace "reduce" with "definitionally equal to" (but not propositionally)
and it's not quite SN as there may be non terminating reduction strategies

view this post on Zulip Meven Lennon-Bertrand (Apr 18 2023 at 15:02):

Jason Gross said:

(btw, the link to the abstract is a 404: https://www.meven.ac/documents/22-Types-abstract.pdf)

Indeed, thanks! It's corrected now


Last updated: Jul 23 2024 at 20:01 UTC