diff options
| -rw-r--r-- | sec/reducer.ltx | 39 |
1 files changed, 38 insertions, 1 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx index 1751b91..82706ed 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -137,9 +137,46 @@ unannotated System~T terms as in \cref{lst:term-ty}. Each phase is accompanied by its own inductive types representing types and type-annotated terms. +Folds in \lang{} are destructive---the inductive components used to +generate the induction hypothesis are unnamed. This has some +interesting interactions with encoding the \(\mathsf{distrib}\) term +in phase one, and implementing the \mapkw{} pseudo-operator in phase +two. Both of these functions are defined by induction on types with +motives that are functions returning terms. This means that the +inductive hypothesis for each branch consists of a type constructor +filled with some number functions. To construct a term, we need not +only the subterms provided by the induction hypothesis, but we also +need the types of those subterms. To preserve this typing information, +both \(\mathsf{distrib}\) and \mapkw{} must return a pair of type and +term. + +\begin{listing} + \begin{verbatim} +; Arrow p => + let myTy = ~(Arrow <Dom: p.Dom.Ty []; Cod: p.Cod.Ty []>) in + < Ty: \env => myTy + ; Term: \env, k, s => ~(Abs ~(Abs ~(Tup + [ <Ty: s; Term: ~(Var 0)> + ; <Ty: myTy; Term: ~(Var 1)>]))) + > + \end{verbatim} + \caption{The branch of \(\mathsf{distrib}\) corresponding to + function types.}\label{lst:distrib-arrow} +\end{listing} + +As a concrete example, consider the branch of \(\mathsf{distrib}\) +over a function type, shown in \cref{lst:distrib-arrow}. The induction +hypothesis is a pair of motives generated from the domain and +codomain. The motive is a pair of functions. The \verb|Ty| component +takes an environment and returns a compiled type. The \verb|Term| +component takes an environment, a chosen type variable \verb|k| and a +type \verb|S| and returns a term distributing an accumulator for +\verb|S| at index \verb|k| outside of the type constructor. Ideally, +we would only need the \verb|Term| component of the pair. However, the +type annotations needed for the tuple force us to also compute the types. + \TODO{ \begin{itemize} - \item show a ``non-destructive'' fold \item justify use of destructive folds \end{itemize} } |