为什么在Haskell中不进行这种类型检查？

Question

这不会输入检查：

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这样Right (y::c) :: Either a c。

Answer 1

问题是当你说

defaultEither _ b = b

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

我了解您要尝试执行的操作-但是，即使一个值Right x（带有xtype c）本身可以是Either d c任何类型的d，您的类型签名也会将输入和输出值限制为具有不同ds的版本。这意味着您不能使用相同的变量来引用两个值。

Answer 2

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

data Foo x = Bar

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

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

现在，如果您有表达式Just True，则从此开始True :: Bool，然后Just True :: Maybe True。但是，表达Nothing肯定是Maybe 某种东西。但是，在没有实际价值存在的情况下，没有什么可以强迫它成为任何特定的可能类型。在这种情况下，类型变量是幻影。

我们在这里有类似的事情。Bar :: Foo x，对于任何x。因此，您会认为我们的定义foobar是合法的。

而你会错的。

即使它们具有完全相同的运行时结构，也不能传递期望Foo a类型值的值。因为类型检查器不在乎运行时结构；它只在乎类型。至于类型检查而言，是不同的，即使在运行时没有观察到的差异。Foo bFoo IntFoo Bool

而这就是为什么你的代码将被拒绝。

其实你要写

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

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

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

正如您所发现的，解决方案是从您的价值中b提取价值Right，然后立即将其重新投入。看起来毫无意义而且很愚蠢，但是它是要明确通知类型检查器类型可能已更改。这也许很烦人，但这只是该语言的那些角落之一。这不是错误，它是专门设计用于这种方式的。