在OCaml手册的§7.20的GADT基本示例中,“type a.”的含义是什么?
为什么声明“eval:a term -> a”还不够?
type _ term =
| Int : int -> int term
| Add : (int -> int -> int) term
| App : ('b -> 'a) term * 'b term -> 'a term
let rec eval : type a. a term -> a = function
| Int n -> n (* a = int *)
| Add -> (fun x y -> x+y) (* a = int -> int -> int *)
| App(f,x) -> (eval f) (eval x)
eval
函数需要多态递归,并且type a. ...
的存在部分是为了打开对其的支持信号。如果省略type
,则会出现尝试在不允许使用多态递归时使用它所期望的错误。 - Jeffrey Scofield