Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generalized coercions #420

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Conversation

Tragicus
Copy link

This PR adds better support for coercions:

  • declares the constructor of the class as an elpi coercion, using elaborate-skeleton to fill in the holes,
  • declares the sort projection as an elpi coercion when there is no coercion target,
  • declares axioms_ as a typeclass (enables inference in the first coercion)

Copy link
Member

@gares gares left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have one question: do we really need the coercions to use unification to see if we are from/to a structure? I don't see the point of aliasing a structure.

If the clauses were of the form

pi bla bla bla\ coercion ctx v (app[Structure|RevArgs]) e r :-

they could be indexed much better (we have some deep indexing features in the pipes). This rule would trigger only if the type is syntactically the structure type constructor applied to the list of arguments. The body can still use unification if needed.

HB/structure.elpi Outdated Show resolved Hide resolved
HB/structure.elpi Outdated Show resolved Hide resolved
HB/structure.elpi Outdated Show resolved Hide resolved
HB/structure.elpi Outdated Show resolved Hide resolved
HB/structure.elpi Outdated Show resolved Hide resolved
@gares
Copy link
Member

gares commented May 28, 2024

@CohenCyril LGTM. Can you double check and merge?

Copy link
Member

@CohenCyril CohenCyril left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's great @Tragicus thanks for pushing.

I have a general question: how does it compose with coq coercions?
e.g. reusing your test-suite file (coercion.v), this is what happens if I have

