为什么不在 Haskell 中进行类型检查？答案

【问题标题】：Why doesn't this type-check in Haskell?为什么不在 Haskell 中进行类型检查？
【发布时间】：2019-09-24 17:53:29
【问题描述】：

这不是类型检查：

module DoesntTypeCheck where {
import Prelude(Either(..));
defaultEither :: a -> Either b c -> Either a c;
defaultEither a (Left _) = Left a;
defaultEither _ b = b;
}

但这确实：

module DoesTypeCheck where {
import Prelude(Either(..));
defaultEither :: a -> Either b c -> Either a c;
defaultEither a (Left _) = Left a;
defaultEither _ (Right b) = Right b;
}

编译器可能有问题，Either a c 类型只能是Left (x::a) 或Right (y::c)，如果不是Left，那么它就是Right，我们知道Right :: b -> Either a b 所以@987654330 @。

【问题讨论】：

“编译器可能有问题”。绝对是每个试图编译他们的第一个 Haskell 程序的人的第一句话。真正的原因绝不是编译器错误。
您也可以使用来自Data.Bifunctor 的first 编写defaultEither = first . const。不过，我可能会称它为setLeft，因为Left 并没有什么特别的默认。
@n.m.无论如何，对于初学者程序来说，它从来都不是编译器错误。有时肯定是在您尝试做更深奥的事情时。
虽然编译器有错误，但我的经验是，一旦你开始责怪编译器，它（接近）肯定不是。简而言之，Either Int Int 类型的 Right x 不是 Either String Int 的 Right x。

标签： haskell types polymorphism

【解决方案1】：

让我们尝试一个更简单的例子：

data Foo x = Bar

foobar :: Foo a -> Foo b
foobar f = f

看一下Foo的定义。左侧有一个类型变量 (x)，它实际上从未出现在右侧的任何位置。这是所谓的“幻像类型变量”的一个例子。类型签名中有一个类型实际上并不对应于实际值中任何内容的类型。（顺便说一句，这是完全合法的。）

现在如果你有表达式Just True，那么因为True :: Bool，然后是Just True :: Maybe True。但是，表达式Nothing 绝对是Maybe something。但是由于没有实际价值，没有什么可以强迫它成为任何特定的可能类型。在这种情况下，类型变量是幻像。

我们这里也有类似的东西； Bar :: Foo x，适用于任何 x。所以你会认为我们对foobar的定义是合法的。

你会错。

您不能传递Foo a 的值，而需要Foo b 类型的值，即使它们具有完全相同的运行时结构。因为类型检查器不关心运行时结构；它只关心类型。就类型检查器而言，Foo Int 与 Foo Bool 不同，即使在运行时没有可观察到的差异。

那就是你的代码被拒绝的原因。

其实你要写

foobar :: Foo a -> Foo b
foobar Bar = Bar

让类型检查器知道您输出的Bar 是一个新的，不同 Bar，而不是您作为输入收到的Bar（因此它可以有不同的类型） .

信不信由你，这实际上是一个功能，而不是一个错误。您可以编写代码，以便（例如）Foo Int 的行为与Foo Char 不同。即使在运行时它们都只是Bar。

正如您所发现的，解决方案是从Right 中取出您的值b，然后立即将其重新放入。这似乎毫无意义和愚蠢，但它是明确地向类型检查器发出类型可能已更改的信号。这可能很烦人，但这只是语言的这些角落之一。这不是错误，它是故意设计成这样工作的。

【讨论】：

【解决方案2】：

问题是当你说

defaultEither _ b = b

您是说输出值b 与第二个输入值相同。这只有在值具有相同类型时才有可能。但是你告诉编译器输入的类型是Either b c，而输出的类型是Either a c。这些是不同的类型，难怪编译器会抱怨。

我理解你想要做什么 - 但即使值 Right x（x 类型为 c）本身可以是任何 Either d c 类型的 d，你的类型签名将输入和输出值限制为具有不同ds 的版本。这意味着您不能使用同一个变量来引用这两个值。

【讨论】：

我并不是说输出与第二个输入具有相同的类型。我只说输出与第二个输入相同。仅仅因为它们是不同的类型并不意味着它们不相交！ Either a c 和 Either b c 的交集正是 Right (y::c) 形式的值
但是没有类型的“交集”这样的东西。值Right (y::c) 的类型为Either a c，您也可以将其称为Either b c，因为类型变量的名称是任意的。但是当您在类型签名中同时使用Either a c 和Either b c 时，编译器必须假定它们是不同的类型。似乎您希望 GHC 的类型推断能够查看 Either 的实现，并看到在您的定义中 b 必须是一个也类型为 Either b c 的值.而且我认为期望它能够做到这一点是不合理的。
@ThePiercingPrince “仅仅因为它们是不同的类型并不意味着它们不相交！”这在 Haskell 中确实是这个意思。 Haskell 的类型系统是名义上的（就像编程语言中使用的几乎所有其他静态类型系统一样） - 即，如果两种类型具有不同的名称，它们（和它们的值！）是完全不同的。当然，可以提取正确的值并将其作为不同类型的另一个正确值注入，但这不会自动发生。

【解决方案3】：

Either ac 类型只能是 Left (x::a) 或 Right (y::c)，如果不是 Left，那么它就是 Right，我们知道 Right :: b -> Either ab 所以对 (y::c) :: 要么是 c。

我认为您将type 构造函数与data 构造函数混淆了。 Either 在 ghc-base 中是这样定义的：

data  Either a b  =  Left a | Right b

Either 是一个带有两个抽象变量的type 构造函数。即它需要任何两种类型（Int、String 等）。并构造一个具体类型，如Either Int String。

另一方面，Left 和 Right 是 data 构造函数。它们采用1、"hi" 等实际值并构造Left 1 和Right "hi" 等值。

Prelude> :t Left
Left :: a -> Either a b
Prelude> :t Right
Right :: b -> Either a b

Haskell 类型推断不适用于values（Left 和Right）。它仅适用于types (Either)。所以类型检查器只知道Either b c 和Either a c - 所以在第一种情况下变量不匹配。

【讨论】：

【解决方案4】：

Either a c 类型只能是...

确实，但在您的第一个示例中，值 b 没有类型 Either a c！正如您的类型签名所证明的那样，它的类型为Either b c。当然，你不能返回一个 Either b c ，而应该是 Either a c 。相反，您必须解构该值并使用正确的类型重新构造它。

【讨论】：