for the few of us.

An Agda library accompanying the paper Algebra of Programming Using Dependent Types (MPC 2008) developed in co-operation with Hsiang-Shang Ko and Patrik Jansson.

Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. The AoPA library allows one to encode Algebra of Programming style program derivation, both functional and relational, in Agda.

Example

The following is a derivation of insertion sort in progress:

sort-der : ∃ ([ Val ] -> [ Val ]) (\f -> ordered? ○ permute ⊒ fun f )
sort-der = exists (
  ⊒-begin
      ordered? ○ permute
  ⊒⟨ (\vs -> ·-monotonic ordered? (permute-is-fold vs)) ⟩
      ordered? ○ foldR combine nil
  ⊒⟨ foldR-fusion ordered? ins-step ins-base ⟩
      foldR (fun (uncurry insert)) nil
  ⊒⟨ { foldR-to-foldr insert []}0 ⟩
      { fun (foldr insert [])
  ⊒∎ }1)

isort : [ Val ] -> [ Val ]
isort = witness sort-der


The type of sort-der is a proposition that there exists a program of type [ Val ] → [ Val ]that 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. The shaded areas denote interaction points — fragments of (proof ) code to be completed. The programmer can query Agda for the expected type and the context of the shaded expression. 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.

The Code

The code consists of the following files and folders:

• AlgebraicReasoning: a number of modules supporting algebraic reasoning. At present we implement our own because the PreorderReasoning module in earlier versions of the Standard Library was not expressive enough for our need. We may adapt to the new Standard Library later.
• ConvFunThm: the converse-of-a-function theorem.
• Examples: currently we have prepared two examples: a functional derivation of the maximum segment sum problem, and a relational derivation of insertion sort (following the paper Functional Algorithm Design by Richard Bird).
• Fold: a key module defining fold on lists, universal property of fold, fold-fusion theorem, etc.
• Relations: modules defining various properties of relations.
• Sets: a simple encoding of sets, upon with Relations are built.

The module Unfold is not yet complete.

Download

The library is still under development. To grab the latest code, install darcs and check our the code from the repository:

darcs get http://pc-scm.iis.sinica.edu.tw/repos/AoPA


A gzipped tarball of the latest stable release is also available.