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?

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

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

fields?

Do you have a simple example?

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

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

no

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

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

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

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.

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

I think this feature is unrelated to PR 15693

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

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

.

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

implementing reification via unification

Exactly

We do use your solution here and there in mathcomp

The one with explicit equality?

And I agree it is awkward, but works

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

I agree the record is unnecessary.

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

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

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

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.

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

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

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

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

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

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.

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

the example has `Nat : type`

, add `List (t : type) : type`

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

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

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

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

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.

I see.

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

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: Nov 29 2023 at 19:01 UTC