使用 OCaml GADT 编写解释器

Question

我正在用 OCaml 编写一个小型解释器，并使用 GADT 来输入我的表达式：

type _ value =
    | Bool : bool -> bool value
    | Int : int -> int value
    | Symbol : string -> string value
    | Nil : unit value
    | Pair : 'a value * 'b value -> ('a * 'b) value
and _ exp =
    | Literal : 'a value -> 'a exp
    | Var : name -> 'a exp
    | If : bool exp * 'a exp * 'a exp -> 'a exp
and name = string

exception NotFound of string

type 'a env = (name * 'a) list
let bind (n, v, e) = (n, v)::e
let rec lookup = function
    | (n, []) -> raise (NotFound n)
    | (n, (n', v)::e') -> if n=n' then v else lookup (n, e')

let rec eval : type a. a exp -> a value env -> a value = fun e rho ->
    match e with
    | Literal v -> v
    | Var n -> lookup (n, rho)
    | If (b, l, r) ->
            let Bool b' = eval b rho in
            if b' then eval l rho else eval r rho

但是我无法编译我的代码。我收到以下错误：

File "gadt2.ml", line 33, characters 33-36:
Error: This expression has type a value env = (name * a value) list
       but an expression was expected of type
         bool value env = (name * bool value) list
       Type a is not compatible with type bool

我的理解是由于某种原因 rho 被强制转换为 bool value env，但我不知道为什么。我还尝试了以下方法：

let rec eval : 'a. 'a exp -> 'a value env -> 'a value = fun e rho ->
    match e with
    | Literal v -> v
    | Var n -> lookup (n, rho)
    | If (b, l, r) ->
            let Bool b = eval b rho in
            if b then eval l rho else eval r rho

但我不确定这到底有何不同，它也给了我一个错误——尽管是一个不同的错误：

File "gadt2.ml", line 38, characters 56-247:
Error: This definition has type bool exp -> bool value env -> bool value
       which is less general than 'a. 'a exp -> 'a value env -> 'a value

关于 GADT 的指导、两个 eval 之间的差异以及这个特殊问题都值得赞赏。干杯。

Answer 1

类型 'a env 旨在表示 name/value 绑定的列表，但列表中的值必须都是同一类型。两个不同的值类型（如bool value和int value）不是同一类型。如果eval b rhoreturnsBool b，rho一定是string * bool value的列表。所以 eval l rho 和 eval r rho 将 return bool value。但是你的注释说函数 returns a value.

Answer 2

有几种可能的方法可以使用 GADT 进行类型化绑定。这是将类型信息与变量和环境条目相关联的设计。

环境查找涉及尝试构建变量类型和环境条目之间的对应关系（这有点慢，但确实以安全的方式恢复了类型）。这就是允许查找 return 任意类型的未包装值的原因。

type var = string

type _ ty =
  | TyInt : int ty
  | TyArrow : 'a ty * 'b ty -> ('a -> 'b) ty

type _ term =
  | Int : int -> int term
  | Var : 'a ty * var -> 'a term
  | Lam : 'a ty * var * 'b term -> ('a -> 'b) term
  | App : ('a -> 'b) term * 'a term -> 'b term

type ('a, 'b) eq = Refl : ('a, 'a) eq

let rec types_equal : type a b . a ty -> b ty -> (a, b) eq option =
  fun a b ->
    match a, b with
    | TyInt, TyInt -> Some Refl
    | TyArrow (x1, y1), TyArrow (x2, y2) ->
      begin match types_equal x1 x2, types_equal y1 y2 with
        | Some Refl, Some Refl -> Some Refl
        | _, _ -> None
      end
    | _, _ -> None

type env = Nil | Cons : var * 'a ty * 'a * env -> env

let rec lookup : type a . a ty -> var -> env -> a =
  fun ty var -> function
    | Nil -> raise Not_found
    | Cons (xname, xty, x, rest) ->
      if var = xname then
        match types_equal ty xty with
        | Some Refl -> x
        | None -> assert false
      else
        lookup ty var rest

let rec eval : type a . env -> a term -> a =
  fun env -> function
    | Int n -> n
    | Var (ty, var) -> lookup ty var env
    | App (f, x) -> (eval env f) (eval env x)
    | Lam (arg_ty, arg_name, body) ->
      fun arg_value ->
        eval (Cons (arg_name, arg_ty, arg_value, env)) body

通过在类型级别强制变量索引和环境之间的对应关系，可以有一个避免类型重构（和字符串比较！）的类型化解释器，但这会变得复杂。

使用 OCaml GADT 编写解释器

Writing an interpreter with OCaml GADTs

ocaml

interpreter

type-systems

gadt