28

在使用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。
  • 不知何故，该定义能够匹配任何输入和输出类型，因此似乎调用 toconvertFoo :: a -> Foo正在选择convertFoo自身的定义，因为无论如何它是唯一可用的定义。
  • 由于convertFoo无限调用自身，函数进入一个永不终止的无限循环。
  • 由于convertFoo永不终止，该定义的类型是底部，所以从技术上讲，没有任何类型被违反，并且程序类型检查。

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

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

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

4

2 回答 2

22

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

类型类惊喜

要查看这里发生了什么，将提高类型签名的赌注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除了底部没有任何值可以容纳。

一个更有趣的答案是，既然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 的类型类系统尚未得到广泛采用的一个很好的理由。尽管它令人印象深刻的受欢迎程度和强大的功能，但它有一些奇怪的角落（无论是在文档、错误消息或语法中，甚至可能在其底层逻辑中）似乎特别不适合我们人类对类型级抽象的看法。

于 2016-05-24T05:16:47.433 回答
7

以下是我在心理上处理这些案例的方式：

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

evil :: Int -> String
evil = convertFoo

首先，我们从计算所需实例集开始。

  • evil直接要求ConvertFoo Int String（1）。
  • 那么，（1）需要ConvertFoo Int Foo（2）和ConvertFoo Foo String（3）。
  • 然后，（2）需要ConvertFoo Int Foo（我们已经计算过了）和ConvertFoo Foo Foo（4）。
  • 那么 (3) 需要ConvertFoo Foo Foo(counted) 和ConvertFoo Foo String(counted)。
  • 那么（4）需要ConvertFoo Foo Foo（counted）和ConvertFoo Foo Foo（counted）。

因此，我们到达了一个固定点，它是所需实例的有限集合。编译器在有限时间内计算集合没有问题：只需应用实例定义，直到不再需要约束。

然后，我们继续为这些实例提供代码。这里是。

convertFoo_1 :: Int -> String
convertFoo_1 = convertFoo_3 . convertFoo_2
convertFoo_2 :: Int -> Foo
convertFoo_2 = convertFoo_4 . convertFoo_2
convertFoo_3 :: Foo -> String
convertFoo_3 = convertFoo_3 . convertFoo_4
convertFoo_4 :: Foo -> Foo
convertFoo_4 = convertFoo_4 . convertFoo_4

我们得到一堆相互递归的实例定义。在这种情况下，这些将在运行时循环，但没有理由在编译时拒绝它们。

于 2016-05-24T08:28:18.330 回答