Haskell如何进行类型检查无限递归值？

Question

定义此数据类型:

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完成的,那么它将无法实现某些正确类型的程序是正确的,或者某些错误输入的程序是不正确的,因为它的不可判定性停止问题.)

Answer 1

好

S :: NaturalNumber -> NaturalNumber

在

infinity = S infinity

我们首先假设什么:我们分配infinity一些未解决的类型_a并试图找出它是什么.我们知道我们已经应用S了infinity,所以_a必须是构造函数类型中箭头左侧的任何内容,即NaturalNumber.我们知道这infinity是应用程序的结果S,所以infinity :: NaturalNumber,再次(如果我们为此定义得到两个冲突类型,我们必须发出类型错误).

类似的推理适用于相互递归的定义.inf1必须是一个NaturalNumber,因为它似乎作为参数传递给S在inf2; inf2必须是NaturalNumber因为它是结果S; 等等

通用算法是分配定义未知类型(值得注意的例外是文字和构造函数),然后通过查看每个定义的使用方式来创建对这些类型的约束.例如,这必须是某种形式的列表,因为它是reversed,并且这必须是Int因为它被用于从a IntMap等查找值.

如果是

oops = S 'a'

'a' :: Char因为它是一个文字,但是,我们必须拥有'a' :: NaturalNumber它,因为它被用作参数S.我们得到明显的伪造约束,即文字的类型必须是Char和NaturalNumber,这会导致类型错误.

并在

bottom = bottom

我们一开始bottom :: _a.唯一的约束是_a ~ _a,因为正在使用type _a(bottom)的值,其中type的值_a是预期的(在定义的RHS上bottom).由于没有什么可以进一步约束类型,因此未解决的类型变量是通用的:它受到通用量词的约束而产生bottom :: forall a. a.

注意bottom上面的两个用法_a在推断类型的同时具有相同的类型()bottom.这打破了多态递归:其定义中每次出现的值都与定义本身的类型相同.例如

-- perfectly balanced binary trees
data Binary a = Leaf a | Branch (Binary (a, a))
-- headB :: _a -> _r
headB (Leaf x) = x -- _a ~ Binary _r; headB :: Binary _r -> _r
headB (Branch bin) = fst (headB bin)
-- recursive call has type headB :: Binary _r -> _r
-- but bin :: Binary (_r, _r); mismatch

所以你需要一个类型签名:

headB :: {-forall a.-} Binary a -> a
headB (Leaf x) = x
headB (Branch bin) = fst (headB {-@(a, a)-} bin)
-- knowing exactly what headB's signature is allows for polymorphic recursion

所以:当某些东西没有类型签名时,类型检查器会尝试为它分配一个类型,如果它遇到伪造的约束,它会拒绝该程序.当某些东西有一个类型签名时,类型检查器会进入它,以确保它是正确的(如果你喜欢这样想的话,试图证明它是错误的).

Haskell的类型系统不是Turing完整的,因为有很多语法限制来防止例如类型lambdas(没有语言扩展),但它不足以确保所有程序运行完成而没有错误,因为它仍然允许底部(更不用说所有不安全的功能).它提供了较弱的保证,如果程序在不使用不安全功能的情况下运行完成,它将保持类型正确.在GHC下,通过足够的语言扩展,类型系统确实成为​​图灵完整的.我不认为它允许通过不良类型的程序; 我认为你能做的最多就是将编译器抛入无限循环.