I am trying to find my way to building hierarchies of “reusable/extensible” classes/types. I have already learned that Modules are too limited for that since every sub-module has to reimplement all members of the super-module (i.e. there is in fact no “inheritance”), and that the suggested way to go is Records or, even better, Typeclasses.
So, here is an attempt with Typeclasses and Substructuring. I am finding it quite satisfactory, but only as long as I complement it with a Coercion, otherwise I still have very clumsy accessors to any “parent” members.
But, could you please have a look at it and tell me if I am missing anything here/if there is any better approach?
Class Group : Type :=
{ G : Set
; i : G
; dot : G -> G -> G
; closure : forall a b : G, exists c : G, dot a b = c
; identity : forall a : G, dot i a = a
; inverse : forall a : G, exists a_inv : G, dot a_inv a = i
; assoc : forall a b c : G, dot a (dot b c) = dot (dot a b) c
}.
Class AbGroup : Type :=
{ AbGroup_Group :> Group
; commut : forall a b : G, dot a b = dot b a
}.
Section Examples_Zadd.
Require Import ZArith.
Open Scope Z_scope.
Local Lemma Z_add_closure :
forall a b : Z, exists c : Z, a + b = c.
Proof.
intros a b.
exists (a + b).
reflexivity.
Qed.
Local Lemma Z_add_inverse :
forall a : Z, exists a_inv : Z, a_inv + a = 0.
Proof.
intros a.
exists (- a).
rewrite Z.add_comm.
rewrite Z.add_opp_diag_r.
reflexivity.
Qed.
Local Instance Zp_ : Group :=
{ G := Z
; i := 0
; dot := Z.add
; closure := Z_add_closure
; identity := Z.add_0_l
; inverse := Z_add_inverse
; assoc := Z.add_assoc
}.
Local Instance Zp : AbGroup :=
{ AbGroup_Group := Zp_ (* fix instance *)
; commut := Z.add_comm;
}.
Check Zp.(AbGroup_Group).(G). (* OK *)
Fail Check Zp.(G).
(* The command has indeed failed with message:
The term "Zp" has type "AbGroup"
while it is expected to have type "Group". *)
Local Coercion AbGroup_to_Group (g : AbGroup) : Group :=
match g with {| AbGroup_Group := g' |} => g' end.
Check Zp.(G). (* OK! *)
End Examples_Zadd.
A hierarchy of classes, not of interfaces otherwise modules would already have been enough. I don’t like Hierarchy Builder, way too complicated, I am looking at the opposite of that spectrum, I just want to find out how to do some real programming in Coq but without requiring a million lines of code to just do most basic things like a little bit of code structuring… – TL;DR Thanks for the reply and link, Enrico, indeed I’ll keep investigating.
I am sorry, I am really asking basic questions: maybe I should be saying I am learning how to use a functional language proper, though my interest is really in applications to software production.
Indeed, about building blocks: eventually it’s dawning on me that it’s coercions that are the fundamental tool for reuse/extensibility here (while modules are the fundamental tool for scoping)…
The unbundled approach is known to have scalability issues […] but to my knowledge provides more automation.
Indeed, an exponential blow-up in the size of terms is simply not acceptable, given that in any real program these hierarchies may get to be dozens of layers deep and more.
That said, I am too new to Coq and related to yet draw judgment, but I am having a hunch that (for historical and perhaps even very good reasons, since SE is simply not CS/maths) we don’t just have different terminologies (I wouldn’t call that “automation” for example), we really have a case of opposite requirements: in software production we want things basic and explicit and staying in control (I’d even switch type inference off if I could find a flag for that), so that even with abstraction we are very careful and parsimonious…
At this point, I am even dissing typeclasses: records are fine, I do not want “automatic resolution” of anything (not per chance I had “fixed the instance” in my example code above), parametric (up to the dependently typed, I mean) seems to be all I need and want to go as abstract as I may need…
One issue with this approach will occur when you have to close a diamond in your hierarchy. Let us suppose you also have CdGroup that derives from Group, and now you want to define AbcdGroup which derives from both AbGroup and CdGroup. If you do the following, you lose, due to the duplication of the underlying Group:
So, it is important to split AbGroup (and CdGroup) into two parts, so that you can do:
Record AbAxioms G dot := {
commut : forall a b : G, dot a b = dot b a
}.
Record AbGroup := {
AbGroup_Group :> Group ;
AbGroup_axioms :> AbAxioms G dot
}.
Record AbcdGroup := {
AbcdGroup_Group :> Group ;
AbcdGroup_AbAxioms : AbAxioms G dot
AbcdGroup_CdAxioms : CdAxioms G ...
}.
Group itself could be split into parts, but since it is at the bottom of your hierarchy, this is kind of useless. Also, the whole splitting is only useful if you have a diamond in your hierarchy. If you are sure there won’t be, it is not needed.
It’s a steep learning curve: just, for a little piece of feedback, I find the main and possibly only difficulty is that the documentation is just not (yet?) up to the task… (I could expand on this in another thread if of interest.) Indeed, back to the present problem, I’ll keep investigating…
Thanks to those who have replied, that was/is very useful.
