Stream: Coq devs & plugin devs

Topic: Canonical projections on `:=` record fields

Janno (Apr 21 2022 at 09:55):

While playing around with https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Having.20implicit.20arguments I noticed that it would be super convenient to be able to declare := records fields canonical. The attribute syntax is already 100% happy with that (probably a bug?) but of course no canonical projection is declared. It seems that one blocker for this feature is that these fields cannot actually be specified in record values, which makes it difficult to control the value used for canonical projections on such fields. The use case from the link is basically inverting a function. If there was a way to indicate how much that function should be reduced for the key used in the table of canonical projections one could probably get away with not having to store the reduced value in any actual term. Imagine something like Structure BLA := { normal_field : X; definition_field := f normal_field }. Canonical Structure bla := {| normal_field := val; #[eval(hnf)] definition_field (* no value *); |}. Or, maybe even an attribute #[canonical] definition_field := t where the OCaml implementation would check that t is convertible to f val. Does any of this make sense? Are there theoretical blockers for a feature like this?

Janno (Apr 21 2022 at 09:56):

Also, is any of this already covered by https://github.com/coq/coq/pull/15693? I do not understand that MR very well.

Janno (Apr 21 2022 at 09:57):

By that I mean: can the same goal be achieved by reversible coercions instead of canonical := fields?

Pierre Roux (Apr 21 2022 at 10:58):

Do you have a simple example?

Gaëtan Gilbert (Apr 21 2022 at 11:13):

Canonical bla := {| foo := bli; bar := zik |}. creates hints that foo _ = bli and bar _ = zik can be inverted by setting _ to bla
could we imagine a more general way to declare unification hints for inverting functions without involving records?
ie some kind of imaginary syntax such that

Definition bla := {| foo := bli; bar := zik |}.
MagiCanonical foo bla := bli.
MagiCanonical bar bla := zik.

would have the same effect as the above Canonical.
(probably with some syntactic restrictions on MagiCanonical, ie it probably can't deal with arbitrary terms)

Guillaume Melquiond (Apr 21 2022 at 11:46):

Do you know about http://www-sop.inria.fr/members/Enrico.Tassi/nonunifcoerc.pdf ?

Gaëtan Gilbert (Apr 21 2022 at 11:47):

no

Guillaume Melquiond (Apr 21 2022 at 11:51):

Actually, I mixed them up, the one I wanted to cite is http://www-sop.inria.fr/members/Enrico.Tassi/tphol09.pdf

Gaëtan Gilbert (Apr 21 2022 at 12:08):

I think I read that but it's been a while

Janno (Apr 21 2022 at 12:08):

@Gaëtan Gilbert I am sure there are more general mechanisms but canonical structures already exist and what little familiarity I have with the code makes me think that this extension could possibly be implemented rather easily, disregarding any possible bikeshedding about how to indicate the exact value used for the canonical projection of such fields.

Enrico Tassi (Apr 21 2022 at 20:30):

Well, unification hints (the second paper cited up there) would let you add to unification any rule as long as the hinted solution is accepted by conversion.

Actually, my original intent in developing elpi was to use it to express unification, and in that setting a hint would just be an extra clause (for the "unif" predicate) which can be used, for example, to invert a function. There is even a toy elaborator (type inference + unification) written in elpi, but lacks error reporting, and I got busy pushing other uses of the language.

Depending on where you want to use this kind of inference, it may or may not be possible to use elpi already today. I hope at some point to provide an opt-in elaborator which you can fully customize, but it is not ready yet.

Enrico Tassi (Apr 21 2022 at 20:37):

Canonical Structures are a subest of unification hints where the problem for which the user is allowed to supply a hint are of the form

$$\frac{?hint~=~record instance}{projection~?hint = value}$$

or in elpi (pseudo code):

unif (app[projection,HINT]) value :- HINT = record instance.

Enrico Tassi (Apr 21 2022 at 20:42):

I think this feature is unrelated to PR 15693

Janno (Apr 21 2022 at 20:42):

The original prompt for my question was the coq users thread I linked to which basically boils down to this scenario:

Inductive type : Set := | Nat.
Definition typeDenote (t:type) : Set :=
  match t with | Nat => nat end.
Inductive binop : type -> type -> type -> Set :=
| Fn : forall {t1 t2 t3:type}, ((typeDenote t1) -> (typeDenote t2) -> (typeDenote t3))
    -> binop t1 t2 t3.
Fail Check @Fn _ _ _ (fun x y : nat => x + y).

Janno (Apr 21 2022 at 20:43):

The problem is likely clear to most people here: unification cannot resolve typeDenote ?x = nat.

Enrico Tassi (Apr 21 2022 at 20:44):

That is the running example of the paper above ;-)

Enrico Tassi (Apr 21 2022 at 20:44):

implementing reification via unification

Janno (Apr 21 2022 at 20:45):

Exactly

Enrico Tassi (Apr 21 2022 at 20:46):

We do use your solution here and there in mathcomp

Janno (Apr 21 2022 at 20:46):

The one with explicit equality?

Enrico Tassi (Apr 21 2022 at 20:46):

And I agree it is awkward, but works

Janno (Apr 21 2022 at 20:46):

Right.. what I am arguing is that it is entirely unnecessary :)

