问题 为什么两个具有不同类型变量的多态高阶函数的类型相同?


来自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中没有子类型关系,对吧?那么为什么这样呢?


3559
2017-10-27 11:07


起源

Haskell的类型推理算法说:“我可以提出一种替换方法,使这两种类型相同吗?”的类型 f 和 g 统一,在替代下 b ~ a,在类型 (a -> a) -> a -> a。所以 xs :: [(a -> a) -> a -> a]。 - Benjamin Hodgson♦
@Benjamin好的,它传递了类型检查,因为缺少Haskell的类型推断可以使用的代码。对于给定的代码,断言这两种类型可能是等价的就足够了。 - ftor
我认为Haskell在这个例子中并不严格,以便最大限度地减少超出其类型系统表现力的程序数量。一世。即程序不编译,但仍然有意义。 - ftor


答案:


Haskell是静态类型的,但这并不意味着它是Fortran。每种类型都必须得到修复 在编译时,但不一定在单一定义内。两者的类型 f 和 g 是 多态。解释这一点的一种方法是 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 在具体情况下,然后创建一个具体的 模板实例化 (一个单态函数固定到那个具体类型,就像我上面写的那个例子)并且只在运行时使用那个具体的实例化。

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

现在,Haskell的参数多态性与C ++模板的解析略有不同,但至少在您的示例中它们相同: g 是一整套功能,包括实例化 g :: (Int -> Char) -> Int -> Char (与...的类型不兼容 f) 但也 g :: (Int -> Int) -> Int -> Int,是的。当你放 f 和 g 在单个列表中,编译器自动实现只有子系列的 g 其类型兼容 f 在这里是相关的。

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


13
2017-10-27 11:45



因此,当这两种类型仅添加到列表中时,类型检查器就足够了 f和 g多态类型有一些共同点。但是只要我映射出类型的纯函数 (a -> b) 在此列表中,类型推断将检测类型错误。 Haskell的类型推断权衡了每一个案例,并且只是根据需要进行限制。那又是辉煌的。 - ftor


@ 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 代表斯科伦常数。

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

当您意外地拥有一个“逃避其范围”的类型变量时,您可能会看到对“rigid,Skolem”类型变量的引用:它在外部使用 forall 介绍它的量词。

接下来,编译器执行a 包含检查。这与类型的正常统一基本相同,其中 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,但具有这种专门的身份功能使编译器明白你 期望 使用它来将函数应用于参数,因此如果你犯了错误,它可以提前纾困并给你一个更具描述性的错误信息。


2
2017-10-27 22:30



对于更高等级的类型,合作/逆转只是真正发挥作用吗?没有 RankNTypes, 一切 foralls在外面,类约束总是“逆变”。但也许我错了...... - dfeuer
@dfeuer:是的,我认为这是逆变的唯一重要时刻。使用§3.3中的示例 这张纸给定 f ∷ ((∀a. [a] → [a]) → Int) → Int, g ∷ (∀a. a → a) → Int,和 h ∷ ([Int] → [Int]) → Int, ∀a. a → a 是 更多 多态的 ∀a. [a] → [a],因此 (∀a. a → a) → Int 是 减 多变的 (∀a. [a] → [a]) → Int, 这就是为什么 f g 是一个类型错误,但 f h 很好。 - Jon Purdy
感谢您对机械的深入了解。我将仔细研究包含过程和类型常量。 - ftor
如果我正确理解您的答案,则只要提供显式的用户定义类型注释,就会将类型变量替换为新的skolem类型变量,以便将它们与编程推断的类型变量区分开来。包含是统一的,它考虑了“更多态”的关系,它描述了一种子类型。它是否正确? - ftor
@ftor:是的,这是对的。我的答案的第一部分描述了为什么你可以使用较不通用的类型签名;第二部分描述了为什么可以将不同(但兼容)类型的多个函数放在同类列表中。 - Jon Purdy