\section{Implementation}
\label{sect.implementation}

We showed in previous sections a specification for GADTs. This specification is declarative and not syntax directed. We show in this section how to overcome this problem. Our solution relies on a system for qualified types.

The first issue is how to deal with is type inference. Clearly, given the example in \Fig{fig.example}, the source language requires an abundant amount of type annotations. However, algorithms that propagate type information only reduce the number of type annotations that are required and do not increase expressiveness. It is therefore an orthogonal issue, already covered by many other authors~\cite{pottier06, vytiniotis06, jones04}.

Secondly, the rules |TXTEAPPC| and |TXTECOERCE| are not syntax directed. This issue is resolved by merging the |TXTEAPPC| rule with the |TXTECON| rule, and the |TXTECOERCE| with the |TXTECASE| rule for each case alternative.

Thirdly, the  entailment rules are not syntax directed. We overcome this problem by using Constraint Handling Rules (CHRs)~\cite{chr98}. Stuckey et al. showed that they are useful for implementing a system of qualified types~\cite{stuckey02, rossberg02}. The entailment rules in \Fig{rules.T.entails.base} are basically CHR rules with some syntactic sugar, with the exception that the subsumption rule may only be applied to assumptions taken from the environment. Lookups in the environment and the judgement |(sub(:-)(s))| are guards of the rules they occur in. The generated coercion is a side effect of applying the CHR rules. The judgement |(sub(:-)(s))| is implemented by modifying the unification function to yield the coercions as side effect. 

We use a framework for the implementation of CHRs~\cite{atze07, geest07} with several attractive properties. The rules can be expressed with so called propagation CHRs only Solving a set of constraints then amounts to applying the rules exhaustively. The solver administers each successful application of a rule as an edge annotated with the coercion in a graph with equality constraints as nodes. A path in this graph from constraint to assumption represents a solution and we obtain the full coercion by composing the coercions on this path.

%if False

\metacomment {
\item CHR regels voor \GADTs.
\item Correspondentie met de entailment relatie in de type regels.
\item Structuur van de regels: guard, reduction (evidence); uitleg van de guards die nodig zijn. Details ook laten zien? Zoals het uitpakken van een rijtje van constraints.
}

\begin{PlainFigure}{t}{Syntax of predicates and constraints}{fig.chrsyn}
\begin{code}
Cn  `elem` Constr                                                                   ^^^^                ^^^^  ^^^^  P     `elem` Pred
    ::=  Ass  P (brack sc)                                                          ^^^^  CASSUME       ^^^^  ^^^^        ::=  ty =*= ty
    |||  Prv  P (brack sc)                                                          ^^^^  CPROVE        ^^^^  ^^^^        |||  (overline(P))
    |||  Red  (overline(P (brack sc))) (sub (~>) (coe')) (overline(P (brack sc)))   ^^^^  CREDUCTION
    ^^^                                                                                                 ^^^^  ^^^^  C     `elem` CHR
GR  `elem` Guard                                                                                        ^^^^  ^^^^        ::=  (overline(Cn)) ^^^ => ^^^ (overline(GR)) ^^^ |> ^^^ (overline(Cn))
    ::=  (overline(sc)) `visible` sc                                                ^^^^  GSCOPING      ^^^^  ^^^^  
    |||  (Substitution, (overline(P)), (overline(coe)), coe) = Uni ty ty            ^^^^  GUNIFICATION  ^^^^  ^^^^  sc    `elem` Scope
\end{code}
\end{PlainFigure}

\Fig{fig.chrsyn} lists the syntax of predicates and constraints. Assumption constraints arise due to pattern matches and
prove constraints when type conversions are required. Reduction constraints represent the steps in an entailment proof and
form an interface to the outside world. The reductions contain a coercion expression |coe'|, which can be turned in a
real coercion |coe| by applying the arguments of the reduction to it. The constraints mention the scope they appear in:
this allows us to solve the constraints together at generalization points.

\rulerCmdUse{rules.C.chr.base}

\Fig{rules.C.chr.base} lists the actual rules. A notation that maps straightforwardly to CHRs is used for didactic reasons: constraints above the
horizontal line are the head of a CHR, constraints below the horizontal line are the body, and the other judgements are
the guards. A rule should be read as follows: the constraints of the part below the horizontal line are added
to the set of constraints when the constraints above the horizontal line match and the guards are satisfied. We omitted
the rules that deal with unpacking constraints with lists of qualifiers to constraints with a single qualifier.

The congruence rules split constraints in smaller constraints for each (incompatible) pair of type components where
one of the two is a skolem type variable in the constraint. There are two variations: the rule for assumptions decomposes
the coercion in smaller coercions, the rule for prove obligations creates a bigger coercion out of many smaller coercions.
The actual functionality is provided by using a modified unification function (\Sect{sect.unification}).

\metacomment {
\item Algoritme om deze CHRs op te lossen (CHR-pipeline, gerrit en atze hun werk).
\item CHRs + constraints $\rightarrow$ reductions $\rightarrow$ graph $\rightarrow$ evidence
\item CHR+constraints naar reductions.
\item Reductions naar reduction graph.
\item Reduction graph naar \GADT evidence.
}

The CHR rules are applied iteratively. The resulting reductions are turned into a graph where the reductions are hyper-edges and the
prove and assume constraints are nodes. A prove constraint is solvable when there is a hyper-path from each prove constraint to assumptions.
The required coercion is constructed by composing the coercions on such a path.

%endif