[ 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.
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 speciﬁcation towards the algorithm. The ﬁrst 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 speciﬁcation.
The complete program is in the Example directory of the code.
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).
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.