用于表示具有多个参数的函数应用程序 (AST) 的 GADT

Question

我在 OCaml 手册中看到这个示例将 GADT 用于具有函数应用程序的 AST：

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
  | Add      -> (fun x y -> x+y)
  | App(f,x) -> (eval f) (eval x)

对于不支持部分应用的语言，这是表示函数应用的正确方式吗？

有没有办法用任意数量的参数制作 GADT 支持函数应用程序？

最后，GADT 是表示类型化 AST 的好方法吗？还有其他选择吗？

Answer 1

嗯，部分评估已经在这里工作了：

# eval (App(App(Add, Int 3),Int 4)) ;;
- : int = 7   

# eval (App(Add, Int 3)) ;;
- : int -> int = <fun>   

# eval (App(Add, Int 3)) 4 ;;
- : int = 7

这个小 gadt 中没有的是抽象 (lambda)，但绝对可以添加它。

如果您对这个话题感兴趣，这里有丰富的（学术）文献。 This 论文介绍了支持部分评估的各种编码。

也有非Gadt解决方案，如图this paper.

一般来说，GADT 是一种非常有趣的表示评估者的方式。当您尝试为编译转换 AST 时，它们往往会有点短（但有 ways）。

此外，您必须记住，您正在对您在宿主语言中定义的语言的类型系统进行编码，这意味着您需要对您想要的类型特征进行编码。有时候，这很棘手。

编辑：让 GADT not 支持部分求值的一种方法是使用不包含函数的特殊值类型和包含函数的 "functional value" 类型。以第一篇论文的最简单表示，我们可以这样修改它：

type _ v =
  | Int : int -> int v
  | String : string -> string v

and _ vf =
  | Base : 'a v -> ('a v) vf
  | Fun : ('a vf -> 'b vf) -> ('a -> 'b) vf

and _ t =
  | Val : 'a vf -> 'a t
  | Lam : ('a vf -> 'b t) -> ('a -> 'b) t
  | App : ('a -> 'b) t * 'a t -> 'b t

let get_val : type a . a v -> a = function
  | Int i -> i
  | String s -> s

let rec reduce : type a . a t -> a vf = function
  | Val x -> x
  | Lam f -> Fun (fun x -> reduce (f x))
  | App (f, x) -> let Fun f = reduce f in f (reduce x)

let eval t =
  let Base v = reduce t in get_val v

(* Perfectly defined expressions. *)
let f = Lam (fun x -> Lam (fun y -> Val x))
let t = App (f, Val (Base (Int 3)))
(* We can reduce t to a functional value. *)
let x = reduce t
(* But we can't eval it, it's a type error. *)
let y = eval t

(* HOF are authorized. *)
let app = Lam (fun f -> Lam (fun y -> App(Val f, Val y)))

你可以根据自己的需要让它变得更复杂，重要的是属性是 'a v 类型不能产生函数。

用于表示具有多个参数的函数应用程序 (AST) 的 GADT

GADTs for Representing Function Application with Multiple Parameters (AST)

ocaml

abstract-syntax-tree

gadt