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.