使用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要么挂在编译中，要么给我一个堆栈溢出错误（我已经看到了后者）之前）。
但是，很显然，类型检查器不会循环，因为它很容易触底并愉快地编译我的代码。为什么？在此特定示例中如何满足实例上下文？为什么这不会给我带来类型错误或产生类型检查循环？
我完全同意这是一个很大的问题。它说明了我们对类型类的直觉与现实之间的差异。
要查看这里发生了什么，将增加以下类型签名的赌注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条件之一的警告：
...
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除了bottom之外，没有其他值可以存在。
一个更有趣的答案是，由于从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的类型类系统尚未得到广泛采用的一个很好的理由。尽管它具有令人印象深刻的受欢迎程度和强大功能，但它仍然存在奇怪的角落（无论是在文档，错误消息，语法还是什至在其底层逻辑中），似乎特别不适合我们人类对类型级抽象的看法。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句