\begin{comment}
\begin{code}
module Compiling where
\end{code}
\end{comment}

This section deals with the topic of getting Agda programs to interact with
the real world. Type checking Agda programs requires evaluating arbitrary
terms, ans as long as all terms are pure and normalizing this is not a problem, but
what happens when we introduce side effects? Clearly, we don't want side effects
to happen at compile time. Another question is what primitives the language should
provide for constructing side effecting programs. In Agda, these problems are solved
by allowing arbitrary Haskell functions to be imported as axioms. At compile time,
these imported functions have no reduction behaviour, only at run time is the
Haskell function executed.

\subsection{Relating Agda types to Haskell types}

In order to be able to apply arbitrary Haskell functions to Agda terms we need
to ensure that the run time representation of the Agda terms is the same as what
the function expects. To do this we have to tell the Agda compiler about the
relationships between our user defined Agda types and the Haskell types used by
the imported functions. For instance, to instruct the compiler that our {\tt Unit}
type should be compiled to the Haskell unit type {\tt ()} we say

\begin{code}
data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}
\end{code}

The {\tt COMPILED\_DATA} directive takes the name of an Agda datatype, the name of the
corresponding Haskell datatype and its constructors. The compiler will check that the
given Haskell datatype has precisely the given constructors and that their types match
the types of the corresponding Agda constructors. Here is the declaration for the maybe
datatype:

\begin{code}
data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A -> Maybe A

{-# COMPILED_DATA Maybe Maybe Nothing Just #-}
\end{code}

Some types have no Agda representation, simply because they are abstract Haskell types
exported by some library that we want to use. An example of this is the {\tt IO} monad.
In this case we simply postulate the existence of the type and use the {\tt COMPILED\_TYPE}
directive to tell the compiler how it should be interpreted.

\begin{code}
postulate IO : Set -> Set
{-# COMPILED_TYPE IO IO #-}
\end{code}

The first argument to {\tt COMPILED\_TYPE} is the name of the Agda type and the second is
the corresponding Haskell type.

\subsection{Importing Haskell functions}

Once the compiler knows what the Agda type corresponding to
a Haskell type is, we can import Haskell functions of that type. For instance, we can
import the {\tt putStrLn} function to print a string\footnote{The string library contains
the compiler directives for how to compile the string type.} to the terminal.

\begin{code}
open import Data.String

postulate
  putStrLn : String -> IO Unit

{-# COMPILED putStrLn putStrLn #-}
\end{code}

Just as for compiled types the first argument to {\tt COMPILED} is the name of the Agda
function and the second argument is the Haskell code it should compile to. The compiler
checks that the given code has the Haskell type corresponding to the type of the Agda
function.

\subsection{Our first program}

This is all we need to write our first complete Agda program. Here is the {\tt main} function:

\begin{code}
main : IO Unit
main = putStrLn "Hello world!"
\end{code}

To compile the program simply call the command-line tool with the {\tt --compile} (or {\tt -c})
flag. The compiler will compile your Agda program and any Agda modules it imports to Haskell
modules and call the Haskell compiler to generate an executable binary.

\subsection{Haskell module imports}

In the example above, everything we imported was defined in the Haskell prelude so there was no
need to import any additional Haskell libraries. This will not be the case in general -- for instance,
you might write some Haskell code yourself, defining Haskell equivalents of some of
your Agda datatypes. To import a Haskell module there is an {\tt IMPORT} directive, which has the
same syntax as a Haskell import statement. For instance, to import a function to print a string to
standard error, we can write the following:

\begin{code}
{-# IMPORT System.IO (hPutStrLn, stderr) #-}

postulate printError : String -> IO Unit
{-# COMPILED printError (hPutStrLn stderr) #-}
\end{code}

\subsection{Importing polymorphic functions}

As we saw in Section~\ref{DependentTypes} in Agda polymorphic functions are modeled by functions
taking types as arguments. In Haskell, on the other hand, the type arguments of a polymorphic
functions are completely implicit. When importing a polymorphic Haskell function we have
to keep this difference in mind. For instance, to import {\em return} and {\em bind} of the IO
monad we say

\begin{code}
postulate
  return : {A : Set} -> A -> IO A
  _>>=_  : {A B : Set} -> IO A -> (A -> IO B) -> IO B

{-# COMPILED return (\a -> return) #-}
{-# COMPILED _>>=_  (\a b -> (>>=)) #-}
\end{code}

Applications of the Agda functions {\tt return} and {\tt \_>>=\_} will include the type arguments,
so the generated Haskell code must take this into account. Since the type arguments are only there
for the benefit of the type checker, the generated code simply throws them away.

\subsection{Exercises}

\NewExercise{Turn the type checker for λ-calculus from Section~\ref{Views} into a complete program
that can read a file containing a raw λ-term and print its type if it's well-typed and an error
message otherwise. To simplify things you can write the parser in Haskell and import it into the
Agda program.
}