\section{Translation}
\label{sect.translation}


We give a translation to \SystemFC in order to give a semantics to the GADTs in our source language.

\paragraph{Target Language}
We limit our explanation to the fragment of \SystemFC that we need. This fragment is given in \Fig{fig.systemfc}. See Sulzmann et al.~\cite{sulzmann07} for a full explanation. There are some essential differences with respect to the source language:
\begin{itemize}
\item A proof of equality is made explicit as a \emph{coercion} value |coe| with the type |ty1 ~ ty2|, meaning that |coe| is a witness that the type |ty1| is equal to type |ty2|. Constructors store coercions as additional fields, and require them to be passed (|TXTEAPPCOE|) when constructing values with such a constructor. Pattern matching against such a constructor bind an identifier to the coercion, allowing referencing to this coercion (|TXTCVAR|).
\item The \emph{cast} operator |:>| takes an expression |e'| of type |ty1|, and a coercion of type |ty1 ~ ty2|, and converts the type of |e'| to |ty2|.
\item There are several language constructs to operate on coercions. Transitivity (|coe1 compose coe2|) and symmetry (|sym|) have the usual interpretation. The |left| construct decomposes a coercion on type applications to a coercion of only the function part. Similarly, the |right| construct decomposes a coercion to the argument part. Coercion application |coe1 coe2| creates a coercion that applies |coe1| to the function part of a type application and |coe2| to the argument part. Reflexivity of type |ty ~ ty| is encoded as the coercion (not type!) |ty|. The other two constructs deal with quantors in types.
\end{itemize}
See Sulzmann et al.~\cite{sulzmann07} for a type system of the target language.

\begin{PlainFigure}{t}{Syntax of the target language}{fig.systemfc}
\begin{code}
e'    ::=  e                                               ^^^^                             ^^^^^  coe  `elem` Coercion
      |||  e' ^^^ :> ^^^ coe                               ^^^^  ECAST                      ^^^^^       ::=  x                              ^^^^  CVAR
      |||  e' coe                                          ^^^^  EAPPCOE                    ^^^^^       |||  coe coe                        ^^^^  CAPP
                                                                                            ^^^^^       |||  ty''                           ^^^^  CREFL
d'    ::=  data D manyalpha = overline(| exists^manybeta dot C manycoe manyty'')            ^^^^^       |||  sym coe                        ^^^^  CSYM
                                                                                            ^^^^^       |||  coe compose coe                ^^^^  CTRANS
ty''  ::=  ty slash { =*= => }                                                              ^^^^^       |||  left coe                       ^^^^  CLEFT
      |||  coe -> ty''                                                                      ^^^^^       |||  right coe                      ^^^^  CRIGHT
                                                                                            ^^^^^       |||  forall^alpha dot coe           ^^^^  CUNIV
p'    ::=  p                                                                                ^^^^^       |||  coe @ ty''                     ^^^^  CINST
      |||  p' coe                                          ^^^^  PAPPCOE                    ^^^^^
                                                                                            ^^^^^  env  |||  x :-> ty =*= ty, env
\end{code}
\end{PlainFigure}

\paragraph{Coercion construction} In environment |env|, the source expression |e| with type |ty| is translated to the same expression |e'| in the target language, with two exceptions (\Fig{rules.T.expr.trans}). The key idea here is that a derivation of entailment is an equality proof out of which a coercion is constructed. The entailment relation expresses here that in environment |env|, |tyl| is equal to |tyr|, witnessed by the coercion |coe| (of type |tyl ~ tyr|).

\rulerCmdUse{rules.T.expr.trans}

Rule |TXTEAPPEQS| states that if an proof of equality is expected for the source language, that this proof as coercion |coe| is passed explicitly as parameter in the target language.

With Rule |TXTECOERCE|, a type constants |v| deep inside |ty'| are converted. The small coercions |overline(coe)| for these type constants need to be combined into one coercion that operates on the entire |ty'|, by adding the appropriate amount of coercion applications, universal abstractions and instantiations, and reflexive-coercions. For reasons of space, we hide this triviality behind the function |lift|.

\rulerCmdUse{rules.T.entails.base}

