Agn*_*yay 1 haskell type-theory
显然,在Haskell中有一种称为无限类型的东西.
例如,当我尝试iterate concatGHCi时,我得到了这个:
*Main> iterate concat
<interactive>:24:9: error:
• Occurs check: cannot construct the infinite type: a ~ [a]
Expected type: [a] -> [a]
Actual type: [[a]] -> [a]
• In the first argument of ‘iterate’, namely ‘concat’
In the expression: iterate concat
In an equation for ‘it’: it = iterate concat
• Relevant bindings include
it :: [a] -> [[a]] (bound at <interactive>:24:1)
我的问题是,究竟什么是无限类型？它们如何适应类型理论以及我可以从哪些资源中了解它们？有没有允许无限类型的编程语言？
显然,在Haskell中有一种称为无限类型的东西.
由于Haskell类型检查器每次出现无限类型时都会引发类型错误,我想说Haskell 中没有无限类型.
无论如何,"无限"类型指的是类型本身出现了多少类型构造函数.例如[[Int]] -> Bool提到[], Bool, Int, (->),所以它是有限的.如果我们可以type L = [[[[...]]]]使用无限多的嵌套来编写,我们将拥有一个无限类型:一个类型,其值是列表列表的列表......永远.
在类型推断期间,通过统一可能会产生无限类型.如果我写
let x = [x] in ...
那么如果T是类型x,它也必须是[x]定义的类型.但是,后者显然有类型[T].因此,我们必须解决方程T = [T],其解决方案将导致L上面讨论的无限类型.
与几乎所有编程语言一样,Haskell拒绝无限类型,因为它们通常是程序员错误的症状.此外,我想添加无限(常规)类型可以使类型检查更加困难.我不记得有关无限类型的任何理论结果,但如果类型检查变得不可判,我也不会感到惊讶.