Verifying Haskell Programs Using Constructive Type Theory

Andreas Abel  Marcin Benke  Ana Bove  John Hughes

Ulf Norell

Haskell Workshop, 2005

1 Example: Queues

A Specification of Queues

• A queue is simply a list.

type Queue a = [a]
empty         = []
add x q       = q ++ [x]
isEmpty q     = null q
front  (x:q) = x
remove (x:q) = q

• Enqueueing has linear time complexity.

• Implementation should have amortized constant time operations.

An Implementation of Queues

• A queue consists of a front list and a reversed back list.

type QueueI a = ([a],[a])
retrieve :: QueueI a -> Queue a
retrieve (f,b) = f ++ reverse b

• An data invariant:

If the front list is empty, then so is the back list.

Implementation of Queue Operations

• Auxiliary operation flipQ restores the invariant.

flipQ ([],b)     = (reverse b,[])
flipQ q          = q

• Queue operations:

emptyI           = ([],[])
addI   x  (f,b) = flipQ (f,x:b)
isEmptyI  (f,b) = null f
frontI  (x:f,b) = x
removeI (x:f,b) = flipQ (f,b)

Soundness

• Diagram should commute:

          QueueI opI QueueI Queue op Queue retrieve retrieve

• Example:

retrieve (addI x q) == add x (retrieve q)

2 From Haskell to Agda

Proofs about Haskell Programs

• We need a translation:

Haskell Agda ?

• But: Haskell is a rich language! Translation Outline

• We use GHC Core as an intermediate language.

Haskell GHC Core Agda GHC ?

• (GHC) Core = System F_{ω} + data types + mutual recursion.

• Type classes and nested patterns are translated away by GHC. Target: Agda

• Purely functional, dependently typed language.

• Propositions are sets (types): Prop = Set.

• Predicates are dependent types, e.g.:

Even : Nat → Prop
lemma : (n : Nat) → Even n → Even(n + 2)

Agda Programs Must Be... • predicative,

• terminating, • and total. Oops!

         front  (x:q) = x

• We need to translate each type A by Maybe A. A Monadic Translation

• Partiality involved? Translate A by Maybe A.

• Everything total? Translate A by A.

• Maybe is a monad.

• Identity is a monad.

• We do a monadic translation. Translation Outline (refined)

Haskell GHC Core Agda GHC

Monadic Translation

3 Monadic Translation

Monads in Agda

• An abstract monad:

m  : Set → Set
return (α:Set)  : α → m α
(≫=) (α, β:Set) : m α → (α → m β) → m β

• Arguments to the right of (:) are implicit.

Translating the λ-Calculus • Translation of types:

\begin{aligned}τ^{†} & = & m τ^{∗} \\ (α τ⃗)^{∗} & = & α τ^{∗} \\ (τ_{1} → τ_{2})^{∗} & = & τ_{1}^{†} → τ_{2}^{†} \end{aligned}

• Translation of programs (domain-free):

\begin{aligned}x^{†} & = & x \\ (λx.e)^{†} & = & return (λx. e^{†}) \\ (f e)^{†} & = & f^{†} ≫= λf′. f′ e^{†} \end{aligned}

Dealing with Polymophism

• In the literature (Barthe, Hatcliff, Thiemann 1997):

(∀α.σ)^{†} = m ((α:Set) → σ^{†})
(Λα.e)^{†} = return (λα. e^{†})

• But Agda is predicative: (α:Set) → σ is not in Set!

• However, we want to instantiate α with some m τ.

• So, m needs to be in Set → Set.

• ⟹ Polytypes are translated non-monadically. Translating Polymorphism

• Our approach:

\begin{aligned}(∀α.σ)^{†} & = & (α:Set) → σ^{†} \\ (Λα.e)^{†} & = & λα. e^{†} \end{aligned}

• Consistent with Haskell semantics:

– Type abstraction and applications are not computations, but information for the compiler.

– (Λα.⊥) = ⊥.

• We need to distinguish between monotypes and polytypes.

Translation Outline (revised)

Haskell GHC Core Pred. Core Agda GHC Preprocessor

Monadic Translation

Predicative Core

• Predicative F_{ω} (restriction of Leivant 1991):

κ ::= ∗ | κ → κ′  kinds
τ ::= α τ⃗ | τ → τ′  monotypes
σ ::= τ | ∀α:κ. σ | σ ↦ σ′ polytypes

• Translation of poly-function types (arise from dictionaries):

\begin{aligned}(σ_{1} ↦ σ_{2})^{†} & = & σ_{1}^{†} → σ_{2}^{†} \\ (λx:σ.e)^{†} & = & λx:σ^{†}. e^{†} \\ (f^{σ_{1}↦σ_{2}} e)^{†} & = & f^{†} e^{†} \end{aligned}

Translating Datatypes

• Lists …

data List α = Nil
| Cons α (List α)

• … are translated as:

data List (α:Set) = Nil
| Cons (mx :m α) (mxs :m (List α))

Demo Conclusions

• New monadic translation.

• Pragmatic approach to Haskell program verification.

• Drawbacks:

– Monads everywhere.

– GHC Core designed as frontend for compiler, not theorem prover.

• But:

– Lightweight translation (easy to get right).

– “Core-ification” preserves most names.

– Proofs about the de-facto semantics of Haskell programs.