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

问题描述

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

  { - ＃LANGUAGE FlexibleInstances＃ - } 
 { - ＃语言MultiParamTypeClasses＃ - } 
 { - ＃LANGUAGE ScopedTypeVariables＃ - } 
 { - ＃LANGUAGE UndecidableInstances＃ - } 
 
 data Foo = Foo 
 
 class ConvertFoo ab其中
 convertFoo :: a  - > b 
 
实例（ConvertFoo a Foo，ConvertFoo Foo b）=> ConvertFoo a b其中
 convertFoo = convertFoo。 （convertFoo :: a  - > Foo）
 
 evil :: Int  - >字符串
邪恶= 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 ab 实例，它尽可能宽容。然而，那需要解决相同的一组约束，我认为这会将类型检查器置于一个无限循环中，导致GHC挂起编译或给我一个堆栈溢出错误（后者我见过

显然，typechecker并不是循环的，因为它开心地开始并编译我的代码。为什么？在这个特定的例子中，实例上下文是如何满足的？为什么这不会给我一个类型错误或产生一个类型检查循环？

解决方案

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

类型类惊喜

看看这里发生了什么，打算为 evil 加
类型签名的赌注：

  data X 
 
 class转换ab其中
 convert :: a  - > b 
 
实例（转换X，转换X b）=>转换一个b 
 convert = convert。 （convert :: a  - > X）
 
 evil :: a  - > b 
 evil =转换
  

显然 Covert ab 实例被选中，因为这个类只有
一个实例。 Typechecker认为像这样的
：

转换X 如果...

• 转换X 是真的[true假设]


• 和转换XX 为真
  
  
  
  
  • 如果...


    

    • 转换XX 为真，转换XX 为true [假设值为真]
    
    
    • 转换XX 为真[假设为真]
    
    
  
  

转换X b 是真的如果...

• 转换XX 是真实的[真实从上面]


• 和转换X b 为真[假设为真]
  

类型检测器让我们感到惊讶。我们并不期望 Convert X X 是
，因为我们没有定义类似的东西。但是（Convert X X，Convert X X）=>转换XX 是一种重言式：它是
自动为真，无论在课程中定义了什么方法，它都是真的。

编译器会在这一点上提出疑问，并抱怨 Convert X X
不能为真，因为我们没有为它定义任何实例。我们期望编译器的
位于 Convert XX 处，寻找另一个点
来到 Convert XX 是真的，并放弃，因为那里是
没有其他地方是真的。但编译器能够
递归！

我们用这种能力祝福了类型检测器，并且我们用
UndecidableInstances 。当文档声明它是
可能将编译器发送到一个循环时，很容易假设
最差，并且我们假设不良循环总是无限循环。但
在这里我们已经演示了一个更加致命的循环，一个循环，
终止 - 除非以一种令人惊讶的方式。

（这在Daniel的评论中更加明显地表现出来：

  class Loop a其中
 loop :: a 
 
实例Loop a => Loop a其中
 loop =循环
  

。

不可判定性的危险

这是 UndecidableInstances
允许。如果我们关闭该扩展并在
（本质上只是语法上的无害扩展）上打开 FlexibleContexts ，我们会收到关于违规的
警告其中一个：

  ... 
约束不小于实例头部
在约束中：转换一个X 
（使用UndecidableInstances来允许这个）
在'Convert a b'的实例声明中
 
 ... 
约束不小于约束中的实例头
：转换X b 
（使用UndecidableInstances来允许这个）
在'Convert a b'的实例声明中
  

不小于实例头部，尽管我们可以在脑海中将它重写为
，因为有可能使用此实例证明自己的
的断言，并引起你极大的痛苦并打个招呼和打字。
Paterson条件共同防止实例解析中的循环。
我们在这里的违规行为证明了为什么他们是必要的，我们可以
大概查阅一些论文，看看它们为什么是足够的。

h2>

至于为什么程序在运行时出现无限循环：有无聊的
答案，其中 evil :: a - > b 不能无限循环或抛出
异常，或者通常会触底，因为我们信任Haskell
类型检查器，并且没有可能存在的值 a - > b 除了
底部。

更有趣的答案是，自 Convert XX 的同义反义词，它的实例定义是这个无限循环

  convertXX :: X  - > X 
 convertXX = convertXX。 convertXX 
  

我们可以类似地扩展 Convert AB 实例定义。

  convertAB :: A  - > B 
 convertAB = 
 convertXB。 convertAX 
其中
 convertAX = convertXX。 convertAX 
 convertXX = convertXX。 convertXX 
 convertXB = convertXB。 convertXX 
  

这种令人惊讶的行为以及如何约束实例解析（由
默认为无扩展名）是这意味着要避免这些
行为，或许可以作为Haskell的
类型类系统为什么还没有被广泛采用的一个很好的理由。尽管其b $ b令人印象深刻的知名度和强大，但它有一些奇怪的角落（无论
是在文档中，错误消息还是语法中，还是甚至在
的基本逻辑中），都显得特别不适合我们人类
如何考虑类型抽象。

