上一篇 LdBeth：NuPRL 中的证明 III–我不做metavariable啦
Part I: Atom type
可能有之前用过 Agda 的人会在开始用 NuPRL 以后觉得，没有 inductive type definition，只有 product 和 disjoint union 但是没有区分 data constructor 的类型，好不习慣啊。
其实这个也不是什么大问题，data constructor 可以用 NuPRL 的 Atom 类型来模拟。
Atom 頋名思义就和 lisp 里的 symbol 类似，可以比较相等。
所以一个 inductive data type definition 的 tree
data Tree a = Node (Tree a) (Tree a) | Leaf a
可以表示成个 dependent pair
${\bf DEF\ }Tree(a) = rec(T. \Sigma x : {\tt Atom}. {\tt if}\ x =_A {\tt"Node"then\ } T \times T {\ \tt else\ if\ } x =_A {\tt"Leaf"then\ } a\ { \tt else\ } \it Void)\\ {\bf DEF\ }Node(a,b) = \langle {\tt"Node"}, \langle a, b \rangle\rangle \\ {\bf DEF\ }Leaf(a) = \langle {\tt"Leaf"}, a\rangle \\ \forall T : Type. Tree(T) \in Type\\ \forall T : Type. \forall a,b : Tree(T). Node(a,b) \in Tree(T)\\ \forall A: Type. \forall a : A. Leaf(a) \in Tree(A)$
想要 extensible record 也可以哦。
$\{L_1=T_1, L_2 = T_2 ...\} = \Pi x. {\tt if\ }x =_A L_1\ {\tt then\ } T_1\ {\tt else\ } {\tt if\ }x =_A L_2\ {\tt then\ } T_2 {\ \tt else} ... {\tt else\ } \it Top$
Part II: Partial Type Theory
这里我们讲下 NuPRL 特色的 partial type theory。
partial type theory 引入了 bar type, 如有一个 type T 且其 member 都是 convergent term，即 evaluation terminal 且 eval to canonical form (canonical 的定义见 NuPRL manual), $\overline{T}$ 就表示类型为 T 的所有 member，也就是属于 T 的 convergent term，以及所有 divergent term，也就是那些 non terminal 的 term。 $\overline{T}$ 定义了个 equal relation，在属于 T 的 equal relation 保留前提下 ( $t_1 = t_2 \in T \vdash t_1 =t_2 \in \overline{T}$ )，所有 divergent term 相等，而且 convergent term 不会等于 divergent term。有一个特別的 type 叫 Base， $Base = \overline{Value}$ ，Value 是所有 canonical term 的类型。
通常意义上的 partial function 就可以用 type $A \rightarrow \overline{B}$ 表示。而通过 fixpoint principle，general recursive function 也能给定类型:
$e \in \overline{T} \rightarrow \overline{T}\Rightarrow {\it fix}(e) \in \overline{T}$
练习:
$A \rightarrow \overline{B}, \overline{A} \rightarrow \overline{B}, \overline{A \rightarrow B}$ 的区別？
Part III: Very Dependent Type
众所周知 dependent function type (Pi type) 是 functions type 和 sum type 的 generalization，dependent product type (Sigma type) 是 sum type 和 product type 的 generalization，其实还有个是 Pi 和 Sigma 的 generalization 的，形为
$\{ f\; |\; x:A \rightarrow B[f,x] \}$
注意这里的 notation 和 refinement type 类似，但是不同的意思。例如 $\{f\; |\; x: \mathbb{N} \rightarrow \{a:\mathbb{N}\;|\; a < x\}\}$ 就相当于 dependent function type $x: \mathbb{N} \rightarrow \{a:\mathbb{N}\;|\; a < x\}$ 。
有了这个就能在 NuPRL 里定义 dependent record 了
$\begin{align*} & \{\pi_1 = a : A, \pi_2 = B[a]\}\\ &\; =\\ & \{f\; |\; l:{\it Atom} \rightarrow {\tt if}\ l =_A \pi_1\ {\tt then} \ A\ {\tt else\ if}\ l=_A \pi_2\ {\tt then}\ B[f\ \pi_1]\ {\tt else}\ \it Top \} \end{align*}$
Note
Partial Objects in Constructive Type Theory
Type-Theoretic Methodology for Practical Programming Languages