diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/systemt.ltx | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 8fcedd1..8b3f173 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -109,24 +109,27 @@ and test equality recursively. In the remainder of the section we outline four different strategies for encoding inductive types within System~T. We judge each encoding on whether it -is a local, simply-typed transformation as well as how easy it is to hand write -the three fundamental operators. As you can see from the summary in -\cref{tbl:encodings}, each strategy is lacking in some regard. +can encode inductive types with higher-order data such as functions; is a local, +simply-typed transformation that does not require polymorphism or a global +program analysis; as well as how easy it is to hand write the three fundamental +operators. As you can see from the summary in \cref{tbl:encodings}, each +strategy is lacking in some regard. \begin{table} \caption{Comparison of encoding strategies for inductive types within - System~T. The first column assesses if the strategy is a local, simply-typed - transformation. The remainder indicate whether it is ``easy'' to hand write - the constructors, fold and pattern matching + System~T. The first two columns assesses whether a strategy works for + higher-order types and is a local, simply-typed transformation. The + remainder indicate whether it is ``easy'' (\ding{51}) or possible + (\ding{81}) to hand write the constructors, fold and pattern matching respectively.}\label{tbl:encodings} - \begin{tabular}{lcccc} + \begin{tabular}{lccccc} \toprule - Strategy & Local & Constructors & Fold & Pattern Match \\ + Strategy & Higher Order & Local & Constructors & Fold & Pattern Match \\ \midrule - G\"odel & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\ - Church & \ding{55} & \ding{51} & \ding{51} & \ding{55} \\ - Eliminator & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\ - Heap & \ding{51} & \ding{55} & \ding{51} & \ding{51} \\ + G\"odel & \ding{55} & \ding{51} & \ding{51} & \ding{81} & \ding{51} \\ + Church & \ding{51} & \ding{55} & \ding{51} & \ding{51} & \ding{81} \\ + Eliminator & \ding{51} & \ding{51} & \ding{51} & \ding{55} & \ding{51} \\ + Heap & \ding{51} & \ding{51} & \ding{81} & \ding{81} & \ding{51} \\ \bottomrule \end{tabular} \end{table} |