我刚刚在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>
我还注意到,当替换type a. a term -> 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
?
它是否特定于 GADT?