FFI

Agda has a very simple foreign function interface for calling Haskell functions from Agda. Foreign functions are only executed in compiled programs (by the Alonzo and MAlonzo compilers), and do not reduce during type checking or interpretation.

The FFI is controlled by three pragmas:

• IMPORT
• COMPILED_DATA
• COMPILED

The IMPORT pragma

  {-# IMPORT HsImport #-}

The IMPORT pragma instructs Alonzo to generate a Haskell import statement in the compiled code. The pragma above will generate the Haskell code

  import HsImport

Imports are not restricted to just a module name, but can use the full language of Haskell imports. For instance,

  {-# IMPORT qualified Data.Map as Map #-}

IMPORT pragmas can appear anywhere in a file.

The COMPILED_DATA pragma

  {-# COMPILED_DATA D HsC1 .. HsCn #-}

The COMPILED_DATA pragma tells Alonzo that the constructors of the Agda datatype D should be compiled to the Haskell constructors HsC1 .. HsCn. These should be the constructors of an existing Haskell datatype with types matching the types of the constructors of D. This is not checked by the compiler.

Example:

  data List (A : Set) : Set where
    []   : List A
    _::_ : A -> List A -> List A

  {-# COMPILED_DATA List [] (:) #-}

The COMPILED pragma

  {-# COMPILED f HsCode #-}

The COMPILED pragma tells Alonzo to compile the postulated function f to the Haskell Code HsCode. HsCode can be an arbitrary Haskell term of the right type. No checking is performed on the Haskell code.

Example:

  postulate String : Set
  {-# BUILTIN STRING String #-}
  {-# COMPILED_TYPE String String #-}

  data Unit : Set where unit : Unit
  {-# COMPILED_DATA Unit () () #-}

  postulate
    IO       : Set -> Set
    putStrLn : String -> IO Unit

  {-# COMPILED_TYPE IO IO #-}
  {-# COMPILED putStrLn putStrLn #-}

Polymorphic functions

Agda is a monomorphic language, so polymorphic functions are modeled as functions taking types as arguments. These arguments will be present in the compiled code as well, so when calling polymorphic Haskell functions they have to be discarded explicitly. For instance,

  postulate
    map : {A B : Set} -> (A -> B) -> List A -> List B

  {-# COMPILED map (\_ _ -> map) #-}

In this case compiled calls to map will still have A and B as arguments, so the compiled definition ignores its two first arguments and then calls the polymorphic Haskell map function.

Overloaded functions

Agda does not support overloading, so foreign calls to overloaded functions have to be made at specific instances. Due to the way the compiler is implemented the Haskell type checker will not be able to infer what these instances are, so when calling an overloaded function we have to be explicit about the type it is called at. For instance,

  postulate
    IO : Set -> Set
    _>>=_ : {A B : Set} -> IO A -> (A -> IO B) -> IO B

  {-# COMPILED _>>=_ (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}