Unbundled or semibundled typeclasses?

[palmskog]

While doing some proofreading of the pdf before, I noticed that the typeclasses in ordinals are seemingly using the so-called semibundled approach when defining typeclasses, and not the unbundled approach recommended by Spitters and van der Weegen. For a development of the current size, I believe the unbundled approach will maximize reusability and benefits of type class automation - the risk of exponential blowups will be low with such a small hierarchy.

I will give a key example, which I tried out quickly in an experimental branch.

Consider the following classes from Prelude/DecPreOrder.v:

Class Total {A:Type}(R: relation A) :=
  totalness : forall a b:A, R a b \/ R b a.             

Class Decidable {A:Type}(R: relation A) :=
  rel_dec : forall a b, {R a b} + {~ R a b}.

Class TotalDec {A:Type}(R: relation A):=
  { total_dec :> Total R ;
    dec_dec :> Decidable R}.

Class TotalDecPreOrder {A:Type}(le: relation A) :=
  {
    total_dec_pre_order :> PreOrder le;
    total_dec_total  :> TotalDec le 
  }.

(* ... *)

Lemma le_lt_equiv_dec  {A:Type}(le : relation A)
      (P0: TotalDecPreOrder le) (a b:A) :
   le a b -> {lt a b}+{preorder_equiv a b}.
Proof.
  intro H;  destruct (rel_dec b a).
 -   right;split;auto.
 -  left;split;auto.
Defined.

If we fully apply the unbundled approach, this leads to further factoring of classes and parameters:

Class Total {A} (R : relation A) := 
 totalness x y : R x y \/ R y x.

Class Decision (P : Prop) := decide : {P} + {~P}.

Class RelDecision {A B} (R : A -> B -> Prop) :=
  decide_rel x y :> Decision (R x y).

Notation EqDecision A := (RelDecision (@eq A)).

Class TotalPreOrder {A} (R : relation A) : Prop := {
  total_pre_order_pre :> PreOrder R;
  total_pre_order_total :> Total R
}.

(* ... *)

Definition le_lt_equiv_dec {A} {le : relation A}
 {P0 : TotalPreOrder le} {dec : RelDecision le} (a b : A) :
 le a b -> {lt a b}+{preorder_equiv a b}.
Proof.
  intro H; destruct (decide (le b a)).
  - right;split;auto.
  - left;split;auto.
Defined.

One important idea here is to never mix Prop-sorted and Type-sorted class members, and always let the latter live in singleton "operational" type classes. See p. 7 in the paper by Spitters and van der Weegen.

But I guess the big question is, what is the design philosophy for type classes in ordinal? If the idea is to aim for unbundledness, then I could package up my experiments into some PR later on.

[Casteran]

@palmskog I'd a look at your experimental branch. That's much better ! Thanks !

[palmskog]

@Casteran in this case, I will probably package the branch as a sequence of smaller pull requests in the next few weeks.

Specifically, besides the above on total pre-orders, I also thought it could be a good idea to introduce an operational typeclass for comparisons:

Class Compare A := compare : A -> A -> comparison.

Class Comparable {A} (lt: relation A) (cmp : Compare A) : Prop := {
  sto :> StrictOrder lt;
  compare_correct: forall a b, CompareSpec (a = b) (lt a b) (lt b a) (compare a b);
}.

This enables using a consistent infix notation across all the comparisons between different types, e.g., x <? y or x <?> y instead of compare x y.

[Casteran]

Since the pdf is now made with Alectryon, we won't have to update too much the latex files, except for a link to Bas Spitter and van der Weegen's article (already cited, section 10.3.1, p. 202, but it's a long time I didn't re-read it).

Since I defined the ONclass much later than E0, I suspect I have proved some specific lemmas about ordinals in Cantor normal form which could have been proved for any ordinal notation. Well, to be considered later!

[palmskog]

It should be noted that there are actually serious developments based on the semibundled approach. The most well-known might be Lean's mathlib, and the mathlib authors describe their approach in a quite recent paper (page 4). However, even they typically use the decision typeclass as a parameter type and not as a member type (p. 5).

[Casteran]

Anyway, It may be interesting to document both definitions and chose one (for instance the unbundled one), using the module system to mask the other.

…

Le 31 août 2021 à 17:06, Karl Palmskog ***@***.***> a écrit : It should be noted that there are actually serious developments based on the semibundled approach, the most well-known might be Lean's mathlib, and the authors describe their approach in a quite recent paper <https://leanprover-community.github.io/papers/mathlib-paper.pdf> (page 4). However, even they typically use the decision typeclass as a parameter type and not as a member type (p. 5). — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#74 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCS4UMFLG2RRMNMFDMLT7TVY3ANCNFSM5DD52CTQ>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[palmskog]

To me, there are right now only two ways of using booleans in a disciplined way in Coq: SSReflect and the Decision typeclass. Anything else will seemingly devolve into a cascade of ad-hoc lemmas connecting boolean functions with Props. Bob Harper's comments about boolean blindness are unfortunately pertinent in many Coq projects that do not use MathComp or stdpp. Probably this can be viewed as a "cost" of moving from a non-computational logic like HOL (where bool and Prop are conflated) to a dependently typed one.

[Casteran]

When we add more stuff in hydra-gaia, it will be interesting to comment and compare both styles, and choose a style for writing bridge lemmas and their proofs.