Formal polytypic programs and proofs
File Type:
PDFItem Type:
thesisDate:
2010Author:
Access:
openAccessCitation:
Wilhelmina Johanna Verbruggen, 'Formal polytypic programs and proofs', [thesis], Trinity College (Dublin, Ireland). School of Computer Science & Statistics, 2010, pp 132Download Item:
Verbruggen, Wilhelmina_TCD-SCSS-PHD-2010-07.pdf (PDF) 860.9Kb
Abstract:
Polytypic or datatype-generic programming is a form of generic programming where we abstract over the shape of datatypes: we define functions by induction over the structure of datatypes. In this thesis we show how to formalize polytypic programming within the proof assistant Coq and show how we can do fully formal proofs over polytypic programs.
Although the formalization of polytypic functions and polytypic proofs is challenging, we provide an easy to use interface for the user which allows to define polytypic functions in a way that is familiar from Generic Haskell and makes it possible to give
straight-forward proofs of properties of polytypic functions. Formal proofs are often time consuming, but support for polytypic proofs reduces the so-called “burden of proof”. A single polytypic proof corresponds to a family of proofs, proving that the property holds for each instance of the polytypic function. To define a polytypic function, a programmer must give instances for each type constant (unit, int, sum and product) and give the type of the function when specialized to types of kind *. Given these, the function can be specialized to any datatype of any kind. We have reified the notion of a polytypic function within Coq as a datatype
PolyFn with fields for exactly these components, and programmers familiar with Generic Haskell should have little difficulty in translating their Generic Haskell definitions to Coq. Function specialization is then defined as an ordinary (dependently typed) function within Coq. It takes a PolyFn as input and returns something of the type computed by type
specialization. This can be regarded as a formal proof that term specialization is correct with respect to type specialization. The main difficulties in this part of the development were the need for impredicativity of the type associated with kind * and the absence of
universe polymorphism. Implementing polytypic programming within a dependently typed language (such as Coq) gives us some distinct advantages. Since we can formalize type specialization within the host language, we get type checking of polytypic functions virtually for free. Furthermore, since polytypic functions are represented by an ordinary datatype within the host language they are first-class citizens. We can define polytypic functions in terms
of other polytypic functions and it becomes possible to define combinators on polytypic functions.
We extend the development with polytypic properties and proofs. The structure of a polytypic proof follows the structure of a polytypic function closely: the user gives a proof for each of the type constants and gives the property for types of kind *. Like for functions, we provide a lemma that says that polytypic proofs can be specialized to arbitrary datatypes of arbitrary kinds. This can be interpreted as a formal proof that to prove a property of a polytypic function it is indeed sufficient to give the instances of the
proof for the type constants. Most problems in this part of the development stemmed from the fact that in the specialization of a polytypic proof we need to refer to the specialization of polytypic functions. A proof specialized to type T is a proof that a property holds for a particular polytypic function specialized to T. Since the definition of term specialization involves a number of type conversions, reasoning about these specialized terms involves reasoning about heterogeneous equalities. However, while our definition of proof specialization is rather involved this does not affect proofs as seen by the user. The user still only needs to provide the proofs for the type constants. These proofs are straight-forward, and it should be possible to automate them to some extent through the use of a custom tactics library. We discuss how we can deal with (co)inductive datatypes and proofs, following the same approach that is taken in Generic Haskell. Unfortunately, this requires some manual work on behalf of the programmer or the prover, and the approach is limited because of restrictions posed by the Coq guardedness checker. Nevertheless, our proof of concept demonstrates that the Generic Haskell approach is feasible in a formal setting. Making the approach more generic, or lifting the restrictions of the guardedness checker, is discussed in future work. We go on to review work related to our own. We mention a number of approaches to generic programming and explain the difference to the approach on which this thesis is based. We then compare our development to a number of other implementations of polytypic programming in dependently typed languages, and discuss some work that is of interest in improving our implementation of recursion. We can extend the work in this thesis in a number of ways. There is some scope for automation and syntactic sugar to make defining polytypic functions and proofs more
intuitive. We would like to extend the definition of polytypic properties to allow for properties about multiple polytypic functions. Other useful extensions include type-indexed types, the extraction of code to Generic Haskell and the addition of meta-information to our type universe to allow for such polytypic functions as pretty printers and parsers. We conclude that our infrastructure allows for Generic Haskell-style polytypic programming in the proof assistant Coq and that we have shown that fully formal (polytypic) proofs about these programs can be straight-forward.
Author: Verbruggen, Wilhelmina Johanna
Advisor:
Hughes, ArthurQualification name:
Doctor of Philosophy (Ph.D.)Publisher:
Trinity College (Dublin, Ireland). School of Computer Science & StatisticsNote:
TARA (Trinity's Access to Research Archive) has a robust takedown policy. Please contact us if you have any concerns: rssadmin@tcd.ieType of material:
thesisCollections:
Availability:
Full text availableLicences: