\section{introduction}
\label{sect.introduction}


Generalized Algebraic Data Types (\GADTs for short) allow for additional equalities to hold between type variables, witnessed by pattern matching on \GADT constructors. These equalities are then used to coerce the type of an expression to an equivalent type. We give a more extensive introduction to \GADTs in \Sect{sect.motivation}.

There are many applications that show that \GADTs are a useful addition to languages. For example when dealing with transformations on typed abstract syntax for the implementation of domain-specific languages~\cite{leftcorner}. Therefore, we added support for \GADTs in EHC, the Haskell compiler that we are developing at Utrecht University. We describe our implementation in terms of some specification. However, we were unable to find a specification that is sufficiently simple to match our implementation, because of two reasons. We sketch these reasons here, and defer a more thorough discussion to \Sect{sect.relatedwork}.

The first reason is that the type systems given by most approaches are complex. A reason for this is that algorithmic type systems are given, which rely on advanced type system infrastructures for the implementation. This makes it harder to incorporate ideas when the infrastructures differ.

Secondly, the GADT-aspect of an approach is often not discussed in isolation, but alongside with other language features. This makes it difficult to determine if one requirement of an approach relates to the GADT-aspect, or is a requirement related to another language feature.

Therefore, we conclude that a specification is needed that is less complex and only takes the key issues of GADTs into account. The techniques we use are not novel: we take the constraint-based approach of Sulzmann et al.~\cite{sulzmann06} and combine this with the unification-based approach of Peyton Jones et al.~\cite{jones06}. However, the resulting type system is easier and less tied to a particular implementation.

More concretely, we give:
\begin{itemize}
\item A declarative type system (\Sect{sect.typesystem}) for an explicitly typed \SystemF-like language extended with GADTs, using qualified types with equalities as qualifiers. Type conversions are restricted without having to resort to rigid types~\cite{jones06} or type shapes~\cite{pottier06}.
\item A denotational semantics (\Sect{sect.translation}) by giving a translation to a subset of \SystemFC, which is a \SystemF-like language with explicit type coercions, defined by Sulzmann et al.~\cite{sulzmann07}. 
\end{itemize}

%if False


. Several approaches to add \GADTs are known, but they are complicated and the type systems given are unconventional. This can be done in an easier way by reusing available mechanisms, most notably those for qualified types, and keep the implementation complexity of the embedding into the programming language minimal.

Our overall goal, independent of the topic of this paper, is to discover which minimal mechanisms we need in order to target as many language features as possible, while keeping the implementation simple, isolated, and understandable. Leading work (\Sect{sect.relatedwork}) in this area gives advanced solutions, but fails in this regard. Many concepts are introduced, which makes it difficult to distinguish what is essential or just a detail specific to a certain implementation.

For example, the approach of Peyton Jones et al.~\cite{jones06} uses a distinction between wobbly and rigid types, ``fresh most general unifiers'', lexically scoped type variables, and type refinement. It is hard to distinguish which of these concepts are essential to a \GADT implementation, and which are not. The authors claim that this approach is simple, and although it is certainly simpler than their earlier work~\cite{jones04}, it is still far removed from a specification that is easy to understand and widely applicable.

Another example is the constraint-based approach of Sulzmann et al.~\cite{sulzmann06}. Again, the typing rules are unconventional in the sense that the rules mention most-general unifiers and syntactic equalities. Furthermore, the typing/translation rules do not mention how to deal with existential data types, which may be transparent to the given approach, but is of interest to a reader because most interesting \GADT examples make use of them. Finally, in contrast to Peyton Jones et al., restrictions on type conversions are not mentioned.

We conclude that there is a need for a minimalistic specification of GADTs and their implementation. We give a specification that consists of:
\begin{itemize}
\item A declarative type system (\Sect{sect.typesystem}) for an explicitly typed \SystemF-like language extended with GADTs, using qualified types with equalities as qualifiers. Only conventional concepts are used for the description of the type system. Type conversions are restricted without having to resort to rigid types~\cite{jones06} or type shapes~\cite{pottier06}.
\item A denotational semantics (\Sect{sect.translation}) by giving a translation to a subset of \SystemFC, which is a \SystemF-like language with explicit type coercions~\cite{sulzmann07}. 
\end{itemize}
Furthermore, we show how to implement the specification as a relatively isolated aspect, independent of a type inference strategy. The implementation of the type system proceeds along similar lines as an implementation for qualified types: (scoped) assumptions are introduced at pattern matches, and proof obligations at the places where type coercions are required by using an instrumented unification algorithm that also returns proof obligations and, by interaction with entailment, coercion terms. Entailment is implemented such that the proving machinery constructs type coercions. In the specification, the entailment rules are tied to the type language, but for the implementation this dependency is factored out by again using the instrumented unification algorithm.

%endif