diff options
| -rw-r--r-- | sec/compiler.ltx | 23 |
1 files changed, 20 insertions, 3 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx index decb2af..cfb5be5 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -219,11 +219,28 @@ have not done this. Our more lax certificates are still sufficiently expressive to prove a term cannot have both a positive and negative certificate. +\TODO{explain the derivation is runtime erased} + +Like with the well-scoped AST, we have the choice for type checking to +produce an intrisically well-typed AST.\@ We have opted against it +because it is harder to express the relation between the input and +output terms. Consider the hypothetical signature of the type +synthesis function for an intrinsically well-typed AST: +\begin{verbatim} +synths : Term context -> (env : TyEnv context) -> Maybe (a : Ty ** WfTerm env a) +\end{verbatim} +The result does not depend on the given input term, so we can give a +trivial implementation such as the function constantly returning a +well-typed closed term. Compare this to a (simplified) signature for +synthesis with an extrinsic certificate: +\begin{verbatim} +synths : (tm : Term context) -> (env : TyEnv context) -> Maybe (a : Ty ** SynthsTy env tm a) +\end{verbatim} +The result explicitly depends on the input invalidating the trivial +implementation. + \TODO{ \begin{itemize} - \item explain the derivation is runtime erased - \item justify extrinsic derivation - \item justify the derivation having no runtime cost \item describe why knowing there is a derivation is necessary \item explain why these extra features do not guarantee compiler correctness \end{itemize} |