Context
I am a relatively new user to Coq with a decent understanding of the basics of dependent type theory and am midway through chapter 2 of the Software Foundations Series of books. I want to start writing projects at a larger scale, and as such have stumbled upon the problem of how to properly package the mathematical theories and structures at scale.
In part of my research into this problem I found this promising paper Packaging Mathematical Structures that claims to give methodology for doing just that. The methodology it uses defines structures in three Layers:
- First is to define a bunch of mixins of type
(M:Type -> Type)that implement certain substructuresM sof a mathematical structure for a given sort/carrier types :Type. (for example in the text one examines mix-ins for a equality structure and that of a Z-module).
2.These are then bundled together to form "classes" which are (C:Type -> Type) which packages together for any sort s:Type a structure type/record of the form {M1 s; M2 s;....} for Mi mix-ins that encodes all the extra structure over s.
- Finaly there are "types" which represent the complete packaged mathematical structure
in question which consists of a record type of the form
{sort :> Type; class :> C sort; _:Type}that gives the underlying sort plus the "class" structure adorned atop it as the first two projections. Together these two projections can define the formalization of an algebraic structure (or perhaps more generally some kind of analogue to an object of concrete category), which is what we wanted. The third anonymous projection is what my question is about. It is not well explained in the text, at least from my point of view.
For context heree is the main example structure layed out as per the text which defines a Z-module structure based on that of a class that defines an equality structure by reflection:
Record mixin_of (T : Type) : Type := ...
Record class_of (T : Type) : Type :=
Class {base :> Equality.class_of T; ext :> mixin_of T}.
Structure type : Type :=
Pack {sort :> Type; class : class_of sort; _ : Type}.
Definition unpack K (k : forall T (c : class_of T), K T c) cT :=
let: Pack T c _ := cT return K _ (class cT) in k _ c.
Definition pack :=
let k T c m := Pack (Class c m) T in Equality.unpack k.
Coercion eqType cT := Equality.Pack (class cT) cT.
End Zmodule.
Notation zmodType := Zmodule.type.
Notation ZmodType := Zmodule.pack.
Canonical Structure Zmodule.eqType.
Question
What is the purpose of this third projection? Reading through the text I see that is maybe meant to represent something refereed to by or linked with the text as a a "head" constant - or at least related to the problem of type coercion. The text introduces the notion of head constant when taking about packaging structures by "telescoping" (of which the packaging structure laid out above is seen as a refinement / generalization of) where it discusses such a notion. Before looking into this packaging problem I had not come upon the concept of a "head constant" in the vernacular surrounding algebraic-structures / universal algebra so I assume that the notion of a "head constant" is something that is domain specific to formalizing mathematics electronically. Alternatively it could be used for something completely different and I have gotten the wrong end of the stick. The text makes no explicit inference to the nature of this projection and I am left to try and figure out from inferring from the surrounding context.
To try to figure out what is going on I dove into one of the referenced texts on "telescoping" Telescopic Mappings in Typed Lambda Calculus, but I could not intuitively relate the formalism laid down there with the context of the original paper - and so this was no help to me. I went one step further and looked at texts referenced in that paper, also to no avail.
Currently, from my (admittedly extremely ignorant) point of view this third projection seems like a useless spandrel that serves no purpose and just adds an arbitrary type into the mix of ones considerations. This is further evidenced by the fact that unpack, which is meant to be used as a dependent destructor for type essentially works by simply throwing away this hidden third argument! Also in all the examples given this third type is always given to that of the same type of the sort - so I see no generalizing benefit either. Being that taxonomising structures is an important design decision in any large scale formalization project I assume that some of the members here may have insight into why this design decision was made?
P.S. I realize the problem that I am trying to solve / methodology I am trying to understand is to do with the specific problem of doing "the plumbing" of concepts in a proof assistant, but trying to find the answer to my question has lead me to look over some nontrivial mathematics. I'm posting here and not, say, maths-stackexchange because I'm coming at it from a proof assistant usage point-of-view and not a mathematical theory point-of-view. the What topics can I ask about here? section of the wiki is currently a stub and it seems according to the Meta that the exact boundires of what questions can be asked here are still being felt out. I understand if this needs to get moved elsewhere.
HB.xxxdefined by the tool. $\endgroup$