在来自ocaml manual的§7.20 的 GADT 基本示例中,“类型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)
最佳答案
雅克的 slide on ML'2011 workshop 有一个很好的介绍。使用局部抽象类型语法引入通用表达式范围变量的想法。
关于ocaml GADT : why "type a." needed?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/33314788/