Project topics and materials
Get Complete Project Material File(s) Now! »
Canonical Structures
Tools of the Trade
Canonical Structure is the name of a command of the Gallina language1that allows a COQ user to equip the unification procedure called by type infer-ence with a specialized heuristic. When asked for a record fitting a given record projection, this heuristic answers with one of some pre-registered definitions.
Canonical Structures also are an instance of a general language construct better known as type classes whose claim to fame originated with its imple-mentation in HA S K E L L.
Canonical Structures also are an effective linguistic tool for structuring and organizing proofs — particularly when it concerns hierarchies of objects of some depth.
Finally, knowledge about the organization of such hierarchies can inform Canonical Structure use, and influence it .
THIS CHAPTER AIMS AT EXPLAINING, LINKING, AND JUSTIFY-I N G T H O S E F O U R C L A I M S. The COQ literature documents the first claim if in a haphazard and fragmented way. The second claim supplies the COQ user with the wide-ranging generic programming facilities of type classes, but has been widely overlooked nonetheless. The third claim was previously made,2 but only in the framework of the SSReflect libraries. Finally, the fourth claim is entirely original, but its smooth explanation depends on a comprehensive exposition to the three previous ones.
Model and Implementation: Σ-types and de-pendent records in COQ
THE USER OF A PROOF ASSISTANT QUICKLY DEVELOPS SOPHIS-T I C AT E D A B S T R AC T I O N N E E D S — usually faster than an alter ego who just wants to compute with some data. Such a user usually means to prove something, and the intuitiveness of abstraction for doing that means that she will probably want to reproduce the generalizations that naturally come to her on the blackboard.
Fortunately, COQ has a module system inherited from the tradition of ML-style languages that purports to do just that: it gives constructs for specifying the functionality of program components abstracting programs and proofs over that specification instantiating programs with specific realizations of these specifications.
In the last couple of decades3 such a system has proven to be an effective language tool for structuring programs.
But it turns out that one does not have to use modules. Anyone that has constructor functions that look like nil and cons can build something that looks like lists.
Record seq_type (A: Type): Type
:= mk_seq_type {
carrier : Type;
seq_nil : carrier;
seq_cons : A
carrier carrier;
}.
In COQ— since the user is here to prove something — one may want to add an induction principle to that, turning seq_type into the definition in Fig. 1.1. One can then define a generic map function as follows:
Definition map_seq_type (A: Type) (B: Type) (ltA: seq_type A)
(ltB: seq_type B) (f: A B): carrier ltA carrier ltB
:= seq_induction
ltA
(fun l : carrier ltA = > carrier ltB)
(seq_nil ltB)
(fun a :A=>
fun tailA : carrier ltA = >
fun tailB : carrier ltB = >
(seq_cons ltB) (f a) tailB).
The question of whether to use modules or records to organize a program or development thus comes up frequently. In the world of programming languages, it is a well-known observation that both mechanisms are similar, though by no means interchangeable. Wehr and Chakravarty made this precise in a detailed comparison between the two,4 and methods of imple-menting one of the mechanisms using the other abound (Dreyer et al. 2007; Oliveira 2009; Yallop 2007). For proof assistants, the situation is a tad less clear.
The Canonical Structure mechanism is, historically, an improvement on a development that took records as the main organization tool (Saibi and Huet 2000). It stemmed from the remark that in the phases we distinguished above ( on the current page) abstraction and instantiation were places where automation can help the user.
The seq above was a simple specification with no dependencies but it is nonetheless possible to define structures depending on other structures. The type parameter A above is a simple variable in the definition above, because we don’t need any more primitives to give the type of the list constructors of seq_type A. By “dependencies” we mean what happens when we need a record type in place of A, to express some of the operations this type comes with. For example, we will see how to specify an order relation as a parametric record in § 1.1.9 on p. 30: if we also want to check this relation is antisymmetric, we will have to require the record parameter to include a pointer to an equality relation in order to write that check
Thus, a structure comes along with its set of constraints. But at specifi-cation time, a user generally wants to manipulate the minimal number of abstractions needed to write his generic proof or program. He rarely wants to mention their prerequisites: in our example, it seems harsh to make him give the whole specification for an equality relation a second time when he wants to specify the record type for an order relation. We can therefore benefit from the inference of structure constraints.
– It is possible to compose instances of specifications to obtain a new in-stance of that same structure, or of another. For instance, the (categorial) product of two list types always yields a list type, or one can assemble two singly-linked lists to form a double-linked list. The composition trend can easily run wild enough in a large library that remembering how exactly a complex compound term fits a specification becomes tedious. Here the user benefits from automatic construction of instances.
Those two specific improvements upon “the record alternative” repre-sent the essence of a type class system. As I will argue based on my experi-ence with the Mathematical Components project,5 they are a necessity for developing large-scale proof libraries.
On the other hand, we do not mean that “the module alternative” is irrelevant to the world of theorem provers. It is simply less mature. For instance, early developments — either at the dawn of the Mathematical Components libraries, or at the time of Saibi and Huet’s development on category theory — had strong but external reasons for leaving modules aside.6Moreover, recent work makes the implementation of modules in COQ an improving alternative (Soubiran 2010). But I intend to show that advantages such as the automatic generation of instances, seen through the lens of the developer of large libraries of mathematics, make a particularly compelling argument for the use of Structures.
Amokrane Saibi implemented Canonical Structures in COQ version 6.1. A summary of the user-level syntax is present in the manual (Coq 2010, §2.7.15). In a technical description of the unification algorithm used in type inference (Saibi 1999, §4.5,4.7), it is possible to remark facilities for Canonical Structure inference, though there is no mention of their operative name or indications on their practical use in that document.
This section aims at describing what this mechanism is, but also at giving some perspective on where (on which terms) it operates, and when it takes effect. The where depends on how COQ represents dependent records, and on why they are an encoding of the more general abstraction known as a telescope.7 The when requires a reminder on type inference, and how it gives rise to higher-order unification problems. Finally, the section takes special interest in exposing how the user can make a complementary use of the coercion and notation mechanisms of COQ.
Σ-Types and telescopes
The first step to adopt records as an organizational basis is to see how general a construction they are. We want to develop a clear idea of what a COQ record is, and what type-theoretic notion they embody.
In type theory, the construct one should aim for to represent mathemat-ical abstractions is – fortunately – clear. Indeed, said abstractions (usually set-theoretic) are in general composed of a domain, operations on that do-main, and, if defined in a proof assistant able to represent them, properties of said operations and domain.
Meanwhile, dependent type theory8systematically defines the dependent product — a generalization of the usual function space. For instance, in COQ, a term having the type ∀x:A, P(x) consists in a procedure yielding a proof of P for all entries of type A. We call those types Π-types or dependent function types. Type theories often strive to define a similar generalization for the pair, for terms that consist of a term x, and the proof that it verifies P(x). Such terms provide a witness of a given property, thus correspond to an existential quantification, and carry a Σ-type or dependent product type.9We will come back later on how COQ represents them exactly.
Those dependent pairs are nonetheless sufficient to specify, for example, a type T and a binary operation of type (T T T) on that type: the key of the representation is simply that the type of the second element of the pair depends on the first element. But mathematical structures usually define more than simply one operation. de Bruijn noted that the repetition of that construction was the perfect way to represent mathematical structures, and baptized such an iteration of Σ-types telescopes (de Bruijn 1991).
Since then, a number of authors besides de Bruijn have confirmed that telescopes express mathematical structures ideally (Betarte and Tasistro 1998; Mu et al. 2008; Pollack 2000, 2002; Sacerdoti Coen and Tassi 2008), and the claim is now well-established. I add that, in COQ, one can use records to represent iterated Σ-types, without loss of generality. It is a frequently encountered but often imprecisely justified claim, especially since neither records nor Σ-types exist as primary constructs in the Cal-culus of Inductive Constructions, and are instead encoded using inductive types. I therefore support it by providing a formal portrait of COQ’s induc-tives.
Table of contents :
Canonical Structures
Implementation
Subfunctors of the identity
Conclusion
Bibliography
