我刚刚在
OCaml’s documentation about 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时.术语 – > a by’a term – > ‘或者只是删除签名,该函数不再编译.
...
| 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
那么这个符号是什么?是什么让它变得与众不同?
它是否特定于GADT?
最佳答案 该手册解释了几个部分的语法:
http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc80
简而言之,输入a. …意味着本地抽象类型a必须是多态的.