为什么使用 UndecidableInstances 编译此代码，然后生成运行时无限循环？

当使用编写一些代码时UndecidableInstances早些时候，我遇到了一些我觉得很奇怪的事情。我无意中创建了一些代码，当我认为不应该进行类型检查时：

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

data Foo = Foo

class ConvertFoo a b where
  convertFoo :: a -> b

instance (ConvertFoo a Foo, ConvertFoo Foo b) => ConvertFoo a b where
  convertFoo = convertFoo . (convertFoo :: a -> Foo)

evil :: Int -> String
evil = convertFoo

具体来说，convertFoo给定时进行函数类型检查any输入生产any输出，如所示evil功能。起初，我以为也许我不小心实现了unsafeCoerce，但这并不完全正确：实际上试图打电话给我convertFoo功能（通过做类似的事情evil 3，例如）只是进入无限循环。

I sort of模糊地理解正在发生的事情。我对这个问题的理解是这样的：

• 的实例ConvertFoo我定义的作品any输入和输出，a and b，仅受转换函数必须存在的两个附加约束的限制a -> Foo and Foo -> b.
• 不知何故，该定义能够匹配任何输入和输出类型，因此看起来调用convertFoo :: a -> Foo正在选择的定义convertFoo本身，因为无论如何它是唯一可用的。
• Since convertFoo无限地调用自身，该函数就会进入一个永远不会终止的无限循环。
• Since convertFoo永远不会终止，该定义的类型是底部，所以技术上没有任何类型被违反，并且程序会进行类型检查。

现在，即使上述理解是正确的，我仍然对为什么整个程序进行类型检查感到困惑。具体来说，我希望ConvertFoo a Foo and ConvertFoo Foo b假设不存在这样的实例，则约束会失败。

I do理解（至少模糊地）在选择实例时约束并不重要——仅根据实例头来选择实例，然后检查约束——所以我可以看到这些约束可能会很好地解决，因为我ConvertFoo a b例如，这是尽可能宽松的。然而，这将需要解决相同的约束集，我认为这会将类型检查器置于无限循环中，导致 GHC 要么挂起编译，要么给我一个堆栈溢出错误（后者是我见过的）前）。

但显然，类型检查器确实not循环，因为它很高兴触底并愉快地编译我的代码。为什么？在这个特定的例子中，实例上下文是如何满足的？为什么这不会给我一个类型错误或产生类型检查循环？

我完全同意这是一个很好的问题。它讲述了如何 我们对类型类的直觉与现实不同。

类型级惊喜

为了看看这里发生了什么，要提高赌注 键入签名evil:

data X

class Convert a b where
  convert :: a -> b

instance (Convert a X, Convert X b) => Convert a b where
  convert = convert . (convert :: a -> X)

evil :: a -> b
evil = convert

显然Covert a b正在选择实例，因为只有 该类的一个实例。类型检查员正在思考类似的事情 这：

• Convert a X is true if...
  • Convert a X是真的[假设为真]
  • and Convert X X is true
    • Convert X X is true if...
      • Convert X X是真的[假设为真]
      • Convert X X是真的[假设为真]
• Convert X b is true if...
  • Convert X X是真的[上面的说法是正确的]
  • and Convert X b是真的[假设为真]

类型检查器让我们感到惊讶。我们不期望Convert X X成为 确实如此，因为我们还没有定义类似的东西。但(Convert X X, Convert X X) => Convert X X是一种同义反复：它是 自动为 true，并且无论类中定义了什么方法，它都是 true。

这可能与我们的类型类心智模型不符。我们期望 编译器此时呆住并抱怨如何Convert X X不可能是真的，因为我们没有为它定义任何实例。我们期待 编译器站在Convert X X，寻找另一个地点 步行到哪里Convert X X是真的，并且放弃，因为有 没有其他地方是这样的。但编译器能够 递归！递归、循环并实现图灵完备。

我们为类型检查器提供了这种功能，我们是用UndecidableInstances。当文档指出它是 可以将编译器发送到循环中，很容易假设 最糟糕的是，我们假设坏循环总是无限循环。但 在这里，我们演示了一个更致命的循环，一个循环终止——除了以一种令人惊讶的方式。

（丹尼尔的评论更加明显地证明了这一点：

class Loop a where
  loop :: a

instance Loop a => Loop a where
  loop = loop

.)

不可判定性的危险

这正是这种情况UndecidableInstances允许。如果我们关闭该扩展并打开FlexibleContexts在 （一个无害的扩展，本质上只是句法），我们得到一个 对违反其中一项规定的行为发出警告帕特森 状况 https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.html#instance-termination-rules:

...
Constraint is no smaller than the instance head
  in the constraint: Convert a X
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’

...
Constraint is no smaller than the instance head
  in the constraint: Convert X b
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’

“不小于实例头”，尽管我们可以在心里重写它 因为“这个实例可能会被用来证明以下断言 它本身会给你带来很多痛苦、咬牙切齿和打字。” Paterson 条件共同防止实例解析中出现循环。 我们在这里的违规行为表明了为什么它们是必要的，我们可以 大概可以查阅一些论文来了解为什么它们足够了。

触底反弹

至于为什么程序在运行时无限循环：有无聊的地方 回答，哪里evil :: a -> b只能无限循环或抛出一个 例外或通常触底，因为我们信任 Haskell 类型检查器并且没有可以居住的值a -> b除了 底部。

一个更有趣的答案是，因为Convert X X是 同义反复，它的实例定义就是这个无限循环

convertXX :: X -> X
convertXX = convertXX . convertXX

我们可以类似地展开Convert A B实例定义。

convertAB :: A -> B
convertAB =
  convertXB . convertAX
  where
    convertAX = convertXX . convertAX
    convertXX = convertXX . convertXX
    convertXB = convertXB . convertXX

这种令人惊讶的行为，以及如何限制实例解析（通过 默认不带扩展名）是为了避免这些 行为，也许可以被视为哈斯克尔的一个很好的理由 类型类系统尚未得到广泛采用。尽管其 令人印象深刻的人气和力量，但也有一些奇怪的角落（无论是 它在文档或错误消息或语法中，甚至可能在 它的基本逻辑）似乎特别不适合我们人类的方式 考虑类型级抽象。