笔记5
Inductive and Co-Inductive Types ¶
inductive type一个很直观的例子是自然数类型 nat
之前的定义是
zero : nat
n: nat |- succ(n) : nat
现在我们引入新的定义
Gamma |- e : unit + nat
------------------
Gamma |- fold(nat, e) : nat
fold(nat, e) 是 nat 的唯一引入形式。在这样的表达式里， z 被定义为 fold(nat, l) 而 s(e) 被定义为 fold(nat, e)
另一个不错的例子是 stream. 熟悉 Haskell 的会知道Haskell内存在无限列表这样的东西。
在之前，我们的递归类型需要递归到把所有值都计算出来，stream相反，需要什么就计算什么
其中 hd(e) 为 head of the stream