为什么两个具有不同类型 var 的多态高阶函数在类型上是等价的？

Question

来自 Javascript 我了解 Haskell 的列表类型强制执行同质列表。现在让我感到惊讶的是，以下不同的函数类型满足了这个要求：

f :: (a -> a) -> a -> a 
f g x = g x

g :: (a -> b) -> a -> b 
g h x = h x

let xs = [f, g] -- type checks

尽管g 比f 更适用：

f(\x -> [x]) "foo" -- type error
g(\x -> [x]) "foo" -- type checks

不应将(a -> a) 与(a -> b) 区别对待。在我看来，后者似乎是前者的子类型。但是 Haskell 中没有子类型关系，对吧？那么为什么会这样呢？

Answer 1

Haskell 是静态类型的，但这并不意味着它是 Fortran。每种类型都必须在编译时得到固定，但不一定在单个定义中。 f 和 g 的类型都是 polymorphic。解释这一点的一种方法是f 不仅仅是一个函数，而是整个重载函数家族。喜欢（在 C++ 中）

int f (function<int(int)> g, int x) { return g(x); }
char f (function<char(char)> g, char x) { return g(x); }
double f (function<double(double)> g, double x) { return g(x); }
...

当然，实际生成所有这些函数是不切实际的，所以在 C++ 中，你可以将其写成一个模板

template <typename T>
T f (function<T(T)> g, T x) { return g(x); }

...意思是，每当编译器找到f，如果你的项目的代码，它会找出T在特定情况下是什么，然后创建一个具体的模板实例化（a固定到那个具体类型的单态函数，就像我上面写的例子一样）并且只在运行时使用那个具体的实例化。

这两个模板函数的具体实例可能具有相同的类型，即使模板看起来有点不同。

现在，Haskell 的参数多态性与 C++ 模板有一点不同，但至少在您的示例中它们是相同的：g 是一个完整的函数家族，包括实例化 g :: (Int -> Char) -> Int -> Char（不是兼容f)的类型，也兼容g :: (Int -> Int) -> Int -> Int，也就是。当您将f 和g 放在一个列表中时，编译器会自动意识到只有与f 类型兼容的g 的子族与此处相关。

是的，这确实是一种子类型。当我们说“Haskell 没有子类型”时，我们的意思是任何 具体（Rank-0）类型与所有其他 Rank-0 类型不相交，但 多态类型可能重叠。

Answer 2

@leftroundabout 的回答很可靠；这是一个更具技术性的补充答案。

有一种在 Haskell 中起作用的子类型关系：System F“通用实例”关系。这是编译器在检查函数的推断类型与签名时使用的。基本上，一个函数的推断类型必须至少和它的签名一样多态：

f :: (a -> a) -> a -> a
f g x = g x

这里f的推断类型是forall a b. (a -> b) -> a -> b，和你给的g的定义一样。但签名更具限制性：它添加约束a ~ b（a 等于b）。

Haskell 首先用 Skolem 类型变量替换签名中的类型变量来检查这一点——这些是新的唯一类型常量，它们只与它们自己（或类型变量）统一。我将使用符号 $a 来表示 Skolem 常数。

forall a. (a -> a) -> a -> a
($a -> $a) -> $a -> $a

当您不小心有一个“超出其范围”的类型变量时，您可能会看到对“刚性、Skolem”类型变量的引用：它在引入它的 forall 量词之外使用。

接下来，编译器进行包含检查。这与正常的类型统一基本相同，其中a -> b ~ Int -> Char 给出a ~ Int 和b ~ Char；但因为它是一种子类型关系，它也解释了函数类型的协变和逆变。如果(a -> b) 是(c -> d) 的子类型，那么b 必须是d 的子类型（协变），但a 必须是c（逆变）的超类型 .

{-1-}(a -> b) -> {-2-}(a -> b)  <:  {-3-}($a -> $a) -> {-4-}($a -> $a)

{-3-}($a -> $a) <: {-1-}(a -> b)  -- contravariant (argument)
{-2-}(a -> b) <: {-4-}($a -> $a)  -- covariant (result)

编译器生成以下约束：

$a <: a  -- contravariant
b <: $a  -- covariant
a <: $a  -- contravariant
$a <: b  -- covariant

并通过统一来解决它们：

a ~ $a
b ~ $a
a ~ $a
b ~ $a

a ~ b

所以推断的类型(a -> b) -> a -> b至少和签名(a -> a) -> a -> a一样多态。

---

当你写xs = [f, g]时，正常的统一开始了：你有两个签名：

forall a.   (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b

这些是实例化的新类型变量：

(a1 -> a1) -> a1 -> a1
(a2 -> b2) -> a2 -> b2

然后统一：

(a1 -> a1) -> a1 -> a1  ~  (a2 -> b2) -> a2 -> b2
a1 -> a1  ~  a2 -> b2
a1 -> a1  ~  a2 -> b2
a1 ~ a2
a1 ~ b2

最终解决并概括：

forall a1. (a1 -> a1) -> a1 -> a1

因此g 的类型已变得不那么通用，因为它被限制为与f 具有相同的类型。因此，xs 的推断类型将是 [(a -> a) -> a -> a]，因此编写 [f (\x -> [x]) "foo" | f <- xs] 会得到与编写 f (\x -> [x]) "foo" 相同的类型错误；尽管g 更笼统，但您已经隐藏了一些通用性。

---

现在您可能想知道为什么您会为函数提供比必要的更严格的签名。答案是——引导类型推断并产生更好的错误消息。

例如($)的类型是(a -> b) -> a -> b；但实际上这是id :: c -> c 的限制性更强的版本！只需设置c ~ a -> b。所以事实上你可以写foo `id` (bar `id` baz quux)而不是foo $ bar $ baz quux，但是拥有这个专门的标识函数让编译器清楚地知道你期望使用它来将函数应用于参数，所以它可以保释如果您犯了错误，请提前发布并给您一个更具描述性的错误消息。