Haskell/GHC UndecidableInstances - 非终止类型检查的示例？

Question

我写了一些需要 -XUndecidableInstances 来编译的 Haskell 代码。我确实理解为什么会发生这种情况，因为违反了某个条件，因此 GHC 大喊大叫。

但是，我从未遇到过类型检查器实际上会挂起或陷入无限循环的情况。

非终止实例定义是什么样的 - 你能举个例子吗？

Answer 1

this paper from HQ 中有一个经典的，有点令人震惊的例子(涉及与函数依赖的交互)。 :

class Mul a b c | a b -> c where
  mul :: a -> b -> c
instance Mul a b c => Mul a [b] [c] where
  mul a = map (mul a)

f b x y = if b then mul x [y] else y

我们需要 mul x [y]具有与 y 相同的类型，所以，取 x :: x和 y :: y ， 我们需要

instance Mul x [y] y

根据给定的例子，我们可以拥有。当然，一定要带 y ~ [z]对于一些 z这样

instance Mul x y z

IE。

instance Mul x [z] z

我们处于一个循环中。

这很令人不安，因为 Mul instance 看起来它的递归在结构上是减少的，这与 Petr 的答案中明显的病态实例不同。然而，它使 GHC 循环(使用无聊阈值来避免挂起)。

问题是，我确信我在某处提到过，是标识 y ~ [z]。尽管 z在功能上取决于 y .如果我们对函数依赖使用函数表示法，我们可能会看到约束表示 y ~ Mul x [y]并拒绝替换，因为它违反了发生检查。

很感兴趣，我想我会试一试，

class Mul' a b where
  type MulT a b
  mul' :: a -> b -> MulT a b

instance Mul' a b => Mul' a [b] where
  type MulT a [b] = [MulT a b]
  mul' a = map (mul' a)

g b x y = if b then mul' x [y] else y

与 UndecidableInstances启用，循环超时需要相当长的时间。与 UndecidableInstances禁用，实例仍然被接受并且类型检查器仍然循环，但是截止发生得更快。

所以...有趣的旧世界。