来自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中没有子类型关系,对吧?那么为什么这样呢?
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类型不相交,但是 多态类型 可能重叠。
@ 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
,但具有这种专门的身份功能使编译器明白你 期望 使用它来将函数应用于参数,因此如果你犯了错误,它可以提前纾困并给你一个更具描述性的错误信息。