Talk at AIM XXXIV

Jesper Cockx

9 June 2021

With Agda, we can write verified functional programs (hooray!)

However, not everyone uses Agda (booh!)

How can we give the benefits of verified code to those poor people??

Agda2Hs is an Agda backend that maps a **subset** of Agda to readable Haskell code.

How to use Agda2Hs:

- Write library in Agda
- Verify library in Agda
- Translate verified code to Haskell
- ???
- Profit

*How feasible is it to verify Haskell libraries using Agda2Hs?*

Sub-questions: how hard is it to…

- port Haskell code to Agda?
- state the properties and invariants?
- actually prove them?

3rd year Bsc students work on research project for 10 weeks in groups of 5.

Each student works individually on a sub-question

**In this case:** Each student works on porting and verifying one existing Haskell library with Agda2Hs.

Students had basic knowledge of Haskell + Agda from FP course, but no other previous experience.

`Data.Map`

: maps implemented as binary search trees`Data.Sequence`

: lists implemented as finger trees`Data.Graph`

: algebraic graphs implemented as patricia trees`QuadTree`

: regions of 2D space`RangedSet`

: unions of continuous ranges of numbers

There are plenty of sources for properties to prove:

- Preconditions for making partial functions total
- Pre- and post-conditions stated in comments
- Laws of type classes that are implemented
- Internal invariants documented in Haskell source
- QuickCheck properties in the source

Large and commonly used library, so it has lots of functions and low-level optimizations.

Finger trees use *heterogeneous recursion*: The type of elements changes in each step.

The `agl`

library defines both an *abstract interface* for working with algebraic graphs, and an implementation of this interface using Patricia trees.

This library relies heavily on *lenses*: functional getter/setter pairs which should satisfy a bunch of laws.

Many functions on ranged sets do not actually preserve all invariants, so the result needs to be normalised first.

- In the FP course, I introduced the predicate
`IsTrue : Bool -> Set`

. - This looks like a nice thing since you can reuse boolean functions.
- … but it’s actually a bit of a trap: you know that a boolean is true but you forget
*why*it is true.

- It is sometimes very tricky to preserve the same type signature.
- Especially for partial functions preserving the type signature is not possible or not desirable.
- Dependent types sometimes actually drive us towards more elegant type signatures!

- Proofs by the students are often very long, and contain a lot of repeated expressions and applications of
`cong`

. - It would be better to identify simple abstract properties and use those to simplify the proof.
- But this probably requires some experience to identify good auxiliary properties.

- Project is still ongoing for four more weeks, but most implementation work is done
- Students impressed me with their productivity
- ‘Simple’ techniques often do not scale
- Standard library is difficult to navigate
- Need for ‘design patterns’ for verifying code