时间戳

首页 > 解决方案 > 此 OCaml 表达式在未定义为 AFAIK 时具有其参数的类型，为什么此其他表达式具有 '_a 而不是 'a？

ocaml - 此 OCaml 表达式在未定义为 AFAIK 时具有其参数的类型，为什么此其他表达式具有 '_a 而不是 'a？

问题描述

我明白了

let apply f x = f x

有类型

('a -> 'b) -> 'a -> 'b

apply是一个函数，它接受一个函数f和一个参数x并返回f应用于x. 因此，如果f xhas type'b和xhas type 'a，则f必须有 type 'a -> 'b，因此您将它们组合起来得到('a -> 'b) -> 'a -> 'b。我明白了。通过扩展，let identity f = f具有类型'a -> 'a，因为它接受一个类型的项目'a'并返回相同的类型项目'a，所以它是类型'a -> 'a。我明白了。

let bf b f = if (f b) then f else (fun x -> b)

是类型

bool -> (bool -> bool) -> bool -> bool

f b必须是 type bool，因此fis'a -> bool并且bhas type 'a。f, of type与which is'a -> bool具有相同的类型。所以, , so取, 那么 的类型是, 并返回, 最终的类型是fun x -> b'c -> 'a'c = 'a = boolbfboolfbool -> boolbool -> bool

bool -> (bool -> bool) -> bool -> bool

我必须找到类型

let t1 = apply bf

与 相同的类型apply bf。

所以，apply f是'a -> 'aif fhas type 'a，所以我希望apply bf有type(bf) -> type(bf)

bool -> (bool -> bool) -> bool -> bool -> bool -> (bool -> bool) -> bool -> bool

显然apply bf是类型bool -> (bool -> bool) -> bool -> bool，我不明白为什么会这样。

我也不明白'a类型和'_a类型之间的区别。

如果let apply f x = f x, 那么apply有 类型('a -> 'b) -> 'a -> 'b, 并且let app2 = apply apply有 类型

('_a -> '_b) -> '_a -> '_b

如果有人可以帮助我理解为什么会这样，这样我就不会在不理解的情况下简单地提交答案而感到迷失，那将不胜感激。

标签： ocamltype-inference

解决方案

我希望 apply bf 有 type(bf) -> type(bf)

这是错误的。首先请注意，应用程序的打字规则是，

f   : A -> B
x   : A
-------------
f x : B

在您的情况下，存在多态性，但想法是相同的，

apply    : ('a -> 'b) -> ('a -> 'b)
bf       :   A -> B
------------------------------------
apply    : (A -> B) -> (A -> B)
bf       :  A -> B
------------------------------------
apply bf :  A -> B

我也不明白 'a 类型和 '_a 类型之间的区别。

该符号'_a表示一个虚拟类型，并且是“值限制”的结果，它指出只有值表达式可以是多态的。见http://mlton.org/ValueRestriction

推荐阅读