When writing some code using UndecidableInstances earlier, I ran into something that I found very odd. I managed to unintentionally create some code that typechecks when I believed it should not:

{-# 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

Specifically, the convertFoo function typechecks when given any input to produce any output, as demonstrated by the evil function. At first, I thought that perhaps I managed to accidentally implement unsafeCoerce, but that is not quite true: actually attempting to call my convertFoo function (by doing something like evil 3, for example) simply goes into an infinite loop.

I sort of understand what’s going on in a vague sense. My understanding of the problem is something like this:

• The instance of ConvertFoo that I have defined works on any input and output, a and b, only limited by the two additional constraints that conversion functions must exist from a -> Foo and Foo -> b.
• Somehow, that definition is able to match any input and output types, so it would seem that the call to convertFoo :: a -> Foo is picking the very definition of convertFoo itself, since it’s the only one available, anyway.
• Since convertFoo calls itself infinitely, the function goes into an infinite loop that never terminates.
• Since convertFoo never terminates, the type of that definition is bottom, so technically none of the types are ever violated, and the program typechecks.

Now, even if the above understanding is correct, I am still confused about why the whole program typechecks. Specifically, I would expect the ConvertFoo a Foo and ConvertFoo Foo b constraints to fail, given that no such instances exist.

I do understand (at least fuzzily) that constraints don’t matter when picking an instance—the instance is picked based solely on the instance head, then constraints are checked—so I could see that those constraints might resolve just fine because of my ConvertFoo a b instance, which is about as permissive as it can possibly be. However, that would then require the same set of constraints to be resolved, which I think would put the typechecker into an infinite loop, causing GHC to either hang on compilation or give me a stack overflow error (the latter of which I’ve seen before).

Clearly, though, the typechecker does not loop, because it happily bottoms out and compiles my code happily. Why? How is the instance context satisfied in this particular example? Why doesn’t this give me a type error or produce a typechecking loop?

解决方案

I wholeheartedly agree that this is a great question. It speaks to howour intuitions about typeclasses differ from the reality.

Typeclass surprise

To see what is going on here, going to raise the stakes on thetype signature for 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

Clearly the Covert a b instance is being chosen as there is onlyone instance of this class. The typechecker is thinking something likethis:

• Convert a X is true if...
  • Convert a X is true [true by assumption]
  • and Convert X X is true
    • Convert X X is true if...
      • Convert X X is true [true by assumption]
      • Convert X X is true [true by assumption]
• Convert X b is true if...
  • Convert X X is true [true from above]
  • and Convert X b is true [true by assumption]

The typechecker has surprised us. We do not expect Convert X X to betrue as we have not defined anything like it. But (Convert X X, Convert X X) => Convert X X is a kind of tautology: it isautomatically true and it is true no matter what methods are defined in the class.

This might not match our mental model of typeclasses. We expect thecompiler to gawk at this point and complain about how Convert X Xcannot be true because we have defined no instance for it. We expectthe compiler to stand at the Convert X X, to look for another spotto walk to where Convert X X is true, and to give up because thereis no other spot where that is true. But the compiler is able torecurse! Recurse, loop, and be Turing-complete.

We blessed the typechecker with this capability, and we did it withUndecidableInstances. When the documentation states that it ispossible to send the compiler into a loop it is easy to assume theworst and we assumed that the bad loops are always infinite loops. Buthere we have demonstrated a loop even deadlier, a loop thatterminates – except in a surprising way.

(This is demonstrated even more starkly in Daniel's comment:

class Loop a where
  loop :: a

instance Loop a => Loop a where
  loop = loop

.)

The perils of undecidability

This is the exact sort of situation that UndecidableInstancesallows. If we turn that extension off and turn FlexibleContexts on(a harmless extension that is just syntactic in nature), we get awarning about a violation of one of the Patersonconditions:

...
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’

"No smaller than instance head," although we can mentally rewrite itas "it is possible this instance will be used to prove an assertion ofitself and cause you much anguish and gnashing and typing." ThePaterson conditions together prevent looping in instance resolution.Our violation here demonstrates why they are necessary, and we canpresumably consult some paper to see why they are sufficient.

Bottoming out

As for why the program at runtime infinite loops: There is the boringanswer, where evil :: a -> b cannot but infinite loop or throw anexception or generally bottom out because we trust the Haskelltypechecker and there is no value that can inhabit a -> b exceptbottom.

A more interesting answer is that, since Convert X X istautologically true, its instance definition is this infinite loop

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

We can similarly expand out the Convert A B instance definition.

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

This surprising behavior, and how constrained instance resolution (bydefault without extensions) is meant to be as to avoid thesebehaviors, perhaps can be taken as a good reason for why Haskell'stypeclass system has yet to pick up wide adoption. Despite itsimpressive popularity and power, there are odd corners to it (whetherit is in documentation or error messages or syntax or maybe even inits underlying logic) that seem particularly ill fit to how we humansthink about type-level abstractions.

这篇关于为什么这段代码使用UndecidableInstances进行编译，然后生成一个运行时无限循环？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！