haskell - 类型级 Peano 数和 UndecidableInstances

Question

正在关注 this tutorial ，我有以下代码:

{-# LANGUAGE DataKinds, TypeFamilies #-}

data Nat = Z | S Nat

type family   Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z     m = m
type instance Plus (S n) m = S (Plus n m)

到目前为止一切顺利。我知道 DataKinds 会自动将类型提升为种类，而 TypeFamilies 会启用类型级函数。

然后我添加:

type family Mul (m :: Nat) (n :: Nat) :: Nat
type instance Mul Z     m = Z
type instance Mul (S n) m = Plus m (Mul n m)

编译给我:

Nested type family application
  in the type family application: Plus m (Mul n m)
(Use UndecidableInstances to permit this)
In the type instance declaration for ‘Mul’

这个扩展的名字很吓人。有人说要avoid它，以及我试过阅读的关于这个扩展的解释对我来说没有意义。

寻求一些帮助来理解错误，为什么它会出现在这个例子中，undecidable 在这种情况下的含义是什么，以及在什么情况下这个扩展和它一样可怕声音？

Answer 1

其实并不可怕。它禁用试图确定类型族和实例定义终止的(相当弱的)GHC 检查。因此，其最坏情况下的行为是非终止类型检查。然而，大多数情况下我们得到的是错误消息而不是实际的循环，因为循环经常超出类型检查器中的堆栈限制。我们不会得到不安全、不连贯或任何其他可能对程序稳健性或推理产生不利影响的属性。

“Undecidable”可能是一个比保证更强烈的表达，因为它只表示 GHC 无法决定定义是否正在终止。在许多情况下，GHC 对于这项工作来说太弱了，而其他依赖语言的编译器将能够毫无问题地检查终止。对于 GHC，UndecidableInstances 通常也需要明显的终止定义，在这种情况下，它的使用是非常合理的。