Foreign Function Interface

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

The FFI is controlled by four pragmas:

• IMPORT
• COMPILED_TYPE
• COMPILED_DATA
• COMPILED

The IMPORT pragma

  {-# IMPORT HsModule #-}

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

  import qualified HsModule

IMPORT pragmas can appear anywhere in a file.

The COMPILED_TYPE pragma

  {-# COMPILED_TYPE D HsType #-}

The COMPILED_TYPE pragma tells the compiler that the postulated Agda type D corresponds to the Haskell type HsType. This information is used when checking the types of COMPILED functions and constructors.

The COMPILED_DATA pragma

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

The COMPILED_DATA pragma tells the compiler that the Agda datatype D corresponds to the Haskell datatype HsD and that its constructors should be compiled to the Haskell constructors HsC1 .. HsCn. The compiler checks that the Haskell constructors have the right types and that all constructors are covered.

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 the compiler to compile the postulated function f to the Haskell Code HsCode. HsCode can be an arbitrary Haskell term of the right type. This is checked by translating the given Agda type of f into a Haskell type (see Translating Agda types to Haskell) and checking that this is the type of HsCode.

Example:

  postulate String : Set
  {-# BUILTIN 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.

Translating Agda types to Haskell

When checking the type of COMPILED function f : A, the Agda type A is translated to a Haskell type TA and the Haskell code Ef is checked against this type. The core of the translation on kinds K[[M]], types T[[M]] and expressions E[[M]] is:

    K[[ Set A ]] = *
    K[[ x As ]] = undef
    K[[ fn (x : A) B ]] = undef
    K[[ Pi (x : A) B ]] = K[[ A ]] ->  K[[ B ]]
    K[[ k As ]] =
      if COMPILED_TYPE k
      then *
      else undef

    T[[ Set A ]] = Unit
    T[[ x As ]] = x T[[ As ]]
    T[[ fn (x : A) B ]] = undef
    T[[ Pi (x : A) B ]] =
      if x in fv B
      then forall x . T[[ A ]] -> T[[ B ]]
      else T[[ A ]] -> T[[ B ]]
    T[[ k As ]] =
      if COMPILED_TYPE k T
      then T T[[ As ]]
      else if COMPILED k E
      then Unit
      else undef

    E[[ Set A ]] = unit
    E[[ x As ]] = x E[[ As ]]
    E[[ fn (x : A) B ]] = fn x . E[[ B ]]
    E[[ Pi (x : A) B ]] = unit
    E[[ k As ]] =
      if COMPILED k E
      then E E[[ As ]]
      else runtime-error

The T[[ Pi (x : A) B ]] case is worth mentioning. Since the compiler doesn’t erase type arguments we can’t translate (a : Set) → B to forall a. B — an argument of type Set will still be passed to a function of this type. Therefore, the translated type is forall a. () → B where the type argument is assumed to have unit type. This is safe since we will never actually look at the argument, and the compiler compiles types to ().