\section{Introduction to \GADTs}
\label{sect.motivation.introduction}

We start this section with an introduction to \GADTs. 
GADTs, combined with the Haskell class system,
form an essential ingredient for many Haskell libraries.
In this section, we picked two simplified examples as
illustration.

\subsection{Typed Abstract Syntax}
\label{sect.typed.abstract}

One popular use of GADTs is related to the embedding of domain-specific languages in such a way that Haskell's type system can be used to type check the domain-specific language.

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}

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                   -- expected: Int
          ^^^^  Tup p q  -> (eval p, eval q)    -- expected: (a,b)
\end{code}

We bypass this restriction imposed by the Haskell type system with 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}

\citet{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
hsym     :: Equal a b -> Equal b a
refl     :: Equal a a
trans    :: Equal a b -> Equal b c -> Equal a c
congr    :: Equal a b -> Equal (f a) (f b)  -- has a more general signature 
subsum   :: Equal (f a) (f b) -> Equal a b  -- than written here
\end{code}
A non-bottom value with the type |Equal ty1 ty2| is a proof that the types |ty1| and |ty2| are equal.
The |coerce| function applied to such a proof is technically the identity function.

As a hypothetical example, consider the proof |p1| out of assumptions |a1| and |a2|:
\begin{code}
a1 :: Equal v1 (Int, v2)
a2 :: Equal v1 (v3, v4)
^^^
p1 :: Equal (Int, v2) (v3, v4)
p1 = trans (hsym a1) a2
^^^
p2 :: Equal (Int,v4) (v3,v2)
p2 = ... congr ... subsum ...
\end{code}

We continue with the running example in this section and
modify the |eval| function such that the case alternatives have the same type, namely the |t| in |Expr t|:

\begin{code}
eval :: Expr t -> t
eval e =  case e of
          ^^^^  Num  ass i    -> coerce (hsym ass) i
          ^^^^  Tup  ass p q  -> coerce (hsym 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.

GHC, the mainstream compiler for Haskell, has built-in support for GADTs.
It offers two ways of writing GADTs. One can use qualified type notation, which resembles
the example above. Instead of an additional field of the type |Equal|, we write an equality constraint:
\begin{code}
data Expr t
  =                (t ~ Int)     => Num Int
  |  forall a b .  (t ~ (a, b))  => Tup (Expr a) (Expr b)
\end{code}
Aternatively, one can use special notation for GADTs:
\begin{code}
data Expr t where
  Num :: Int -> Expr Int
  Tup :: Expr a -> Expr b -> Expr (a,b)
\end{code}
These two forms of notation are interchangeable. To convert from the above qualified-type notation
to GADT notation, turn each equality constraint into a substitution and apply it exhaustively to the
type signature of the constructor. The other way around, given a type siganture of the constructor,
take the result type as written (e.g. |Expr (a, b)|), and match it against the actual result type
(|Expr t|).

Proofs do not have to be written manually. These are automatically constructed by GHC.
The |eval| function can simply be written using either function alternatives
or a case expression:
\begin{code}
eval :: Expr t -> t
eval (Num i)    = i
eval (Tup p q)  = (eval p, eval q)
\end{code}
GHC (version 6.12.1) requires the type signature to be given.
We discuss in Section~\ref{sect.motivation.inference} if this type signature could be inferred and
if it is desirable to do so.

\subsection{Generic Programming}

\citet{Cheney03first-classphantom} show how GADTs, called
Phantom Types in their work, can be used to implement generic functions
that work for many data types.
The idea is to have a representation of types as a first class value,
then use this representation to navigate generically over a particular
value:
\begin{code}
data Rep t where
  RInt   :: Rep Int
  RChar  :: Rep Char
  RList  :: Rep a -> Rep [a]
  RTup   :: Rep a -> Rep b -> Rep (a,b)

x :: [(Int,Char)]  ^^^^  r :: Rep [(Int,Char)]
x = [(3, '4')]     ^^^^  r = RList (RTup RInt RChar)
\end{code}
In this example, |x| is a value of some type, and |r| is a
value of a representation of that type.

The following function, for example, traverses a value of any
type for which we have a representation, and increments all
integers with one:
\begin{code}
replace :: Rep t -> t -> t
replace RInt        x      = x + 1
replace RChar       c      = c
replace (RList r)   xs     = map (replace r) xs
replace (RTup a b)  (p,q)  = (replace a p, replace b q)
\end{code}
Values of |Rep t| can typically be obtained automatically
at |replace|'s call site using Haskell's class system.

\citet{Cheney03first-classphantom} continue from here, and define a data type
for the sum of products representation of data types,
and use this representation to define combinators to
express generic traversals over arbitrary data types
for which there is a representation.

\section{Design Rationale}
\label{sect.designdecisions}

In this section, we discuss the design decisions of \SystemFAI.
We are liberal concerning syntax in this section, without loss of generality.
In Section~\ref{sect.typesystem.language}, we treat \SystemFAI{} formally.

\subsection{Church Encoding of Data Types}

In other GADT specifications and algorithms, GADT matches are described in combination
with case-expressions. In many type system descriptions, however, data types and
case expressions are not part of the language, because these are implied by using a
Church encoding or Mogensen-Scott encoding~\citep{DBLP:journals/jfp/Mogensen92}
of the data types. In our specification, we take a similar approach and consider a
Church encoding of GADTs.

\paragraph{Church encoding of ADTs.}
As a prelude, we informally sketch the Church encoding of algebraic data types.

The easiest example to start with are Church booleans. The constructors |True|
and |False| can be represented as functions that take two continuation-expressions
as parameters and return the appropriate one:
\begin{code}
type Bool' = forall alpha . alpha -> alpha -> alpha

mkTrue, mkFalse :: Bool'
mkTrue   t f = t
mkFalse  t f = f
\end{code}
The functions |mkTrue| and |mkFalse| can be used instead of the original
constructors. To pattern match against such a constructor, we give it the
continuations. For example, the following function:
\begin{code}
ifThenElse :: Bool -> a -> a -> a
ifThenElse b f g
  = case b of
      True   -> f
      False  -> g
\end{code}
can be encoded as:
\begin{code}
ifThenElse :: Bool' -> a -> a -> a
ifThenElse b f g = b f g
\end{code}

In general, the Church encoding of a data constructor is a function that takes
(Church encoded) values for each of its fields, and several
continuation functions, one for each constructor.
The values are passed on to the appropriate continuation
function. For example, given the following data type:
\begin{code}
data D
  =  C1 Int
  |  C2 D
\end{code}
We introduce a (recursive) type |D'| for Church-encoded |D|s, and constructor functions |mkC1| and |mkC2|:
\begin{code}
type D' = forall r . (Int -> r) -> (D' -> r) -> r

mkC1 :: Int -> D'
mkC1 x f1 _  = f1 x

mkC2 :: D' -> D'
mlC2 r _ f2  = f2 r
\end{code}
In this example, we assume that built-in types are not encoded. As a technical detail,
we require a number of built-in types in order to map recursive types to
System F~\citep{DBLP:journals/fuin/Urzyczyn96}.

When we pattern match in a case-expression, we get a value of type |D'|,
and parameterize it with functions that deal with each of the cases. For
example, given the following case expression:
\begin{code}
case x of
  C1 y  -> y + 1
  C2 _  -> undefined
\end{code}
In the Church encoding, this corresponds to:
\begin{code}
x (\y . y + 1) (\_ . undefined)
\end{code}

Likewise, we can look at encodings of other forms of pattern matching.
A let-binding can be encoded by means of a lambda and application:
\begin{code}
let (C1 y) = x in y + 1
\end{code}
The pattern match takes place when |y| is evaluated.
We can encode such a let-expression as a lambda, if we assume that patterns in a lambda match
lazily:
\begin{code}
(\y . y + 1) ((\(C1 y) . y) x)
\end{code}
As continuation functions we take |undefined|, except for the continuation
corresponding to the data constructor matched on.
\begin{code}
(\y . y + 1) ((\d . d (\y . y) undefined) x)
\end{code}
If a let-binding involves multiple variables, we use the
Church encoding of tuples.

Haskell has irrefutable (or, lazy) patterns.
A match against such pattern always succeeds, and is actually only
performed when values of variables that are bound by the pattern
are needed. In the following example, the pattern match against |C1|
is only performed when the value of |y| is needed:
\begin{code}
case x of
  ~(C1 y) -> y + 1
\end{code}
We can write the irrefutable pattern with a let-binding.
\begin{code}
case x of
  z ->  let (C1 y) = z
        in y + 1
\end{code}
This expression can be encoded again in a similar way as above.

\paragraph{Church encoding of GADTs.}
The above approach has as advantage that we only need to consider lambda applications
in our specification, and from it, the behavior for case-expressions, let-bindings,
etc. can be derived.

In the previous section, we showed that the mechanism underlying GADTs is the
construction and application of equality proofs.
These proofs are constructed and stored as fields in the constructor, such that
they can be taken out when the match succeeds.
In the Church encoding, a field has become a lambda. We thus introduce two
new forms of expressions. An expression |tau =*= sigma| that builds a proof
of the equality between |tau| and |sigma|, and an expression
|\(tau =*= sigma) . e| that matches against such a proof and allows it to be
used for coercions in |e|.

For example, for a GADT (written using qualified-type notation):
\begin{code}
data Rep a
  = (a =*= Int) => RInt
\end{code}
The encoding for |RInt| takes an equality proof, and passes it on to
the continuation:
\begin{code}
type Rep' a = forall r . ((a =*= Int) -> r) -> r

mkRInt :: (a =*= Int) -> Rep' a
mkRInt = \(a =*= Int) . \f . f (a =*= Int)
\end{code}
In order to construct a value of |Rep' a| using |mkRInt|, we first need
to pass a proof that |a =*= Int|.

\paragraph{Lazy equalities.}
We choose the equality-lambda to bind lazily. The following example gives an explanation.
The pattern occurs in a let-expression and does not define any variables,
which essentially means that it will never be evaluated. 
\begin{code}
f :: Rep a -> a -> Int
f x y  =  let   RInt = x
          in 3
\end{code}
In the encoding, |x| is only evaluated if its equality proof is needed when equalities
bind lazily:
\begin{code}
\(x :: Rep a) . \(y :: a) . (\(a =*= Int) . 3 :: Int) (x (\(a =*= Int) . (a =*= Int)))
\end{code}
However, if we replace the |3| by |y|, the equality proof is needed to coerce the
type |a| to |Int|. This subsequently leads to evaluation of |x|.

It is, however, undesirable that the construction of an equality proof influences the
evaluation of the program. With our encoding, we have a model to reason about these
effects. For example, it is straightforward to verify that the encoding of GADT matches
in a case expression, and the encoding of GADT matches in a lambda, do not influence
the evaluation of the program.

\subsection{Type Inference}
\label{sect.motivation.inference}

Above, we gave type signatures to all expressions involving GADTs.
Several authors showed that there are situations where coercions
can be inferred without an accompanying type annotation.
So far, such approaches are not predictable: it is not intuitive
when an annotation may be omitted or when it is obligatory.
Several examples in this section illustrate the difficulties
regarding inference.
We therefore decided to allow coercions only when
directed to via a type annotation, and describe how this shows
up in the specification.

The main problem regarding GADT inference is that without a
type annotation, it is not clear whether or not to coerce a
type. In the following example, the pattern match on |Num|
brings an equality on |Int| in scope, which may be applied
to coerce the type of |3|:
\begin{code}
data Expr t where
  Num    :: Int -> Expr Int
  Tuple  :: Expr a -> Expr b -> Expr (a,b)

eval (Num x) = x
\end{code}
There are several types possible for |eval|:
\begin{code}
(1)  eval :: forall t dot Expr t -> t
(2)  eval :: Expr Int -> Int
(3)  eval :: forall t dot Expr t -> Int
\end{code}
The second type seems appropriate in this case.
However, the first type is more general than the second, and
the first and third are incomparable.
We cannot choose between the first and third type,
unless we know precisely how |eval| is to be used.
Many inference
approaches analyze the usages of such a function to make a choice.
When usage of such a function changes due to modifications of the programmer,
this may affect the choice, and cause type errors in other parts of the
program. This leads to an unpredictable type inference.
We choose only to apply equalities when directed to via a type annotation. In
the above case, no type annotation is present, we do not apply the equality,
which results in type (3).

In the above example, the usage of |x| in the body seems
to suggest a relation to type |t| in |Expr t|. However, the following
example demonstrates that this is not a good criterium, because there are
also expressions that have a coercible type, aside from variables occurring
in the pattern:
\begin{code}
flex True (Num x)   = x
flex False (Num x)  = 3
\end{code}
Multiple pattern matches pose additional challenges. In the following example,
there are two possible equalities on |Int| to choose from:
\begin{code}
choose (Num x) (Num y) = 3
\end{code}
There are now many alternative types possible, including:
\begin{code}
choose  :: forall t s dot Expr t -> Expr s -> t
choose  :: forall t s dot Expr t -> Expr s -> s
choose  :: forall t s dot Expr t -> Expr s -> Int
\end{code}
During inference of the body of |choose|, the problem boils
down to making a choice between either coercion to a
Skolem constant such as |s| or |t|, or not coerce types at
all.
Again, we refrain from applying an equality unless directed
to by a type annotation, and thus end up with the last
type.

When there are multiple function or case alternatives, there is often
no choice. The equalities have to be applied to have branches with
equal types.
\begin{code}
eval (Num x)    = x
eval (Tup a b)  = (a,b)
\end{code}
We still require a type annotation. The design rationale is here that
adding additional cases to a function without changing the existing
cases, should only make a type less specific. In the above case, adding
the |Tup| alternative causes the type of |eval| to change to
an incomparable type, which again makes type inference hard to predict
from the perspective of the programmer.
Also, we point out that in the situation that multiple function or
case alternatives are written, the overhead of the annotation (expressed
for example in terms of lines of code) decreases.

In our specification, we abstract from the type inference algorithm.
Moreover, we require type inference to be completed before the inference
of coercions.
The language \SystemFAI{}, based on System F, is explicitly typed.
These explicit types represent the types derived from type annotations
and those inferred.
This makes it unambiguous where to find the locations where
a coercion is needed: at those locations where the actual type does not
match the expected type (Section~\ref{sect.algorithm}).
What remains is to specify how coercions are
inferred, and that we make explicit in the specification.