Foreign Function Interface

• Compiler Pragmas

• Haskell FFI

  • The FOREIGN pragma

  • The COMPILE pragma

  • Using Haskell Types from Agda

  • Using Haskell functions from Agda

  • Using Agda functions from Haskell

  • Polymorphic functions

  • Level-polymorphic types

  • Handling typeclass constraints

• JavaScript FFI

Compiler Pragmas

There are two backend-generic pragmas used for the FFI:

{-# COMPILE <Backend> <Name> <Text> #-}
{-# FOREIGN <Backend> <Text> #-}

The COMPILE pragma associates some information <Text> with a name <Name> defined in the same module, and the FOREIGN pragma associates <Text> with the current top-level module. This information is interpreted by the specific backend during compilation (see below). These pragmas were added in Agda 2.5.3.

Haskell FFI

Note

This section applies to the GHC Backend.

The FOREIGN pragma

The GHC backend interprets FOREIGN pragmas as inline Haskell code and can contain arbitrary code (including import statements) that will be added to the compiled module. For instance:

{-# FOREIGN GHC import Data.Maybe #-}
{-# FOREIGN GHC
  data Foo = Foo | Bar Foo
  countBars :: Foo -> Integer
  countBars Foo = 0
  countBars (Bar f) = 1 + countBars f
#-}

The COMPILE pragma

There are four forms of COMPILE annotations recognized by the GHC backend

{-# COMPILE GHC <Name> = <HaskellCode> #-}
{-# COMPILE GHC <Name> = type <HaskellType> #-}
{-# COMPILE GHC <Name> = data <HaskellData> (<HsCon1> | .. | <HsConN>) #-}
{-# COMPILE GHC <Name> as <HaskellName> #-}

The first three tells the compiler how to compile a given Agda definition and the last exposes an Agda definition under a particular Haskell name allowing Agda libraries to be used from Haskell.

Using Haskell Types from Agda

In order to use a Haskell function from Agda its type must be mapped to an Agda type. This mapping can be configured using the type and data forms of the COMPILE pragma.

Opaque types

Opaque Haskell types are exposed to Agda by postulating an Agda type and associating it to the Haskell type using the type form of the COMPILE pragma:

{-# FOREIGN GHC import qualified System.IO #-}
postulate FileHandle : Set
{-# COMPILE GHC FileHandle = type System.IO.Handle #-}

This tells the compiler that the Agda type FileHandle corresponds to the Haskell type System.IO.Handle and will enable functions using file handles to be used from Agda.

Data types

Non-opaque Haskell data types can be mapped to Agda datatypes using the data form of the COMPILED pragma:

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A
{-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-}

The compiler checks that the types of the Agda constructors match the types of the corresponding Haskell constructors and that no constructors have been left out (on either side).

Record types

The data form of the COMPILE pragma also works with Agda’s record types:

import Agda.Builtin.List
{-# FOREIGN GHC import Data.Tree #-}
record Tree (A : Set) : Set where
  inductive
  constructor node
  field root-label : A
  field sub-forest : Agda.Builtin.List.List (Tree A)
{-# COMPILE GHC Tree = data Tree (Node) #-}

Built-in Types

The GHC backend compiles certain Agda built-in types to special Haskell types. The mapping between Agda built-in types and Haskell types is as follows:

Warning

Haskell code manipulating Agda natural numbers as integers must take care to avoid negative values.

Warning

Agda FLOAT values have only one logical NaN value. At runtime, there might be multiple different NaN representations present. All such NaN values must be treated equal by FFI calls.

Using Haskell functions from Agda

Once a suitable mapping between Haskell types and Agda types has been set up, Haskell functions whose types map to Agda types can be exposed to Agda code with a COMPILE pragma:

open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit
{-# FOREIGN GHC
  import qualified Data.Text.IO as Text
  import qualified System.IO as IO
#-}
postulate
  stdout    : FileHandle
  hPutStrLn : FileHandle → String → IO ⊤
{-# COMPILE GHC stdout    = IO.stdout #-}
{-# COMPILE GHC hPutStrLn = Text.hPutStrLn #-}

The compiler checks that the type of the given Haskell code matches the type of the Agda function. Note that the COMPILE pragma only affects the runtime behaviour–at type-checking time the functions are treated as postulates.

Warning

It is possible to give Haskell definitions to defined (non-postulate) Agda functions. In this case the Agda definition will be used at type-checking time and the Haskell definition at runtime. However, there are no checks to ensure that the Agda code and the Haskell code behave the same and discrepancies may lead to undefined behaviour.

This feature can be used to let you reason about code involving calls to Haskell functions under the assumption that you have a correct Agda model of the behaviour of the Haskell code.

Using Agda functions from Haskell

Since Agda 2.3.4 Agda functions can be exposed to Haskell code using the as form of the COMPILE pragma:

module IdAgda where
  idAgda : ∀ {A : Set} → A → A
  idAgda x = x
  {-# COMPILE GHC idAgda as idAgdaFromHs #-}

This tells the compiler that the Agda function idAgda should be compiled to a Haskell function called idAgdaFromHs. Without this pragma, functions are compiled to Haskell functions with unpredictable names and, as a result, cannot be invoked from Haskell. The type of idAgdaFromHs will be the translated type of idAgda.

The compiled and exported function idAgdaFromHs can then be imported and invoked from Haskell like this:

-- file UseIdAgda.hs
module UseIdAgda where
import MAlonzo.Code.IdAgda (idAgdaFromHs)
-- idAgdaFromHs :: () -> a -> a
idAgdaApplied :: a -> a
idAgdaApplied = idAgdaFromHs ()

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
  ioReturn : {A : Set} → A → IO A
{-# COMPILE GHC ioReturn = \ _ x -> return x #-}

In this case compiled calls to ioReturn will still have A as an argument, so the compiled definition ignores its first argument and then calls the polymorphic Haskell return function.

Level-polymorphic types

Level-polymorphic types face a similar problem to polymorphic functions. Since Haskell does not have universe levels the Agda type will have more arguments than the corresponding Haskell type. This can be solved by defining a Haskell type synonym with the appropriate number of phantom arguments. For instance:

data Either {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  left  : A → Either A B
  right : B → Either A B
{-# FOREIGN GHC type AgdaEither a b = Either #-}
{-# COMPILE GHC Either = data AgdaEither (Left | Right) #-}

Handling typeclass constraints

There is (currently) no way to map a Haskell type with type class constraints to an Agda type. This means that functions with class constraints cannot be used from Agda. However, this can be worked around by wrapping class constraints in Haskell data types, and providing Haskell functions using explicit dictionary passing.

For instance, suppose we have a simple GUI library in Haskell:

module GUILib where
  class Widget w
  setVisible :: Widget w => w -> Bool -> IO ()
  data Window
  instance Widget Window
  newWindow :: IO Window

To use this library from Agda we first define a Haskell type for widget dictionaries and map this to an Agda type Widget:

{-# FOREIGN GHC import GUILib #-}
{-# FOREIGN GHC data WidgetDict w = Widget w => WidgetDict #-}
postulate
  Widget : Set → Set
{-# COMPILE GHC Widget = type WidgetDict #-}

We can then expose setVisible as an Agda function taking a Widget instance argument:

postulate
  setVisible : {w : Set} {{_ : Widget w}} → w → Bool → IO ⊤
{-# COMPILE GHC setVisible = \ _ WidgetDict -> setVisible #-}

Note that the Agda Widget argument corresponds to a WidgetDict argument on the Haskell side. When we match on the WidgetDict constructor in the Haskell code, the packed up dictionary will become available for the call to setVisible.

The window type and functions are mapped as expected and we also add an Agda instance packing up the Widget Window Haskell instance into a WidgetDict:

postulate
  Window    : Set
  newWindow : IO Window
  instance WidgetWindow : Widget Window
{-# COMPILE GHC Window       = type Window #-}
{-# COMPILE GHC newWindow    = newWindow #-}
{-# COMPILE GHC WidgetWindow = WidgetDict #-}

We can then write code like this:

openWindow : IO Window
openWindow = newWindow         >>= λ w →
             setVisible w true >>= λ _ →
             return w

JavaScript FFI

The JavaScript backend recognizes COMPILE pragmas of the following form:

{-# COMPILE JS <Name> = <JsCode> #-}

where <Name> is a postulate, constructor, or data type. The code for a data type is used to compile pattern matching and should be a function taking a value of the data type and a table of functions (corresponding to case branches) indexed by the constructor names. For instance, this is the compiled code for the List type, compiling lists to JavaScript arrays:

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A
{-# COMPILE JS List = function(x,v) {
    if (x.length < 1) {
      return v["[]"]();
    } else {
      return v["_∷_"](x[0], x.slice(1));
    }
  } #-}
{-# COMPILE JS []  = Array() #-}
{-# COMPILE JS _∷_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-}