The actual construction of the coercion is a side effect of using the entailment rules of \Fig{rules.T.entails.base} to proof an equality.
\begin{itemize}
\item The translation for pattern matches translates each assumption |tyl =*= tyr| of a constructor to an explicit match on a coercion of type |tyl ~ tyr|, binding this coercion to some unique identifier |x| and adding this binding to the environment. Then, entailment rule |TXTEASSUME| lookups this binding in the environment and refers to it as the coercion |x|.
\item The coercion for the congruence rule may only replace some type constants somewhere deep inside the type structure. Again, |lift| is used for the construction of the full coercion.
\item The subsumption rule decomposes a coercion in small coercions, by adding the appropriate amount of |left| and |right| coercions in front of them. We omit rules for this decomposition and hide this triviality behind the |decompose| function.
\end{itemize}


%if False

First we give the syntax of a fragment of \SystemFC in \Fig{fig.systemfc} and a type system for it in \Fig{rules.T.expr'.base} and \Fig{rules.T.coercion.base} (a subset of the rules of Sulzmann et al.~\cite{sulzmann07}). Then we give a translation of \SystemFAPrime to this fragment of \SystemFC in \Fig{rules.T.expr.trans}. This translation boils down to using the derivation of entailment to construct coercion terms, which is given in \Fig{rules.T.entails.base}. These entailment rules use some utility rules listed in \Fig{rules.T.spine.base}.

\Fig{fig.systemfc} gives the relevant parts of the syntax of the target language (a fragment of \SystemFC). Compared to the \SystemFAPrime, the target language explicitly states where types are converted with a cast expression using a coercion expression, and how these coercions are structured. A cast |:>| takes a coercion |coe| to convert the type of an expression.

\Fig{rules.T.expr'.base} lists a type system for the new constructs of \SystemFC. \Fig{rules.T.coercion.base} lists how to type coercions, where |coe : tya ~ tyb| means that coercion |coe| can convert a type |tya| to |tyb|.

\rulerCmdUse{rules.T.expr'.base}
\rulerCmdUse{rules.T.coercion.base}

Each expression is translated to the same expression in the target language, with two exceptions (\Fig{rules.T.expr.trans}). The key idea here is that a derivation of entailment is an equality proof out of which a coercion is constructed. In the target language coercions are passed explicitly and end up as coercion `values' in constructors (\Fig{fig.systemfc}). Furthermore, a cast expression |:>| is inserted at those places where type conversions are performed. From the entailment we get coercions |coei| for sub components of the type |ty|. These individual coercions are merged in one encapsulating coercion for the type by adding additional coercions to walk over the spine of |ty|, using judgement |(sub(:-)(s))| (\Fig{rules.T.spine.base}) (we cover this judgement in more detail later).

\rulerCmdUse{rules.T.expr.trans}

The translation for data types add a coercion component to a data constructor for each quality constraint in the data type definition. The translation for pattern matches bind a name to these coercion `values' of a constructor, such that these coercions can be referenced later (|TXTEASSUME| in \Fig{rules.T.entails.base}).

\rulerCmdUse{rules.T.entails.base}

So, the entire translation boils down to coercion generation by means of entailment. Most of the entailment rules have a direct counter part in the coercion language (i.e. symmetry and transitivity). Indeed, the translation for entailment in \Fig{rules.T.entails.base} maps each step of the equality proof to a coercion. However, the congruence and subsumption rule have no direct counter parts. Congruence takes several small coercions for sub components of a type and constructs a coercion for the entire type. Subsumption does the inverse, it decomposes a big coercion in smaller coercions. In both cases, a common spine of two types need to be traversed and the appropriate coercion terms generated, such as |left| and |right| for subsumption or coercion applications for congruence.

\rulerCmdUse{rules.T.spine.base}

The judgement |(sub(:-)(s))| in \Fig{rules.T.spine.base} takes care of both ways of constructing coercions. The result |coe| is produced by combining inputs |(overline(coeii))|. Each result |coei| in |(overline coe)| is produced by decomposing the input coercion |coeii|. A coercion for an application is glued together from a coercion for the function part and a coercion for the argument part using coercion application, and decomposed to the function part by taking the |left| and the argument part by taking the |right|. For example, 
|(sub(:-)(s)) f Int ~~ g Int| with inputs |coefgintint| and the singleton list |coefg|, results in |coefg Int| and |left coefgintint, right coefgintint|.

%endif