Fetching contributors…
Cannot retrieve contributors at this time
160 lines (137 sloc) 6.37 KB
\section{Reversing Elaboration}
As well as translating from \Idris{} to \TT{}, so that programs can be type
checked and evaluated, it is valuable to define the reverse transformation. This
serves two principal purposes:
\item To assist the user, it is preferable that the results of evaluation, and any
error messages produced by the elaborator, are presented in \Idris{} syntax
rather than \TT{}.
\item For correctness, we would like to ensure as far as possible that the
result of elaboration is equivalent to the original program. Informally, we can
achieve this by checking that reversing the elaboration process yields the original
program (with implicit arguments expanded).
In this section, we describe the process for reversing elaboration and the required
properties of the elaboration process as a whole. Fortunately, translating from
\TT{} to \Idris{} is significantly easier than \Idris{} to \TT{}, because it is
primarily \emph{erasing} information.
\subsection{From \TT{} to \Idris{}}
We define a meta-operation $\uninterp{\vt}$, which converts a \TT{} expression
$\vt$ to an \Idris{} expression which would elaborate to $\vt$:
\uninterp{\vx} &\mq\:\vx\\
\uninterp{\vc} &\mq\:\vc\\
\uninterp{\vx\;\ta} &\mq\:\vx\;(\vec{\MO{Impl}}\:\vx\:\ta) \\
\uninterp{\vf\:\va} &\mq\:\uninterp{\vf}\:\uninterp{\va}\\
\uninterp{\lam{\vx}{\vT}\SC\ve} &\mq \:\ilam{\vx}\uninterp{\ve} \\
\uninterp{\all{\vx}{\vT}\SC\ve} &\mq \:\piexp{\vx}{\uninterp{\vT}}\uninterp{\ve} \\
\uninterp{\LET\:\vx\defq\vt\Hab\vT\SC\ve} &\mq
\mbox{(if the $i$th argument to $\vx$ is implicit argument $\vn$)}\\
& \carg{\ttinterp{\va_i}} &
\mbox{(if the $i$th argument to $\vx$ is a constraint argument)}\\
& \ttinterp{\va_i} & \mbox{(otherwise)}
This is mostly a straightforward
traversal of the \TT{} expression, translating directly to an \Idris{} equivalent.
The interesting case is for applications of named functions,
$\uninterp{\vx\:\ta}$, where the arguments are translated to either implicit,
constraint or explicit arguments according to the definition of $\vx$.
Since only type declarations are allowed to have implicit or constraint arguments,
and $\uninterp{\cdot}$ translates \emph{expressions},
all function types are assumed to take explicit arguments.
We also define an operation $\MO{Unelab}$, which translates \TT{} declarations
to corresponding \Idris{} declarations. This generates data declarations and
pattern matching definitions only --- it makes no attempt to reconstruct
or \texttt{instance} declarations, or rebuild \texttt{case} expressions.
First, we define the reverse elaboration of type declarations, which must reconstruct
which arguments are implicit or constraint arguments:
\mq & \piimp{\vx}{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\
& \hg\mbox{(if the $i$th argument to $\vx$ is an implicit argument)} \\
& \piconst{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\
& \hg\mbox{(if the $i$th argument to $\vx$ is a constraint argument)} \\
& \piexp{\vx}{\uninterp{\vT}}(\MO{UnelabTyDecl}\:(\vi+1)\:\ve) \\
& \hg\mbox{(otherwise)} \\
Using this, we define $\MO{Unelab}$ for top level declarations. For pattern
matching clauses reversing elaboration proceeds as follows, discarding the explicit
pattern variable bindings and applying $\MO{UnelabType}$ to reconstruct
the type declaration:
For data type declarations, reverse elaboration proceeds as follows, applying $\MO{UnelabType}$
for each of the top level type declarations:
\subsection{Elaboration Properties}
Elaboration satisfies two important properties. We limit our discussion of
these properties to \IdrisM{} without type classes, i.e. elaboration of type
declarations, functions, and data types. This is primarily because there is not
enough information in a \TT{} program alone to reverse elaboration fully. However, since
elaboration of the higher level \Idris{} constructs is implemented in terms of
the lower level \IdrisM{} constructs, we should not consider this a serious
Informally stated, the properties that elaboration satisfies are
i) that if elaboration is successful, the
resulting program is a well-typed \TT{} program; ii) elaboration preserves the
meaning of the original \Idris{} program. The first property is true by the
definition of elaboration --- elaboration fails if it attempts to construct an ill-typed
term at any point. Furthermore, the development calculus \TTdev{} ensures that
partial constructions are well-typed.
The second property can be stated as the following conjecture:
\textbf{Conjecture: Preservation of meaning}\\
Given an \IdrisM{} declaration $\vd$, which is either a type declaration, a
pattern match clause, or a data type declaration,
if $\MO{Elab}\:\vd\:\mq\:\vt$, and $\MO{Unelab}\:\vt\:\mq\:\vd'$,
then $\MO{Match}\:\vd\:\vd'$ produces a valid match.
The output of $\MO{Unelab}$ is not necessarily equal to the input of $\MO{Elab}$
because elaboration fills in placeholder subexpressions. Therefore it suffices for
the input to match the output.
We have not yet proved this conjecture. Its truth depends on the implementation
of $\MO{Elab}$ faithfully translating each construct, and we observe that the
present description of $\MO{Elab}$ elaborates each non-placeholder subexpression
according to the structure of the expression. However, since the truth of this
conjecture is crucial to the correctness of the implementation, the elaborator
checks \emph{dynamically} that meaning is preserved by evaluating
$\MO{Unelab}\:\vt$ and matching the input against the result. In practice, this
does not have a significant impact on performance.