agda2lh

§ Introduction to agda2hs

In the paper Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs
https://jesper.sikanda.be/files/reasonable-agda-is-correct-haskell.pdf
Placeholder description for https://jesper.sikanda.be/files/reasonable-agda-is-correct-haskell.pdfReasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs, the authors identify a reasonable correspondence between a subset of Agda and Haskell within which they can perform a reasonable translation from Agda to Haskell.

For example, consider the following Agda program:

-- utilities

⊔ : ℕ → ℕ → ℕ
⊔-comm : ∀ m n → m ⊔ n ≡ n ⊔ m
{-# COMPILE AGDA2HS ⊔-comm irrelevant #-}

-- Tree

data Tree (A : Set) : (@0 _ : ℕ) -> Set where
  Leaf : Tree A 0
  Branch : A → ∀ nₗ nᵣ → Tree A nₗ → Tree A nᵣ → Tree A (nₗ ⊔ nᵣ)
{-# COMPILE AGDA2HS Tree #-}

-- mirror

mirror : ∀ {A} {n} → Tree A n → Tree A n
mirror Leaf = Leaf
mirror (Branch a nₗ nᵣ tₗ tᵣ) rewrite ⊔-comm nₗ nᵣ =
  Branch a nᵣ nₗ (mirror tᵣ) (mirror tₗ)
{-# COMPILE AGDA2HS mirror #-}

Tree is indexed by its height, which is annotated by @0 as runtime-irrelevant. Without the height indexing, this Agda program could be written in Haskell as the following, which is in fact what the AGDA2HS annotations specify agda2hs to extract.

-- Tree

data Tree a where
  Leaf :: Tree
  Branch :: a -> Tree -> Tree -> Tree

-- mirror

mirror :: Tree a -> Tree a
mirror Leaf = Leaf
mirror (Branch a tl tr) = Branch a (mirror tr) (mirror tl)

Behaviorally, these programs are the same. But still something has been lost in translation.

§ Problem: Agda is more expressive than Haskell

Since Haskell does not support full dependent typing, the Haskell program above does not have the same statically-checked properties as the Agda program. In particular, the Agda mirror preserves the height of the Tree it operates on, since both the input and the output type are Trees with height index n. The Haskell mirror has no such statically-ensured property -- the Haskell Tree is not height-indexed.

Of course, one could use some advanced Haskell type features to include a sort of height-indexing into the Haskell Tree (perhaps something like -XGADTs, -XDataKinds, -XTypeFamilies). But, these sorts of techniques are clunky, hard to generalize, probably require some explicit witnesses, and, very importantly, don't interoperate well with other Haskell code that are not also using fancy GADTs with indexing.

In summary, what we are lacking is a Haskell target that maintains the static checks of the original Agda code and is still easily interoperable with normal Haskell code when desired.

§ Solution: target LiquidHaskell with agda2lh

Liquid Haskell
https://github.com/ucsd-progsys/liquidhaskell
Placeholder description for https://github.com/ucsd-progsys/liquidhaskellLiquid Haskell is a plugin to Haskell that adds automatically-checked refinement types to Haskell's type system. A refinement type is a basic Haskell type that is refined by a boolean predicate over values of the type. For example, the following function has a refined input type and a refined output type.

{-@ mulOdds :: {x:Int | (x % 2) == 1} -> {y:Int | (x % 2) == 1}
            -> {z:Int | (z % 2) == 0} @-}
mulOdds :: Int -> Int -> Int
mulOdds x y = x * y

In this way, Liquid Haskell adds lightweight dependent types to Haskell, with heavy (SMT-powered) automation for checking refinements (The proof that the product of two odds is even is not totally trivial, and the SMT solver figured it out!). Since Liquid Haskell can ensure dependent-types related properties (such as indexing of datatypes) via typechecking then perhaps we can attempt to encode the information discarded by agda2hs as Liquid Haskell refinements.

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}

-- utilities

{-@ by :: {x:a1 | b1} -> {y:a2 | b2} -> {x':a1 | (x == x') && b1 && b2} @-}

-- Nat

data Nat = Zero | Suc Nat deriving (Eq)

{-@ reflect max @-}
max :: Nat -> Nat -> N
max Zero n = n
max m Zero = m
max (Suc m) (Suc n) = Suc (max m n)

{-@ max_comm :: m:Nat -> n:Nat -> {max m n == max n m} @-}
max_comm :: Nat -> Nat -> ()
max_comm (Suc m) (Suc n) = max_comm m n
max_comm _ _ = ()

-- Tree

data Tree a = Leaf | Branch a (Tree a) (Tree a)

-- derived from indexing in definition of Agda `Tree`
{-@ reflect height @-}
height :: Tree a -> Nat
height Leaf = Zero
height (Branch _ tl tr) = max (height tl) (height tr)

-- mirror

-- preserves height of `Tree`
{-@ mirror :: t:Tree a -> {t':Tree a | height t == height t'} @-}
mirror :: Tree a -> Tree a
mirror Leaf = Leaf
mirror (Branch a tl tr) =
    Branch a (mirror tr) (mirror tl)
      `by` max_comm (height tl) (height tr)

This kind of translation required a few derivations:

• The Agda lemma ⊔-comm was translated to the Liquid Haskell lemma max_comm, which implicitly converted Agda's propositional equality _≡_ into Liquid Haskell's refinement-level decidable equality (==). This translation requires that Agda's _≡_ {ℕ} is decidable, and also the the user must specify that _≡_ is meant to be proof-irrelevant
• The Agda datatype Tree's height index is extracted to a reflected Liquid Haskell function height. This derivation is performed by inspecting the output index for each constructor of Agda's Tree.

In the same style of agda2hs, an agda2lh could be annotated like so to specify these derivations.

-- utilities

-- decidable equality over ℕ
_==_ : ∀ (m n : ℕ) → Dec (m ≡ n)
zero == zero = yes refl
zero == suc n = no λ ()
suc m == zero = no λ ()
suc m == suc n with m == n
suc m == suc n    | yes m≡n = yes (cong suc m≡n)
suc m == suc n    | no ¬m≡n = no (λ { refl → ¬m≡n refl })
-- specify that `_==_` should be used as the instance of decidable equality
-- over `ℕ` for refinement-relevant extractions
{-# COMPILE AGDA2LH _==_ REFINEMENT-EQUALITY(ℕ) #-}

⊔ : ℕ → ℕ → ℕ
⊔-comm : ∀ m n → m ⊔ n ≡ n ⊔ m
-- specify that `⊔-comm` is proof-irrelevant but refinement-relevant; uses
-- `_==_` as the instance of decidable equality in the extracted refinement, as
-- per the previous annotation
{-# COMPILE AGDA2LH ⊔-comm REFINEMENT #-}

-- Tree

data Tree (A : Set) : (@0 height : ℕ) -> Set where
  Leaf : Tree A 0
  Branch : A → ∀ nₗ nᵣ → Tree A nₗ → Tree A nᵣ → Tree A (nₗ ⊔ nᵣ)
-- specify that `Tree`'s term-irrelevant parameter `height` should be extracted
-- as an index which is kept track of by extracted refinements.
{-# COMPILE AGDA2LH Tree REFINEMENT-INDEX(height) #-}

-- mirror

mirror : ∀ {A} {n} → Tree A n → Tree A n
mirror Leaf = Leaf
mirror (Branch a nₗ nᵣ tₗ tᵣ) rewrite ⊔-comm nₗ nᵣ =
  Branch a nᵣ nₗ (mirror tᵣ) (mirror tₗ)
-- no special annotations needed here; the enforcement of `mirror` preserving
-- height is derived from the previous annotation that specifies the `height`
-- of a tree to be refinement-relevant index
{-# COMPILE AGDA2LH mirror #-}

§ References

• agda2hs
  https://jesper.sikanda.be/files/reasonable-agda-is-correct-haskell.pdf
  Placeholder description for https://jesper.sikanda.be/files/reasonable-agda-is-correct-haskell.pdfagda2hs
• Liquid Haskell
  https://github.com/ucsd-progsys/liquidhaskell
  Placeholder description for https://github.com/ucsd-progsys/liquidhaskellLiquid Haskell

§ References

• Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs
• Liquid Haskell
• agda2hs
• Liquid Haskell

§ Signature

The following code block is the Ed25519 signature of this post's markdown content encoded in base 64, using my secret key and public key.

8fb5528bd5c3b7c67b42eb6965249a80247ec8b124b4eb5ffbd6775cab7c55eb68827230a824f6b7529ee703c6458146187876f53e069043eae35f8803023f0d

See Signature for more information.