logo标签列表

OCaml的 `type a. a t` 语法

syntaxocamlgadtlocally-abstract-type
6

我刚刚在OCaml关于GADTs的文档中发现了以下代码片段：

let rec eval : type a. a term -> a = function
  | Int n -> n
  | Add -> (fun x y -> x + y)
  | App (f, x) -> (eval f) (eval x)

在utop中评估后，其签名如下：
val eval : 'a term -> 'a = <fun>

我还注意到，当用'a term -> 'a替换type a. a term -> a或仅删除签名时，该函数将无法编译。
...
| Add -> (fun x y -> x + y)
...
Error: This pattern matches values of type (int -> int -> int) term
  but a pattern was expected which matches values of type int term
  Type int -> int -> int is not compatible with type int

那么这个符号是什么？它与'a t有何不同之处？

它是否专门针对GADTs？

1个回答
3
不，它不是多态的。这就是'a . 的用法（参见手册中的7.12节）。类型系统不会将let f (x:'a) : 'a = x + 1视为错误，因为int可以统一。而type a创建了一个局部抽象类型。在GADTs中，每个分支都可以实例化为不同的类型，例如示例Antoine中的a。在希望在多态函数中使用具体类型的情况下，这允许引用该类型。 - nlucaroni
9
type a. ... 这个语法要求 a 是可以多态的。它由 'a. ...（用于强制多态性）和 (type a)（声明一个局部抽象类型）组合而成。 - Leo White
更新链接：https://ocaml.org/manual/locallyabstract.html，解释了(type a)以及type a.的展开方式。而'a语法则在https://ocamlverse.github.io/content/weak_type_variables.html中有详细说明。 - Max Heiber
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接