如果我写一些
data L t = Empty | L t (L t)
在haskell中，这种类型允许无限列表，如L 1 (L 2 (L 3 (..)))。在严格语言（如ML）中，等价的代数类型定义是否也允许无限列表？如果是，是否是语言求值机制的缺陷，无法实际给它一个无限列表？如果不是，ML如何从该类型中排除无限列表？其次，从理论的Angular 来看，类型中的值的类是某个生成函数的最小不动点吗？（比较一下，像阶乘这样的递归函数定义的值是相关生成函数的lfp）
L 1 (L 2 (L 3 (..)))
e3bfsja21#
在OCaml中有循环列表：
let rec c = 1 :: 2 :: 3 :: c
ML如何从该类型中排除无限列表？如果禁止对非函数类型进行递归定义，那么就无法构造无限列表。从理论的观点来看，类型中的值的类是某个生成函数的最小不动点吗？不动点确实是在指称语义中建模类型的一种常用方法。首先，从符号上看，我们可以看到：
L a = Nil | Cons a (L a)
使L a成为F的固定点：
L a
F
F x = Nil | Cons a x
事实上，我们已经：
L a = F (L a)
这里Nil表示单位空间，Cons a x是a和x的乘积，|是和。根据"空间"和那些运算（单位、乘积和求和）的含义，您会得到不同的结果。
Nil
Cons a x
a
x
|
⊥ : ⊥ : ⊥
1条答案
按热度按时间e3bfsja21#
在OCaml中有循环列表：
ML如何从该类型中排除无限列表？
如果禁止对非函数类型进行递归定义，那么就无法构造无限列表。
从理论的观点来看，类型中的值的类是某个生成函数的最小不动点吗？
不动点确实是在指称语义中建模类型的一种常用方法。首先，从符号上看，我们可以看到：
使
L a成为F的固定点：事实上，我们已经：
这里
Nil表示单位空间，Cons a x是a和x的乘积，|是和。根据"空间"和那些运算（单位、乘积和求和）的含义，您会得到不同的结果。
⊥ : ⊥ : ⊥...）作为上述F的初始代数和最终余代数（当讨论代数结构上（而不是代数结构上）的运算时，"最小不动点"和"最大不动点"的推广）。