Enrico Tassi (Apr 21 2022 at 20:54):

here

Enrico Tassi (Apr 21 2022 at 20:55):

I agree the record is unnecessary.

Janno (Apr 21 2022 at 20:56):

I agree the record is unnecessary.

That's taking it one step further than what I was trying to say. I am simply claiming that the equality is unnecessary (and thus any explicit rewriting).

Janno (Apr 21 2022 at 20:57):

And by that I mean that Coq already has all the ingredients to make this work without an equality. It really just needs a bit of surface syntax to make it possible to declare := record fields canonical with a specific value (which needs to be convertible to the body of the field).

Enrico Tassi (Apr 21 2022 at 20:58):

If you take the example in math comp, the record has two fields, if you remove one then the record becomes silly.

Janno (Apr 21 2022 at 20:59):

In that case there is indeed a local maximum of silliness but I suspect there are other use cases (such as the example above) where the record would still have fields without a body.

Janno (Apr 21 2022 at 21:00):

Although maybe even that could be turned into a one-field record? It seems that way.

Enrico Tassi (Apr 21 2022 at 21:00):

In the example by the user, there is no record, there is an inductive type (AST) and a function on it (interpretation).

Janno (Apr 21 2022 at 21:00):

In any case, nobody ever said they wanted to write records to guide unification. CS is simply one tool we already have.

Enrico Tassi (Apr 21 2022 at 21:00):

Maybe, but my point is that "there should be no record"

Janno (Apr 21 2022 at 21:02):

I fully agree but I don't know how quickly we can get there.

Enrico Tassi (Apr 21 2022 at 21:03):

Well, yes, "upgrading" CS is doable, but I'm afraid that to make that example work in practice you would need a bit more, e.g. in CS "recursion" is somewhat hardcoded, while there you need to say a bit more. Imagine the AST has "list of AST" as one constructors. You quickly need a language which is not much simpler than the one I give in the paper, I'm afraid.

Janno (Apr 21 2022 at 21:05):

That sounds intriguing. Can you make that new AST node more concrete? I don't think I understand what you mean.

Enrico Tassi (Apr 21 2022 at 21:06):

the example has Nat : type, add List (t : type) : type

Enrico Tassi (Apr 21 2022 at 21:06):

if a CS instance has a structure as argument, it uses it and this adds a projection which is where "inference will do a rec call".

Enrico Tassi (Apr 21 2022 at 21:08):

I'm sorry but it is getting late, I'll catch up on this thread tomorrow.

Janno (Apr 21 2022 at 21:10):

Sure! I'll play around with the new AST node

Janno (Apr 21 2022 at 21:13):

This here works (and so would a hypothetical version using a := field) so I suspect I am doing something wrong

Inductive type : Set := | Nat | List (t : type).
Fixpoint typeDenote (t:type) : Set :=
  match t with | Nat => nat | List t => list (typeDenote t) end.
Inductive binop : type -> type -> type -> Set :=
| Fn : forall {t1 t2 t3:type}, ((typeDenote t1) -> (typeDenote t2) -> (typeDenote t3))
    -> binop t1 t2 t3.
Fail Check @Fn _ _ _ (fun x y : nat => x + y).

Structure type' :=
  { #[canonical=no] type'_type :> type;
    typeDenote' :> Set;
    #[canonical=no] typeDenote'_ok : typeDenote type'_type = typeDenote';
  }.
Canonical Structure type'_nat := {| type'_type := Nat; typeDenote' := nat; typeDenote'_ok := eq_refl |}.
Canonical Structure type'_list (t : type') :=
  {| type'_type := List t;
    typeDenote' := list t;
    typeDenote'_ok := f_equal (A:=Set) (B:=Set) (fun T => list T) (typeDenote'_ok t)
  |}.
Definition Fn' {t1 t2 t3 : type'} : (typeDenote' t1 -> typeDenote' t2 -> typeDenote' t3) -> binop t1 t2 t3 :=
  match typeDenote'_ok t1 in _ = T1, typeDenote'_ok t2 in _ = T2, typeDenote'_ok t3 in _ = T3 return
        (T1 -> T2 -> T3) -> _
  with
  | eq_refl, eq_refl, eq_refl => Fn
  end.
Check @Fn' _ _ _ (fun (x y:nat)=>x).
Check @Fn' _ _ _ (fun (x y:list nat)=> x).

Enrico Tassi (Apr 21 2022 at 21:18):

I expressed myself badly. If you stay with records it will work. I just find that is the record the boring part, not the equation.

Janno (Apr 22 2022 at 07:41):

I see.

Janno (Apr 22 2022 at 07:42):

Again, I do agree with that and you won't see me complaining when I never have to write canonical structures ever again. :)

Janno (Apr 22 2022 at 07:51):

My takeaway from the discussion so far is that 1) everybody seems to have a better system in mind (and that systems seems to be unification hints or some restricted version of it) and 2) nobody has specific objections to the proposed extension to CS. I'd love to hear more on (2). I still think that implementing the extension would be worthwhile on its own. It might even produce more examples and ideas for a more powerful mechanism.

Last updated: Sep 15 2024 at 13:02 UTC