EqClass

An experiment: Turning eqType into a Class

(Slides from a Working Group)

Context

• Explore canonical structures and type classes for stdlib2

• How to overload notations, operator names, lemmas?

Basic idea

• Rebuild the mathematical components library using type classes
• current state https://github.com/vbgl/math-comp/tree/typeclasses

Spoiler

• Not yet successful; but we’ve learned a few things

Limitations of Canonical Structures

• Hard to understand
• Resolution only triggered during type unification: hence phantom types
• No back-tracking (or ad-hoc and bounded, using tags)
• Hard to introduce a new layer in an existing hierarchy

The hierarchy

Which canonical structures: Superstructures as subobjects

Module Choice.

Record mixin_of T := Mixin {
  find : pred T -> nat -> option T;
  _ : …
}.

Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}.

Structure type := Pack {sort; _ : class_of sort}.

(* Inheritance *)
Canonical eqType (cT: type) : Equality.type := ….

End Choice.

• Mixins collect operators and properties.
• Classes pack mixins with superclasses.
• Types pack carriers with classes.

Inference by unification

Goal forall (T: Choice.type) (x : Choice.sort T), x == x.

To infer the first (implicit) argument of “==” (at Equality.type), the types of x are unified:

• as argument of “==”: Equality.sort ?U;
• as given: Choice.sort T.

We are looking for an equality type, knowing a choice type; fortunately, Choice.eqType has been registered as canonical.

With type classes

Module Choice.

Record mixin_of T := Mixin {
  find : pred T -> nat -> option T;
  _ : …
}.

Class class T := Class { base :> eqClass T; mixin : mixin_of T }.
Hint Mode class ! : typeclass_instances.

End Choice.

• Other possible designs: take operators as one or more arguments
• The base property is registered as an instance (∀ T, Choice.class T → Equality.class T)
• Use of modes to prevent wild guesses

Inference by resolution (à la Prolog)

Goal forall (T: Type) (cT: Choice.class T) (x: T), x == x.

To infer the second (implicit) argument of “==” (at Equality.class T), rules (aka instances) are applied:

• is there a solution in context?
• is there some way to deduce a solution from something else?

On sait d’où l’on vient sans savoir où l’on va (ou bien l’inverse).

Minor issues

A few tactics are not ready

• Issues with pose, have, rewrite… They resolve type-classes too early or generalize them too much.

Constants take many more arguments

• Not too annoying yet.

• Might be much worse with operators-as-arguments.

A few bugs

Bad interaction of scheduling with modes

Various cases of resolution fail, when it shouldn’t.

See https://github.com/coq/coq/issues/9058

Hint Extern If not yet available

To implement cuts, a crucial instrument in prolog programming

See https://github.com/coq/coq/pull/6285

Opacity

The typeclass opacity mechanism should be per type and per class

A major performance concern

With canonical structures, both ends of the searched path are part of the problem, with classes only one:

• Equality.sort ?U === Choice.sort T
• Equality.Class T

It is very difficult to correctly guide the resolution, since the other end of the path is unknown.

Guessing

• It works in Haskell, since:

  • hierarchies are more shallow (e.g., a commutative ring is the same as a ring);
  • expressions are small (e.g., no big polynomial as a literal expression in usual programs).

• The blow-up of the number of arguments will become an annoyance.

• The performance issue will be very problematic.

Questions

• Will the open issues be addressed?
• Should we carry on this experiment?
• Are unification hints the real solution? or ELPI? or theory combinators