你如何使用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
这完全有道理。这更像是一个问题，我不确定typecheck的正确类型应该是什么。
无论如何，你如何修复这些功能？
这是上下文或环境的可能类型
type _ ctx =
| Empty : unit ctx
| Item : string * 'a * 'b ctx -> ('a*'b) ctx
环境的诀窍是确保环境的类型嵌入到表达式的类型中。否则，没有足够的信息来使事情类型安全。这是一个完整的翻译。目前，我没有有效的类型检查器来从无类型表达式转换为类型化表达式。
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
如果您希望术语表示强制执行良好类型，则需要更改表示类型环境（和变量）的方式：您不能精确地键入从字符串到值的映射（表示映射的类型是同类的）。经典的解决方案是使用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。
好吧，所以我终于解决了问题。因为我可能不是唯一发现这个有趣的人，所以这里有一套完整的代码，可以进行类型检查和评估：
type (_,_) texp =
| TAdd : ('gamma,int) texp * ('gamma,int) texp -> ('gamma,int) texp
| TAnd : ('gamma,bool) texp * ('gamma,bool) texp -> ('gamma,bool) texp
| TApp : ('gamma,('t1 -> 't2)) texp * ('gamma,'t1) texp -> ('gamma,'t2) texp
| TLam : (('gamma*'t1),'t2) texp -> ('gamma,('t1 -> 't2)) texp
| TVar0 : (('gamma*'t),'t) texp
| TVarS : ('gamma,'t1) texp -> (('gamma*'t2),'t1) texp
| TInt : int -> ('gamma,int) texp
| TBol : bool -> ('gamma,bool) texp
type _ typ =
| Integer : int typ
| Boolean : bool typ
| Arrow : 'a typ * 'b typ -> ('a -> 'b) typ
type (_,_) iseq = IsEqual : ('a,'a) iseq
let rec is_equal : type a b. a typ -> b typ -> (a,b) iseq option = fun a b ->
match a, b with
| Integer, Integer -> Some IsEqual
| Boolean, Boolean -> Some IsEqual
| Arrow(t1,t2), Arrow(u1,u2) ->
begin match is_equal t1 u1, is_equal t2 u2 with
| Some IsEqual, Some IsEqual -> Some IsEqual
| _ -> None
end
| _ -> None
type _ isint = IsInt : int isint
let is_integer : type a. a typ -> a isint option = fun a ->
match a with
| Integer -> Some IsInt
| _ -> None
type _ isbool = IsBool : bool isbool
let is_boolean : type a. a typ -> a isbool option = fun a ->
match a with
| Boolean -> Some IsBool
| _ -> None
type _ context =
| CEmpty : unit context
| CVar : 'a context * 't typ -> ('a*'t) context
type exp =
| Add of exp*exp
| And of exp*exp
| App of exp*exp
| Lam : 'a typ * exp -> exp
| Var0
| VarS of exp
| Int of int
| Bol of bool
type _ exists_texp =
| Exists : ('gamma,'t) texp * 't typ -> 'gamma exists_texp
let rec typecheck
: type gamma t. gamma context -> exp -> gamma exists_texp =
fun ctx e ->
match e with
| Int i -> Exists ((TInt i) , Integer)
| Bol b -> Exists ((TBol b) , Boolean)
| Var0 ->
begin match ctx with
| CEmpty -> failwith "Tried to grab a nonexistent variable"
| CVar(ctx,t) -> Exists (TVar0 , t)
end
| VarS e ->
begin match ctx with
| CEmpty -> failwith "Tried to grab a nonexistent variable"
| CVar(ctx,_) ->
let tet = typecheck ctx e in
begin match tet with
| Exists (te,t) -> Exists ((TVarS te) , t)
end
end
| Lam(t1,e) ->
let tet2 = typecheck (CVar (ctx,t1)) e in
begin match tet2 with
| Exists (te,t2) -> Exists ((TLam te) , (Arrow(t1,t2)))
end
| App(e1,e2) ->
let te1t1 = typecheck ctx e1 in
let te2t2 = typecheck ctx e2 in
begin match te1t1,te2t2 with
| Exists (te1,t1),Exists (te2,t2) ->
begin match t1 with
| Arrow(t11,t12) ->
let p = is_equal t11 t2 in
begin match p with
| Some IsEqual ->
Exists ((TApp (te1,te2)) , t12)
| None ->
failwith "Mismatch of types on a function application"
end
| _ -> failwith "Tried to apply a non-arrow type"
end
end
| Add(e1,e2) ->
let te1t1 = typecheck ctx e1 in
let te2t2 = typecheck ctx e2 in
begin match te1t1,te2t2 with
| Exists (te1,t1),Exists (te2,t2) ->
let p = is_equal t1 t2 in
let q = is_integer t1 in
begin match p,q with
| Some IsEqual, Some IsInt ->
Exists ((TAdd (te1,te2)) , t1)
| _ ->
failwith "Tried to add with something other than Integers"
end
end
| And(e1,e2) ->
let te1t1 = typecheck ctx e1 in
let te2t2 = typecheck ctx e2 in
begin match te1t1,te2t2 with
| Exists (te1,t1),Exists (te2,t2) ->
let p = is_equal t1 t2 in
let q = is_boolean t1 in
begin match p,q with
| Some IsEqual, Some IsBool ->
Exists ((TAnd (te1,te2)) , t1)
| _ ->
failwith "Tried to and with something other than Booleans"
end
end
let e1 = Add(Int 1,Add(Int 2,Int 3))
let e2 = Add(Int 1,Add(Int 2,Bol false))
let e3 = App(Lam(Integer,Add(Var0,Var0)),Int 4)
let e4 = App(App(Lam(Integer,Lam(Integer,Add(Var0,VarS(Var0)))),Int 4),Int 5)
let e5 = Lam(Integer,Lam(Integer,VarS(Var0)))
let e6 = App(Lam(Integer,Var0),Int 1)
let e7 = App(Lam(Integer,Lam(Integer,Var0)),Int 1)
let e8 = Lam(Integer,Var0)
let e9 = Lam(Integer,Lam(Integer,Var0))
let tet1 = typecheck CEmpty e1
(*let tet2 = typecheck CEmpty e2*)
let tet3 = typecheck CEmpty e3
let tet4 = typecheck CEmpty e4
let tet5 = typecheck CEmpty e5
let tet6 = typecheck CEmpty e6
let tet7 = typecheck CEmpty e7
let tet8 = typecheck CEmpty e8
let tet9 = typecheck CEmpty e9
let rec eval : type gamma t. gamma -> (gamma,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 (env,x) e
| TVar0 ->
let (env,x)=env in
x
| TVarS e ->
let (env,x)=env in
eval env e
| TInt i -> i
| TBol b -> b
type exists_v =
| ExistsV : 't -> exists_v
let typecheck_eval e =
let tet = typecheck CEmpty e in
match tet with
| Exists (te,t) -> ExistsV (eval () te)
let v1 = typecheck_eval e1
let v3 = typecheck_eval e3
let v4 = typecheck_eval e4
let v5 = typecheck_eval e5
let v6 = typecheck_eval e6
let v7 = typecheck_eval e7
let v8 = typecheck_eval e8
let v9 = typecheck_eval e9
以下是我遇到麻烦的部分以及我如何设法解决它们