小编H. *_*ser的帖子

定义此数据类型:

data NaturalNumber = Zero | S NaturalNumber
    deriving (Show)

在Haskell中(使用GHC编译),此代码将在没有警告或错误的情况下运行:

infinity = S infinity
inf1 = S inf2
inf2 = S inf1

因此,递归和相互递归的无限深度值都会通过类型检查.

但是,以下代码给出了错误:

j = S 'h'

错误说明Couldn't match expected type ‘NaturalNumber’ with actual type 'Char'.即使我设置,(相同)错误仍然存​​在

j = S (S (S (S ... (S 'h')...)))

有一百个左右的嵌套S.

Haskell怎么能说这infinity是一个有效的成员NaturalNumber但j不是？

有趣的是,它还允许:

bottom = bottom
k = S bottom

Haskell只是试图证明一个程序的不正确性,如果它不能这样做,那么允许它吗？或者Haskell的类型系统不是图灵完整的,所以如果它允许程序那么程序可证明(在类型级别)正确吗？

(如果类型系统(在Haskell的形式语义中,而不仅仅是类型检查器)是Turing完成的,那么它将无法实现某些正确类型的程序是正确的,或者某些错误输入的程序是不正确的,因为它的不可判定性停止问题.)