[ Project Site|Code Repository ]
The AoPA library allows one to encode Algebra of Programming style program derivation, both functional and relational, in Agda.
Since the 90s, the program derivation community has been exploring moving from functions to a relational theory of program calculation, culminating in the work of Bird and de Moor. A problem is specified as a relation that maps inputs to outputs, which allows us not to be over specific about which output to choose when they are equally good, leaving the choices to implementations. The task is to refine the specification into a functional implementation, using algebraic properties.
Meanwhile, the programming language community has been moving toward more reliance on machine-aided program verification. Complex theorems are considered "proved" only if the proof is verified by a theorem prover or a proof assistant.
AoPA allows us to to develop relational proofs, in Agda, in the style of Bird and de Moor. Elements of the relational theory of programs are modelled in the type system of Agda. Calculations are expressed as program terms that, if type-checked, is guaranteed to be correct. In the end of a calculation one may extract a functional program that is proved to respect the relational specification.
Example
The following is a derivation of insertion sort:
isort-der : ∃ (\f -> ordered? ○ permute ⊒ fun f )
isort-der = (_ ,
(⊒-begin
ordered? ○ permute
⊒⟨ ○-monotonic-r permute-is-fold ⟩
ordered? ○ perm
⊒⟨ ⊒-refl ⟩
ordered? ○ foldR combine nil
⊒⟨ foldR-fusion-⊒ ordered? ins-step ins-base ⟩
foldR (fun (uncurry insert)) nil
⊒⟨ foldR-to-foldr insert [] ⟩
fun (foldr insert [])
⊒∎))
The type of sort-der is a proposition that there exists a function f which, after being lifted to a relation by fun, is contained in ordered ? ◦ permute , a relation mapping a list to one of its ordered permutations. The proof proceeds by derivation from the specification towards the algorithm. The first step exploits monotonicity of ◦ and that permute can be expressed as a fold. The second step makes use of relational fold fusion. When the proof is completed, an algorithm isort is obtained by extracting the witness of the proposition. It is an executable program that is backed by the type system to meet the specification.
The complete program is in the Example directory of the code.
History
AoPA (Algebra of Programming in Agda) started as an Agda library accompanying the JFP paper Algebra of programming in Agda: dependent types for relational program derivation by Shin-Cheng Mu, Hsiang-Shang Ko and Patrik Jansson. (The JFP paper is an extended version of the earlier MPC paper: Algebra of Programming Using Dependent Types (MPC 2008) by the same authors.)
The development is currently picked up by Yu-Hsi Chiang and Shin-Cheng Mu. New additions include universe polymorphism, generic datatypes with polymorphic base functors, and theories for developing algorithms from Galois connections (see Chiang and Mu 2015).
Download
The library is still under development. Grab the latest code from the Git Repository.
MSc thesis project
Extending, improving and applying the AoPA code base to some interesting algorithm could make a good MSc thesis topic for an ambitious student with a background in Advanced Functional Programming and Types for Programs and Proofs. In Gothenburg, contact Patrik Jansson or Jean-Philippe Bernardy if you are interested. Link to other FP-related MSc thesis proposals.