# Compilers¶

See also Foreign Function Interface.

## Backends¶

### GHC Backend¶

The GHC backend translates Agda programs into GHC Haskell programs.

#### Usage¶

The backend can be invoked from the command line using the flag
`--compile`

:

```
agda --compile [--compile-dir=<DIR>] [--ghc-flag=<FLAG>] <FILE>.agda
```

#### Pragmas¶

#### Example¶

The following “Hello, World!” example requires some Built-ins and uses the Foreign Function Interface:

```
module HelloWorld where
open import Agda.Builtin.IO
open import Agda.Builtin.Unit
open import Agda.Builtin.String
postulate
putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}
{-# COMPILE GHC putStrLn = Text.putStrLn #-}
main : IO ⊤
main = putStrLn "Hello, World!"
```

After compiling the example

```
agda --compile HelloWorld.agda
```

you can run the HelloWorld program which prints `Hello, World!`

.

### JavaScript Backend¶

The JavaScript backend translates Agda code to JavaScript code.

#### Usage¶

The backend can be invoked from the command line using the flag
`--js`

:

```
agda --js [--compile-dir=<DIR>] <FILE>.agda
```

## Optimizations¶

### Builtin natural numbers¶

Builtin natural numbers are represented as arbitrary-precision integers. The builtin functions on natural numbers are compiled to the corresponding arbitrary-precision integer functions.

Note that pattern matching on an Integer is slower than on an unary natural number. Code that does a lot of unary manipulations and doesn’t use builtin arithmetic likely becomes slower due to this optimization. If you find that this is the case, it is recommended to use a different, but isomorphic type to the builtin natural numbers.

### Erasable types¶

A data type is considered *erasable* if it has a single constructor whose
arguments are all erasable types, or functions into erasable types. The
compilers will erase

- calls to functions into erasable types
- pattern matches on values of erasable type

At the moment the compilers only have enough type information to erase calls of top-level functions that can be seen to return a value of erasable type without looking at the arguments of the call. In other words, a function call will not be erased if it calls a lambda bound variable, or the result is erasable for the given arguments, but not for others.

Typical examples of erasable types are the equality type and the accessibility predicate used for well-founded recursion:

```
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
data Acc {a} {A : Set a} (_<_ : A → A → Set a) (x : A) : Set a where
acc : (∀ y → y < x → Acc _<_ y) → Acc _<_ x
```

The erasure means that equality proofs will (mostly) be erased, and never looked at, and functions defined by well-founded recursion will ignore the accessibility proof.