Как с помощью GADT определить в OCaml простой DSL, похожий на лямбда-исчисление? В частности, я не могу понять, как правильно определить средство проверки типов для преобразования нетипизированного AST в типизированный AST, а также не могу определить правильный тип для контекста и среды.
Вот код для простого языка, подобного лямбда-исчислению, с использованием традиционного подхода в OCaml.
(* 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"
Вот в чем проблема. Во-первых, я не уверен, как определить правильный тип для TLam и TVar в типе texp. Обычно я предоставляю типу имя переменной, но я не уверен, как это сделать в данном контексте. Во-вторых, я не знаю правильный тип контекста в функции проверки типов. Раньше я использовал какой-то список, но теперь я уверен в типе списка. В-третьих, после исключения контекста функция typecheck сама не проверяет тип. Это не срабатывает с сообщением
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
