\newcommand{\Fig}[1]{Figure~\ref{#1}}
\newcommand{\Sect}[1]{Section~\ref{#1}}
\newcommand{\SystemF}{System $F\,$}
\newcommand{\SystemFA}{System $F_A\,$}
\newcommand{\SystemFAPrime}{System $F_A'\,$}
%%\newcommand{\SystemFAI}{System $F_A^i$}
\newcommand{\SystemFAI}{System $F_{|~|}$}
\newcommand{\SystemFC}{System $F_C$}
\newcommand{\GADT}{GADT }
\newcommand{\GADTs}{GADTs}
\newcommand{\metacomment}[1] {}


%include format.lhs


Generalized Algebraic Data Types are a generalization of Algebraic Data Types
with additional type equality constraints. These found their use in many functional
programs, including the development of embedded domain specific programming languages and
generic programming.

Recently, several authors published novel inference algorithms and
corresponding type system specifications.
These approaches tend to be more algorithmic than declarative in
nature, and tied to a given compiler infrastructure. This results in
complex specifications.
For a language implementor,
adopting such a complex approach is hard due to conflicting infrastructure and
language features. Similarly, type inference is difficult to comprehend
for a programmer when the specification is complex.

To make the integration of GADTs in languages easier, we thus need a more orthogonal
specification. We present an orthogonal specification for GADTs:
the language \SystemFAI, consisting of
System F augmented with first-class equality proofs.
This specification exploits the Church encoding of
data types to describe GADT matches in terms of conventional
lambda abstractions.


%include introduction.lhs
%include motivation.lhs
%include typesystem.lhs
%include translation.lhs
%% %include algorithm.lhs
%include related-work.lhs
%include conclusion.lhs