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

We define the semantics of \SystemFAI{} in terms of \SystemFC{}~\citet{sulzmann07}.
We introduction to \SystemFC, then show the important parts of the translation.

\subsection{\SystemFC}
\SystemFC{} extends \SystemF{} with equality coercions. It has a built-in
syntax to represent values of the |Equal| data type mentioned in
the Section~\ref{sect.typed.abstract}.

\begin{figure}[htb]
\rule{\linewidth}{0.1pt}
\begin{code}
coe  `elem` Coercion                       ^^^^             ^^^^^   e'  `elem`  Expr
       ::=  x                              ^^^^  CVAR       ^^^^^       |||     e :> coe                                                                    ^^^^ EAPPCOE
       |||  coe1 coe2                      ^^^^  CAPP       ^^^^^       |||     case e' of (overline (p -> e'))                                             ^^^^ ECASE
       |||  ty                             ^^^^  CREFL      ^^^^^
       |||  sym coe                        ^^^^  CSYM       ^^^^^   p   `elem`  Pat
       |||  coe1 compose coe2              ^^^^  CTRANS     ^^^^^       |||     C (overline (coe : tau ~ sigma)) (overline (alpha : star)) (overline (x : rho))     ^^^^ PCON
       |||  right coe                      ^^^^  CRIGHT
       |||  left   coe                     ^^^^  CLEFT      ^^^^^   d   `elem`  Decl
       |||  forall alpha dot coe           ^^^^  CUNIV      ^^^^^       |||     data D (overline a) ^^^ (overline (| C (overline (tau ~ sigma)) (overline (alpha : star)) (overline rho)))
       |||  coe @ rho                      ^^^^  CINST
\end{code}
\rule{\linewidth}{0.1pt}
\caption{Subset of syntax of \SystemFC{}}
\label{fig.systemfc}
\end{figure}

We limit our explanation to a simplified fragment of \SystemFC{}, which contains
what we need: System F (lambda abstraction, etc.), data types, case expressions, and coercions.
\Fig{fig.systemfc} lists the extensions to System F.
A data constructor |C| consists of three components: equality coercions, existentials, and fields, respectively, hence
it is a representation of the qualified-type style of GADT constructors.

A coercion |coe| can be applied to an
(\SystemFC) expression |e'|, denoted as |e' :> coe|, which changes the
type of |e'| according to coercion.
A coercion |coe| of type |ty1 ~ ty2| represents a proof of the equality
of |ty1| and |ty2|. \Fig{fig.coercionrules} lists the typing rules of
coercion terms. See Sulzmann et al.~\cite{sulzmann07} for the full listing.

  \begin{figure}[htb]
  \rule{\linewidth}{0.1pt}
  \begin{mathpar}
  \fbox{|env :- coe : ty1 ~ ty2|}\\

  \inferrule*[right=var]
    {|x :: ty1 ~ ty2 `elem` env|}
    {|env :- x : ty1 ~ ty2|}
  
  \inferrule*[right=app]
    { |env :- coe1 : ty1 ~ ty3| \\
      |env :- coe2 : ty2 ~ ty4|
    }
    {|env :- coe1 coe2 : ty1 ty2 ~ ty3 ty4|}
  
  \inferrule*[right=refl]
    {}
    {|env :- ty : ty ~ ty|}
  
  \inferrule*[right=sym]
    {|env :- coe : ty2 ~ ty1|}
    {|env :- sym coe : ty1 ~ ty2|}
  
  \inferrule*[right=trans]
    { |env :- coe1 : ty1 ~ ty2| \\
      |env :- coe2 : ty2 ~ ty3|
    }
    {|env :- coe1 compose coe2 : ty1 ~ ty3|}
  
  \inferrule*[right=left]
    {|env :- coe : ty1 ty2 ~ ty3 ty4|}
    {|env :- left coe : ty1 ~ ty3|}
  
  \inferrule*[right=right]
    {|env :- coe : ty1 ty2 ~ ty3 ty4|}
    {|env :- right coe : ty2 ~ ty4|}
  
  \inferrule*[right=forall]
    {|env :- coe : ty1 ~ ty2| \\
     |alpha notelem ftv env|}
    {|env :- forall alpha dot coe : forall alpha dot ty1 ~ forall alpha dot ty2|}
  
  \inferrule*[right=inst]
    {|env :- coe : forall alpha dot ty1 ~ forall beta dot ty2|}
    {|env :- coe @ rho : ty1 [alpha := rho] ~ ty2 [beta := rho]|}
  \end{mathpar}
  \rule{\linewidth}{0.1pt}
  \caption{Coercion type rules}
  \label{fig.coercionrules}
  \end{figure}

  Coercion application |coe1 coe2| builds a coercion that applies |coe1| to the function part |f|
  and |coe2| to the argument part |a| of a type application |f a|.
  With transitivity |coe2 compose coe1|,
  the second coercion is applied to the result of applying the first coercion.
  The |right|-coercion extracts the coercion of the arguments from a coercion on a type application |f a|.

