\section{Motivation and Examples}
\label{sect.motivation}

A typical implementation of an embedded domain specific language consists of some combinators to construct an abstract syntax tree, and some functionality in the host language to manipulate this abstract syntax tree. After analysis and transformation, the abstract syntax tree is translated to some denotation in the host language in order to use it.

For example, assume that we use Haskell as a host language and embed an expression language containing only tuples and numbers, using the following abstract syntax:

\begin{code}
data Expr
  =  Num  Int
  |  Tup  Expr Expr
\end{code}

However, the following straightforward translation of the expression to a tuple in the host language does not type check, because the inferred types for the case alternatives are not the same:

\begin{code}
eval e =  case e of
          ^^^^  Num i    -> i
          ^^^^  Tup p q  -> (eval p, eval q)
\end{code}

We can bypass this restriction imposed by the Haskell type system by using a typed abstract syntax and encode a proof that the generated tuples are type correct. For that, we add a type parameter |t| to the abstract syntax, which represents the type of the expression, and embed in the constructors a proof (with type |Equal t t'|) that states that this |t| is equal to the real type |t'| of this specific expression (an |Int| for a |Num| and some tuple type for a |Tup|):

\begin{code}
data Expr t
  =                  Num  (Equal t Int)    Int
  |  forall a b dot  Tup  (Equal t (a,b))  (Expr a) (Expr b)
\end{code}

Baars et al.~\cite{baars02} give a definition of this |Equal| data type and some operations, including a function |coerce| that converts the type to a proved equivalent type, and some combinators to construct equality proofs:

\begin{code}
coerce  :: Equal a b -> a -> b
sym     :: Equal a b -> Equal b a
refl    :: Equal a a
\end{code}

Now, we can modify the |eval| function in such a way that the case alternatives have the same type (namely the |t| in |Expr t|):

%format sym = "sym"
\begin{code}
eval :: Expr t -> t
eval e =  case e of
          ^^^^  Num  ass i    -> coerce (sym ass) i
          ^^^^  Tup  ass p q  -> coerce (sym ass) (eval p, eval q)
\end{code}

The assumptions used by |eval| need to be proved when constructing values of type |Expr t|, which we achieve by using |refl|:

\begin{code}
Tup refl (Num refl 4) (Num refl 2) ^^^^ :: Expr (Int,Int)
\end{code}

The important observation to make at this point is that the proofs are a \emph{static} property of the program. Hence, the goal is to construct these proofs automatically, at those places explicitly indicated by the programmer using type signatures. In case of the example, at those places where the type |t| shows up.

In order not to tie ourselves to Haskell or to a specific implementation of a type system, we use as source language an explicitly typed lambda calculus, called \SystemFA~\cite{sulzmann07}, where the equalities are not encoded as values, but with qualified type notation similar to Stuckey et al.~\cite{stuckey05}:

\begin{code}
data Expr t =
  |                  (t =*= Int)    => Val Int
  |  exists a b dot  (t =*= (a,b))  => Tuple (Expr a) (Expr b)
;  let (eval :: forall t dot Expr t -> t)
        = \\t -> \(e :: Expr t) ->
            ( case e of
                Num (x :: Int)  -> x
                (Tup p q) a b   -> (,) (eval a p) (eval b q)
            ) :: t
   in eval (Tup (Num 4) (Num 2))
\end{code}

Similarly, instead of translating to Haskell, we translate to an explicitly typed lambda calculus with native support for equality proofs, called \SystemFC~\cite{sulzmann07}:

%format sym = "\mathtt{sym}"
\begin{code}
data Expr t =
  |                  Num  (t ~ Int)    Int
  |  exists a b dot  Tup  (t ~ (a,b))  (Expr a) (Expr b)
;  let (eval :: forall t dot Expr t -> t)
        = \\t -> \(e :: Expr t) ->
            ( case e of
                Num   eqInt (x :: Int)  -> x                          :> sym eqInt
                (Tup  eqTup p q) a b    -> (,) (eval a p) (eval b q)  :> sym eqTup
            ) :: t
   in eval (Tup (Int,Int) (Num Int 4) (Num Int 2))
\end{code}

Each constructor contains equality proofs of type |t1 ~ t2| (a proof that |t1| and |t2| are equal), called \emph{coercions}, which can be used after pattern matching on them. The |:>| operator corresponds with the |coerce| function given above. Note that |sym| in this case is not a function, but a construction in the target language that operates on coercions, and that a type |t| as coercion represents the reflexivity |t ~ t|.

A specification for GADTs consists of two parts: a type system for the source language (\Sect{sect.typesystem}), and a translation that constructs the equality proofs and inserts the coercions (\Sect{sect.translation}).


%if False

Deliverables: type system, and translation
Question: type rules do only specify when a coercion is needed; do not specify
  where to insert a coercion. That is up to an implementation. We do make
  explicit where to 

\begin{code}
data Expr t
  =                  Num  (t ~ Int)    Int
  |  forall a b dot  Tup  (t ~ (a,b))  (Expr a) (Expr b)
; let (eval :: forall t dot Expr t -> t)
        = \\t -> \(e :: Expr t) ->
            ( case e of
                Num eqInt (x :: t)  -> x |> sym eqInt
                (Tup eqTup p q) a b -> (,) (eval a p) (eval b q) |> sym eqTup
            ) :: t
\end{code}

Alternatively, assume that the evaluation function is lifted to some monad.

\begin{code}
data Expr t
  =  Val (t ~ Int) t
  |  forall a b dot Tuple (t ~ (a,b)) (Expr a) (Expr b)
; let (eval :: forall t m dot Monad m => Expr t -> m t)
        = \\t m -> \(e :: Expr t) ->
            ( case e of
                Val eqInt (x :: t) -> return m (x |> sym eqInt)
                (Tuple eqTup p q) a b -> do p' <- eval m a p
                                            q' <- eval m a q
                                            return m ((,) (eval a p) (eval b q) |> sym eqTup)
            ) :: m t
\end{code}

%endif