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?

- Make a by-hand copy of all the relevant safechecker files/definitions, without using squashing (probably has maintenance overhead?)
- 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
- Adapt some form of "retyping" to prove
`∥ typing ... ∥ -> typing ...`

(not sure how feasible this is?) - 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?)
- Something else???

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.

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

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

A typing assumption in my first question

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).

@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?

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.

I guess you would rather have it now right?

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

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

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

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.

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?

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?

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.

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).

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?

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.

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.

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:

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".
```

)

(This is with Coq 8.16)

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

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.)

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

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.

and template poly isn't planned ever, right?

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?

Well it would mean being independent of the standard library?

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?

Also, what's the issue with eta?

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.

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.

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

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

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

But for sure we tried.

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

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

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?)

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

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.

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)

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?)

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

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?

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.

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

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

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 η

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

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

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)

I think the usual definition of canonicity is state with definitional equality, because that's the thing that exists in most type theories: if $n$ is a **closed** term of type $\mathbb{N}$ then it is definitionally equal to a numeral.

The version with reduction I would call *effective* or *computational canonicity*.

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 $n$ is a

closedterm of type $\mathbb{N}$ then it is definitionally equal to a numeral.

The version with reduction I would calleffectiveorcomputational canonicity.

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

"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

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