\subsection{Translation Overview}

  We use a type-directed translation. The typing relations have the form:
  \begin{code}
  env :- e : ty ~> e'          -- \SystemFC-expr |e'| is the translation of \SystemFAI-expr |e|.
  env ::- ty1 =*= ty2 ~> coe   -- |coe| is a \SystemFC-coercion term of type |ty1 ~ ty2|.
  \end{code}
  
  The translation consists of two challenges: we need to represent \SystemFAI's equality
  proofs in \SystemFC, and need to associate with each equality-proof rule of the previous
  section a well-typed \SystemFC-coercion term.
  
  \subsection{\SystemFAI{} expressions}

  \begin{CenterFigure}{h}{\SystemFAI-expr translation rules}{fig.trans.expr}
  \rule{\linewidth}{0.1pt}
  \begin{mathpar}
    \fbox{|env :- e : ty ~> e'|}\\

    \inferrule*[right=var]
      { |x :: tau `elem` env| \\
      }
      { |env :- x : tau ~> x| }

    \inferrule*[right=coerce]
      { |env :- e : sigma ~> e'|\\\\
        |env ::- sigma =*= tau ~> coe|\\\\
        |ftv tau `subset` ftv env|
      }
      { |env :- e : tau ~> e' :> coe| }

    \inferrule*[right=eq]
      { |env ::- tau =*= sigma ~> coe| \\\\
        |ftv tau `subset` ftv env| \\\\
        |ftv sigma `subset` ftv env|
      }
      { |env :- tau =*= sigma : tau =*= sigma ~> (semb (tau =*= sigma)) coe| }

    \inferrule*[right=app.expr]
      { |env :- f : sigma -> tau ~> f'| \\\\
        |env :- e : sigma ~> e'|
      }
      { |env :- f e : tau ~> f' e'| }

    \inferrule*[right=app.ty]
      { |env :- f : sigma -> tau ~> f'| \\\\
        |ftv sigma `subset` ftv env|
      }
      { |env :- f sigma : tau ~> f' (semb sigma)| }

    \inferrule*[right=lam.expr]
      { |env, x :: sigma :- e : ty ~> e'|
      }
      { |env :- \(x :: sigma) . e : sigma -> ty ~> \(x :: (semb sigma)) . e'| }

    \inferrule*[right=lam.ty]
      { |env, alpha :- e : ty ~> e'| \\\\
        |alpha notelem ftv env |
      }
      { |env :- BigLam alpha . e : forall alpha . ty ~> BigLam alpha . e'| }

    \inferrule*[right=lam.eq]
      { |env, x :: rho =*= sigma :- e : tau ~> e'|\\
        |x,y notelem env|
      }
      { |env :- \(rho =*= sigma) . e : (rho =*= sigma) -> tau ~> \y . case y of (semb (rho =*= sigma)) (x : (semb rho) =*= (semb sigma)) -> e'| }
  \end{mathpar}
  \rule{\linewidth}{0.1pt}
  \end{CenterFigure}
  \begin{CenterFigure}{h}{Equality proof translation rules}{fig.trans.equal}
  \rule{\linewidth}{0.1pt}
  \begin{mathpar}
    \fbox{|env ::- ty1 =*= ty2 ~> coe|} \\
  
    \inferrule*[right=refl]
      {}
      {|env ::- ty =*= ty ~> (semb ty)| }

    \inferrule*[right=sym]
      { |env ::- tyr =*= tyl ~> coe| }
      { |env ::- tyl =*= tyr ~> sym coe| }

    \inferrule*[right=trans]
      { |env ::- ty1 =*= ty2 ~> coe1| \\\\
        |env ::- ty2 =*= ty3 ~> coe2|
      }
      { |env ::- ty1 =*= ty3 ~> coe2 compose coe1| }

    \inferrule*[right=assum]
      { |x : ty1 =*= ty2 `elem` env|
      }
      { |env ::- ty1 =*= ty ~> x|}
    
    \inferrule*[right=con.arr]
      { |env ::- sigma =*= tau ~> coe1| \\\\
        |env ::- rho =*= varrho ~> coe2|
      }
      { |env ::- tau -> rho =*= sigma -> varrho ~> coe1 -> coe2| }

    \inferrule*[right=sub.arr]
      { |coe1 :: (tau3 =*= (tau4 -> tau5)) `elem` env| \\
        |coe2 :: (tau6 =*= (tau7 -> tau8)) `elem` env| \\\\
        |env ::- tau3 =*= (tau6 ~> coe3)| \\\\
        |coe5 = right (sym coe1 compose coe3 compose coe2)|\\
        |coe6 = right (right (sym coe1 compose coe3 compose coe2))|\\\\
        |coe5 :: tau4 =*= tau7, coe6 :: tau5 =*= tau8 ::- tau1 =*= tau2 ~> coe4| \\\\
        |coe1,coe2 notelem env|
      }
      { |env ::- tau1 =*= tau2 ~> coe4| }
  \end{mathpar}
  \rule{\linewidth}{0.1pt}
  \end{CenterFigure}
  
  The first-class equality proofs in \SystemFAI{} have no direct counterpart in
  \SystemFC. However, in \SystemFC, equality proofs may be stored in a data constructor.
  For example, for an equality proof of type |alpha =*= beta -> Int|, we can associate a
  data type:
  \begin{code}
  data D alpha beta = C (alpha =*= beta -> Int)
  \end{code}
  In general, we associate a data type $|D|_{|key(tau,sigma)|} |(overline alpha)|$
  with a \SystemFAI{} proof of type |tau =*= sigma| (|(overline alpha) = ftv tau +++ ftv sigma|),
  as well as a constructor $|C|_{|key(tau,sigma)|}$ storing the \SystemFC-coercion.
  We denote with |(semb (tau =*= sigma))| the conversion from a \SystemFAI-proof type to
  a \SystemFC{} data type, or data constructor according to the above procedure.
  Similarly, |(semb sigma)| denotes the translation of a \SystemFAI{} type to a
  \SystemFC{} type, by recursively mapping each coercion type |tau =*= sigma| to
  $|D|_{|key(tau,sigma)|} |(overline alpha)|$.

  Figure~\ref{fig.trans.expr} shows the translation rules, which are the type rules of the previous
  section extended with the resulting |e'| expression.

\subsection{Translation of Proofs}

  Figure~\ref{fig.trans.equal} shows how to produce coercion terms from the
  equality proof. We omitted the rules for universal quantification: these
  are analogous.
  The rules \TirName{refl}, \TirName{sym}, \TirName{trans}, and \TirName{assum}
  have a direct mapping to a coercion-term.

  Each individual rule is a solution to a small puzzle.
  For a proof of |tau =*= sigma|, we combine coercions |coe| until they
  have exactly the same type according to coercion type rules in
  Figure~\ref{fig.coercionrules}.
  For example, we can verify that rule \TirName{sub.arr} constructs a coercion
  with the right type as follows:
  \begin{code}
  coe1                                                :: tau3 =*= (tau4 -> tau5)
  coe2                                                :: tau6 =*= (tau7 -> tau8)
  coe3                                                :: tau3 =*= tau6
  sym coe1 compose coe3 compose coe2                  :: (tau4 -> tau5) =*= (tau7 -> tau8)
  right (sym coe1 compose coe3 compose coe2)          :: tau4 =*= tau7
  right (right (sym coe1 compose coe3 compose coe2))  :: tau5 =*= tau8
  \end{code}

\subsection{Correctness}

  It is easy to show that a well-typed equality-proof is translated to a well-typed
  coercion term (see above). It is also easy to show that a \SystemFAI{} expression
  is translated to a well-typed \SystemFC{} expression.
  Because \SystemFC{} has type soundness, we thus obtain that \SystemFAI{} also
  has type soundness.