diff options
| -rw-r--r-- | main.tex | 6 | ||||
| -rw-r--r-- | sec/encoding.ltx | 35 |
2 files changed, 32 insertions, 9 deletions
@@ -245,7 +245,10 @@ \newcommand\arb{\ensuremath{\mathsf{arb}}} %% Recursive types -\newcommand\roll{\ensuremath{\mathsf{roll}}} +\ExplSyntaxOn +\NewDocumentCommand \roll {s} + { \ensuremath{\mathsf{roll} \IfBooleanT{#1}{'}} } +\ExplSyntaxOff \newcommand\unroll{\ensuremath{\mathsf{unroll}}} \newcommand\foldkw{\ensuremath{\mathsf{fold}}} \newcommand\foldtm[3]{\foldkw~{#1}~\mathsf{with}~{{#2}.~{#3}}} @@ -331,6 +334,7 @@ { {#1} [ \squid_checksub [] #2 } \ExplSyntaxOff +\newcommand\submult[2]{{#1}[ {#2} ]} %% Document %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 8087e20..ffc868b 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -72,15 +72,34 @@ the \roll*{} operator, which has the following type derivation: \] Rather than include the inductive values within the term to roll, they are instead gathered into an external list. The places that contained inductive -values in the rolled term now contain indices into the list. +values in the rolled term now contain indices into the list. The new operator +satisfies the following equation: +\[ +\dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u} +\] -\TODO{ - \begin{itemize} - \item justify why I add lists as a built-in type former - \item describe the strength function, the key step in this phase - \item state it is defined by induction on the outer functor - \end{itemize} -} +\TODO{justify why I add lists as a built-in type former} + +To encode \roll{} into \roll*{} we require a function that traverses a term of +type \(\sub{A}{X/\mu X. A}\) and collects all inductive values into a single list. +We can extend a list with a single value and return the index of that value with +the writer monad~\cite{writer}: \(\mathsf{extend} : A \to \mathsf{List}~A \to +\mathsf{List}~A \times \nat\). By using the \mapkw{} operator we can replace all +inductive values in a term \(\sub{A}{X/\mu X. A}\) with accumulator functions +\(\sub{A}{X/\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times \nat}\). The +non-trivial step is ``distributing'' the writer monad with the substitution to +obtain a value of type \(\mathsf{List}~(\mu X. A) \to \mathsf{List}~(\mu X. A) \times +\sub{A}{X/\nat}\). We can apply this function to the empty list to obtain the +arguments for \roll*{}. + +Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X \in +\Psi\), a type environment \(\alpha\) and a type \(S\), we have a term +\(\mathsf{distrib}\) defined in phase-one \lang{} of type +\[ +\submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha} +\] +that calls each accumulator within \(A\) in sequence. The definition is by +induction on the well-formedness derivation. \TODO{ \begin{itemize} |