Agda - Help with importing Haskell function via FFI

Question

I'm trying out Agda's Foreign Function Interface with a simple correctness proof of quicksort (which I have defined in Haskell), but I'm having trouble importing the Haskell function. I've been working through the documentation as well as the example included in the stdlib, but I'm stuck, and neither are very helpful for diagnosing the problem.

This is my Verification/quicksort.hs:

module Quicksort (quicksort) where

quicksort :: [Integer] -> [Integer]
quicksort [] = []
quicksort (x:xs) = 
       quicksort [n | n <- xs, n < x] 
    ++ [x] 
    ++ quicksort [n | n <- xs, n >= x]

And here is my Verification/verify_quicksort.agda:

-- Please excuse all the imports
open import Agda.Builtin.List
open import Data.List using ([]; [_];_∷_; _++_; length; reverse; map; foldr; downFrom)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All)

open import Agda.Builtin.Nat
open import Data.Nat using (_≤_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                  +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)

{-------------------------------------------
  Import foreign function Quicksort 
  from quicksort.hs
--------------------------------------------}  
{-# FOREIGN GHC import Verification.Quicksort #-}

postulate
    quicksort : List Nat → List Nat

{-# COMPILE GHC quicksort = Quicksort.quicksort #-}


{-------------------------------------------
  Datatype that says list is sorted
--------------------------------------------} 
data Sorted? : List Nat → Set where
    nil : Sorted? []
    one : ∀ {x : Nat} → Sorted? [ x ]
    constr : ∀ {xs} → ∀ {x y : Nat} → 
        x ≤ y → Sorted? (y ∷ xs) → Sorted? (x ∷ y ∷ xs)

{-------------------------------------------
  The actual verification of Quicksort.
--------------------------------------------}
verify-quicksort : ∀ (xs : List Nat) → 
    (Sorted? (quicksort xs))
verify-quicksort [] = {! nil  !}
verify-quicksort (x ∷ []) = {! one  !}
verify-quicksort (x ∷ y ∷ xs) = {! constr  !}

You can see at the end that I'm trying to give nil as proof of the fact that [] is sorted, but I get the error

[] != quicksort [] of type List Nat
when checking that the expression nil has type
Sorted? (quicksort [])

So it seems like Agda is failing to reduce quicksort []. Does this mean I didn't import quicksort from Haskell properly? Or maybe I didn't import/coerce Haskell Lists correctly? (It's not clear to me from the documentation whether Haskell lists automatically get compiled as Agda lists, or if I need to do this myself.) Or maybe the way I'm doing Haskell imports isn't right... Figuring out what the issue is at all is a bit annoying, since Agda won't throw any errors for the pragmas.

Thanks!!

Answer 1

Functions do not compute across the FFI. If you want your functions to reduce at typechecking time (which is needed to prove them correct) then you will need to define them directly in Agda.

Think of the FFI as a way to give, at runtime, a computational interpretation to postulates.