ocaml - 在 OCaml 中使用 GADT 的简单 lambda 演算 DSL

Question

如何使用 GADT 在 OCaml 中定义简单的类似 lambda 演算的 DSL？具体来说，我无法弄清楚如何正确定义类型检查器以将非类型化 AST 转换为类型化 AST，也无法找出上下文和环境的正确类型。

这里有一些使用 OCaml 中传统方法的简单 lambda 演算语言的代码

(* Here's a traditional implementation of a lambda calculus like language *)

type typ =
| Boolean
| Integer
| Arrow of typ*typ

type exp =
| Add of exp*exp
| And of exp*exp
| App of exp*exp
| Lam of string*typ*exp
| Var of string
| Int of int
| Bol of bool

let e1=Add(Int 1,Add(Int 2,Int 3))
let e2=Add(Int 1,Add(Int 2,Bol false)) (* Type error *)
let e3=App(Lam("x",Integer,Add(Var "x",Var "x")),Int 4)

let rec typecheck con e =
    match e with
    | Add(e1,e2) ->
        let t1=typecheck con e1 in
        let t2=typecheck con e2 in
        begin match (t1,t2) with 
        | (Integer,Integer) -> Integer
        | _ -> failwith "Tried to add with something other than Integers"
        end
    | And(e1,e2) ->
        let t1=typecheck con e1 in
        let t2=typecheck con e2 in
        begin match (t1,t2) with 
        | (Boolean,Boolean) -> Boolean 
        | _ -> failwith "Tried to and with something other than Booleans"
        end
    | App(e1,e2) ->
        let t1=typecheck con e1 in
        let t2=typecheck con e2 in
        begin match t1 with 
        | Arrow(t11,t12) ->
            if t11 <> t2 then
                failwith "Mismatch of types on a function application"
            else
                t12
        | _ -> failwith "Tried to apply a non-arrow type" 
        end
    | Lam(x,t,e) ->
        Arrow (t,typecheck ((x,t)::con) e)
    | Var x  ->
        let (y,t) = List.find (fun (y,t)->y=x) con in
        t
    | Int _ -> Integer
    | Bol _ -> Boolean

let t1 = typecheck [] e1
(* let t2 = typecheck [] e2 *)
let t3 = typecheck [] e3

type value = 
| VBoolean of bool
| VInteger of int
| VArrow of ((string*value) list -> value -> value)

let rec eval env e = 
    match e with
    | Add(e1,e2) ->
        let v1=eval env e1 in
        let v2=eval env e2 in
        begin match (v1,v2) with 
        | (VInteger i1,VInteger i2) -> VInteger (i1+i2) 
        | _ -> failwith "Tried to add with something other than Integers"
        end
    | And(e1,e2) ->
        let v1=eval env e1 in
        let v2=eval env e2 in
        begin match (v1,v2) with 
        | (VBoolean b1,VBoolean b2) -> VBoolean (b1 && b2) 
        | _ -> failwith "Tried to and with something other than Booleans"
        end
    | App(e1,e2) ->
        let v1=eval env e1 in
        let v2=eval env e2 in
        begin match v1 with 
        | VArrow a1 -> a1  env v2 
        | _ -> failwith "Tried to apply a non-arrow type" 
        end
    | Lam(x,t,e) ->
        VArrow (fun env' v' -> eval ((x,v')::env') e) 
    | Var x  ->
        let (y,v) = List.find (fun (y,t)->y=x) env in
        v 
    | Int i -> VInteger i 
    | Bol b -> VBoolean b

let v1 = eval [] e1
let v3 = eval [] e3

现在，我正在尝试将其转换为使用 GADT 的内容。这是我的开始

(* Now, we try to GADT the process *) 

type exp =
| Add of exp*exp
| And of exp*exp
| App of exp*exp
| Lam of string*typ*exp
| Var of string
| Int of int
| Bol of bool

let e1=Add(Int 1,Add(Int 2,Int 3))
let e2=Add(Int 1,Add(Int 2,Bol false))
let e3=App(Lam("x",Integer,Add(Var "x",Var "x")),Int 4)

type _ texp =
| TAdd : int texp * int texp -> int texp
| TAnd : bool texp * bool texp -> bool texp
| TApp : ('a -> 'b) texp * 'a texp -> 'b texp
| TLam : string*'b texp -> ('a -> 'b) texp
| TVar : string -> 'a texp
| TInt : int -> int texp
| TBol : bool -> bool texp

let te1 = TAdd(TInt 1,TAdd(TInt 2,TInt 3))

let rec typecheck : type a. exp -> a texp = fun e ->
    match e with
    | Add(e1,e2) ->
        let te1 = typecheck e1 in
        let te2 = typecheck e2 in
        TAdd (te1,te2)
    | _ -> failwith "todo"

问题就在这里。首先，我不确定如何在类型 texp 中定义 TLam 和 TVar 的正确类型。通常，我会提供带有变量名称的类型，但我不确定在这种情况下如何执行此操作。其次，我不知道函数类型检查中上下文的正确类型。之前，我使用了某种列表，但现在我确定了列表的类型。第三，在忽略上下文之后，类型检查函数本身不会进行类型检查。失败并显示消息

File "test03.ml", line 32, characters 8-22:
Error: This expression has type int texp
       but an expression was expected of type a texp
       Type int is not compatible with type a 

这完全有道理。这更多是一个问题，因为我不确定类型检查的正确类型应该是什么。

无论如何，您如何修复这些功能？

<小时/>

编辑 1

这是上下文或环境的可能类型

type _ ctx =
| Empty : unit ctx
| Item :  string * 'a * 'b ctx -> ('a*'b) ctx

<小时/>

编辑2

环境的技巧是确保环境的类型嵌入到表达式的类型中。否则，没有足够的信息来确保类型安全。这是一个完整的解释器。目前，我没有有效的类型检查器来从非类型化表达式转移到类型化表达式。

type (_,_) texp =
| TAdd : ('e,int) texp * ('e,int) texp -> ('e,int) texp
| TAnd : ('e,bool) texp * ('e,bool) texp -> ('e,bool) texp
| TApp : ('e,('a -> 'b)) texp * ('e,'a) texp -> ('e,'b) texp
| TLam : (('a*'e),'b) texp -> ('e,('a -> 'b)) texp
| TVar0 : (('a*'e),'a) texp
| TVarS : ('e,'a) texp -> (('b*'e),'a) texp
| TInt : int -> ('e,int) texp
| TBol : bool -> ('e,bool) texp

let te1 = TAdd(TInt 1,TAdd(TInt 2,TInt 3))
(*let te2 = TAdd(TInt 1,TAdd(TInt 2,TBol false))*)
let te3 = TApp(TLam(TAdd(TVar0,TVar0)),TInt 4)
let te4 = TApp(TApp(TLam(TLam(TAdd(TVar0,TVarS(TVar0)))),TInt 4),TInt 5)
let te5 = TLam(TLam(TVarS(TVar0)))

let rec eval : type e t. e -> (e,t) texp -> t = fun env e -> 
    match e with
    | TAdd (e1,e2) ->
        let v1 = eval env e1 in
        let v2 = eval env e2 in
        v1 + v2
    | TAnd (e1,e2) ->
        let v1 = eval env e1 in
        let v2 = eval env e2 in
        v1 && v2
    | TApp (e1,e2) ->
        let v1 = eval env e1 in
        let v2 = eval env e2 in
        v1 v2
    | TLam e ->
        fun x -> eval (x,env) e 
    | TVar0 ->
        let (v,vs)=env in
        v
    | TVarS e ->
        let (v,vs)=env in
        eval vs e 
    | TInt i -> i
    | TBol b -> b

然后，我们有

# eval () te1;;
- : int = 6
# eval () te3;;
- : int = 8
# eval () te5;;
- : '_a -> '_b -> '_a = <fun>
# eval () te4;;
- : int = 9

Answer 1

如果您希望术语表示强制类型正确，则需要更改类型环境(和变量)的表示方式:您无法精细地键入从字符串到值的映射(表示映射的类型是同类的)。经典的解决方案是使用 De Bruijn indices 转向变量的表示。 (强类型数字)而不是变量名称。它可能会帮助您首先在无类型世界中执行该转换，然后只关心在无类型 -> GADT 传递中的类型。

这是一个粗略的草图，用于强类型变量的 GADT 声明:

type (_, _) var =
  | Z : ('a, 'a * 'g) var
  | S : ('a, 'g) var -> ('a, 'b * 'g) var

('a, 'g) var 类型的值应理解为从环境中提取 'a 类型值的方法的描述类型为'g。环境由一系列右嵌套元组表示。 Z 情况对应于选择环境中的第一个变量，而 S 情况则忽略最上面的变量并在环境中更深入地查找。

Shayan Najd 有一个(Haskell)实现这个想法 on github 。欢迎查看the GADT representation或the type-checking/translating code .