26

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

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

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

4

2 回答 2

40

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实例看起来它的递归在结构上是减少的，这与 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实例仍然被接受并且类型检查器仍然循环，但是截止发生得更快。

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

于 2013-02-02T13:00:27.927 回答
20

例如：

{-# LANGUAGE UndecidableInstances #-}

class C a where
    f :: a -> a

instance C [[a]] => C [a] where
    f = id

g x = x + f [x]

发生了什么：键入f [x]时编译器需要确保x :: C [a]对于某些a. 实例声明说只有当它也是xtype时才可以是 type 。所以编译器需要确保，等等，并陷入无限循环。C [a]C [[a]]x :: C [[a]]

另请参阅是否可以在本地使用 UndecidableInstances pragma 对编译终止产生全局影响？

于 2013-02-02T11:12:18.653 回答