Axioms (A B B' C : Type) (AtoB : A -> B) (BtoB' : B -> B').
Axioms (P : A -> Prop) (CtoAP : C -> sigType A P). 
Coercion AtoB : A >-> B.
Coercion BtoB' : B >-> B'.
(* does postcompose automatically with Coq coercions*) 
Check fun (x : sigType A P) => x : B.
Check fun (x : sigType A P) => x : B'.

(* testing a Coq coercion to sigType *)
Coercion CtoAP : C >-> sigType.
Check fun (x : C) => x : sigType A P.

(* does not precompose automatically with Coq coercions *)
Fail Check fun (x : C) => x : A.
Check fun (x : C) => (x : sigType A P) : A.
Check fun (x : C) => (x : sigType A P) : B.

HB/structure.elpi Outdated Show resolved Hide resolved
HB.structure Definition Sig (T : Type) (P : T -> Prop) := {x of isSigma T P x}.

Check fun (T : Type) (P : T -> Prop) (x : sigType T P) => x : T.
Check fun (T : Type) (P : T -> Prop) (x : T) (Px : Sig T P x) => x : sigType T P.
Copy link
Member

@CohenCyril CohenCyril May 28, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks really nice! But...

  • it is a bit more than generalized coercions, for which I would expect this coercion to work only when (x : T) has been endowed with a HB.instance of isSigma. e.g.
Axioms (A : Type) (P : A -> Type) (x : A) (Px : Sig A P x).

(* should not work indeed *)
Fail Check (x : sigType A P).

(* this works though ...*)
Succeed Check (let Px' := Px in x : sigType A P).

(* This should works but does not *)
HB.instance Definition _ := Px.
Fail Check x : sigType A P.

In comparison, the analogous code, but on Type works:

HB.mixin Record isSigmaT (P : Type -> Prop) (x : Type) := { _ : P x }.
#[short(type="sigTType"), verbose]
HB.structure Definition SigT (P : Type -> Prop) := {x of isSigmaT P x}.

Axioms (X : Type) (PT : Type -> Prop) (PX : SigT PT X).

(* should not work indeed *)
Fail Check (X : sigTType A PT).

(* this works though now ... cf my next point*)
Succeed Check (let PX' := PX in X : sigTType PT).

(* This is what should work and does *)
HB.instance Definition _ := PX.
Succeed Check X : sigTType PT.
  • I cannot find what exactly in the code makes this work, I was wondering what makes it work even when the coercion is not handled by elpi and but by Coq. In comparison, on master the following fails:
From Coq Require Import ssreflect.
From HB Require Import structures.

HB.mixin Record isSigmaT (P : Type -> Prop) (x : Type) := { _ : P x }.

#[short(type="sigTType"), verbose]
HB.structure Definition SigT (P : Type -> Prop) := {x of isSigmaT P x}.

Fail Check fun (P : Type -> Prop) (x : Type) (Px : SigT P x) => x : sigTType P.
Fail Check (let PX' := PX in X : sigTType PT).

Copy link
Member

@gares gares May 28, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the code just above does not work because the whole business does not kick in since the coercion sort is handled by Coq (the tgt is a supported one in this case), so nobody triggers the TC search.

Copy link
Author

@Tragicus Tragicus May 28, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am extremely confused as to why it works in Type but not in Prop. In both cases, HB.instance declares canonical structures and not typeclasses, so it should not work.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Your tests with a let work and not the previous ones because (afaict) the elaborator sees the local context but not the global context.

@Tragicus
Copy link
Author

As your tests show, the sort coercion postcomposes and does not precompose with Coq's coercions. This is because when the algorithm sees that the type of the input term is a structure, it applies the projection and then asks for a coercion to the target type.
The converse holds for the reverse coercion: it precomposes and does not postcompose with Coq's coercions. This is because when the algorithm sees that the target type is a structure, it tries to build the package and lets the elaborator find the missing class. I assume that the elaborator also catches the type mismatch of the subjects and looks for a coercion.

@gares
Copy link
Member

gares commented May 28, 2024

About post composition, the code does not look at the expected type. If the inferred type is a structure it elaborates (sort t) against the expected type. So Coq can insert further coercions.

If the inferred type is not a structure, then it does nothing.

In your last examples I think that the first coercion from C to sigType is inserted by Coq, then elpi goes to A and then Coq goes to C.

I'm not so sure I see a use case for something (that is not a structure) coercing to a structure.

@CohenCyril
Copy link
Member

I'm not so sure I see a use case for something (that is not a structure) coercing to a structure.

One way to test it on a large scale would be to systematically replace Coq coercions by elpi coercions even for structures in Type and see if/where it breaks.

@Tragicus
Copy link
Author

A use case for something that is not a structure coercing to a structure is when you have an object that satisfies properties that would promote it to a structure, e.g. morphisms and subobjects. This coercion allows you to skip the packaging phase.

@gares
Copy link
Member

gares commented Jun 5, 2024

IMO, the only missing bit is a documentation, et least in the changelog.

Changelog.md Outdated Show resolved Hide resolved
@gares
Copy link
Member

gares commented Jun 6, 2024

@CohenCyril can you look at the PR again and decide what to do?

Changelog.md Outdated
Comment on lines 12 to 18
- **Change** `HB.structure` declares the class of a structure (`axioms_`) as a
type class on the subject with all arguments in output mode but for the
subject that is in input mode.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't this completely ortogonal to the coercion part?
To me these raises yet unresolved nontrivial. I have nothing against merging it, but, just in case, I would prefer that it is a distinct commit/PR so that we can revert easily if something goes wrong.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maybe an #[predicate_subtype] default to false?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes or rather #[typeclass]

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for the delay, I rewrote the history as suggested and added a typeclass option.

Changelog.md Outdated Show resolved Hide resolved
structures.v Outdated
@@ -15,7 +15,7 @@ Definition ignore {T} (x: T) := x.
Definition ignore_disabled {T T'} (x : T) (x' : T') := x'.

(* ********************* structures ****************************** *)
From elpi Require Import elpi.
From elpi Require Import elpi coercion.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
From elpi Require Import elpi coercion.
From elpi Require Import elpi.
From elpi.apps Require Import coercion.

Comment on lines 310 to 314
mk-reverse-coercion-aux (prod _N _T Body) Structure G Args Clause :-
Clause = (pi x\ C x),
pi x\ mk-reverse-coercion-aux (Body x) Structure G [x | Args] (C x).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
mk-reverse-coercion-aux (prod _N _T Body) Structure G Args Clause :-
Clause = (pi x\ C x),
pi x\ mk-reverse-coercion-aux (Body x) Structure G [x | Args] (C x).
mk-reverse-coercion-aux (prod _N _T Body) Structure G Args (pi x\ C x) :-
pi x\ mk-reverse-coercion-aux (Body x) Structure G [x | Args] (C x).


pred mk-reverse-coercion i:gref, o:prop.
mk-reverse-coercion Structure Clause :-
coq.typecheck (global Structure) T ok,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
coq.typecheck (global Structure) T ok,
coq.env.typeof Structure T,


pred mk-sort-coercion i:term, i:term, o:prop.
mk-sort-coercion Structure P Clause :-
coq.typecheck Structure T ok,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
coq.typecheck Structure T ok,
std.assert-ok! (coq.typecheck Structure T) "anomaly: mk-sort-coercion",

@gares
Copy link
Member

gares commented Jun 27, 2024

I did a couple of suggestions, to be tested. Other than that it looks OK. @CohenCyril ?

@CohenCyril
Copy link
Member

Taking a look this afternoon

@CohenCyril
Copy link
Member

CohenCyril commented Jun 27, 2024

Could you squash and rebase?
I am considering backtracking on the default status of #[typeclass], would you mind running a bench to check the impact on MC and MCA in both scenarios?

@Tragicus
Copy link
Author

Do we have tools to do a benchmark?

@gares
Copy link
Member

gares commented Jun 28, 2024

I think it would be enough to time make -j1.
You can also make TIMED=1 to get a per file compilation time.

@Tragicus
Copy link
Author

Ok thanks, I will do that tonight or tomorrow.

@Tragicus
Copy link
Author

Tragicus commented Jun 29, 2024

It took forever, but the bench is done. Interestingly enough, the version with typeclasses by default is slightly slower and uses slightly less memory, though the difference is negligible.
bench.ods Should I compare with a bench of master?

@Tragicus
Copy link
Author

Well, I did it anyway, and master is about 3x faster than proto-coercion.
bench.ods.

@Tragicus
Copy link
Author

Here is the new bench, proto-coercion is a little less than 2x slower than master. The profiling might be complicated since the slowdown occurs in tactics like apply:.
benchcoe.ods

@gares
Copy link
Member

gares commented Jul 29, 2024

Damn, I guess we will have to wait for some speedup in the bootstrap time of elpi... or disable coercion in apply: but I don't know if the api makes it easy.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants