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

Question

在之前使用 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 函数在给定任何输入以产生任何输出时进行类型检查，如 evil 函数所示。起初，我以为我可能意外地实现了 unsafeCoerce ，但事实并非如此:实际上尝试调用我的 convertFoo 函数(例如，通过执行类似 evil 3 的操作)只是进入了无限循环。

我有点模糊地理解正在发生的事情。我对这个问题的理解是这样的:

我定义的 ConvertFoo 实例适用于任何输入和输出， a 和 b ，仅受转换函数必须存在于 a -> Foo 和 Foo -> b 的两个附加约束的限制。

不知何故，该定义能够匹配任何输入和输出类型，因此似乎对 convertFoo :: a -> Foo 的调用正在选择 convertFoo 本身的定义，因为无论如何它是唯一可用的定义。

由于 convertFoo 无限调用自身，函数进入一个永不终止的无限循环。

由于 convertFoo 永远不会终止，该定义的类型是底部，所以从技术上讲，没有任何类型被违反，并且程序类型检查。

现在，即使上面的理解是正确的，我仍然对为什么整个程序进行类型检查感到困惑。具体来说，鉴于不存在此类实例，我预计 ConvertFoo a Foo 和 ConvertFoo Foo b 约束会失败。

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

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

Answer 1

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

类型类惊喜

看看这里发生了什么，要提高赌注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是真的，如果...

Convert a X为真[假设为真]

和 Convert X X是真的

Convert X X是真的，如果...

Convert X X为真[假设为真]

Convert X X为真[假设为真]

Convert X b是真的，如果...

Convert X X是真的[从上面看是真的]

和 Convert X b为真[假设为真]

类型检查器让我们感到惊讶。我们不期望Convert X X成为
真的，因为我们还没有定义任何类似的东西。但是(Convert X X, Convert X X) => Convert X X是一种重言式:它是
自动为真，无论在类中定义什么方法，它都是真的。

这可能与我们的类型类心智模型不匹配。我们预计
编译器在这一点上呆住并提示 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上
(一个无害的扩展，本质上只是句法)，我们得到一个
关于违反 Paterson conditions 之一的警告:

...
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只能无限循环或抛出一个
异常(exception)或通常触底，因为我们信任 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

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