使用OCaml GADT编写解释器 [英] Writing an interpreter with OCaml GADTs
问题描述
我正在OCaml中编写一个小型解释器,并使用GADT键入表达式:
I am writing a small interpreter in OCaml and am using GADTs to type my expressions:
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
但是我无法编译我的代码.我收到以下错误:
But I cannot get my code to compile. I get the following error:
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
,但是我不知道为什么.我还尝试了以下方法:
My understanding is that for some reason rho
is being coerced into a bool value env
, but I don't know why. I also tried the following:
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
但是我不确定这到底有什么不同,它也给我一个错误-尽管是另外一个错误:
But I am not sure how exactly that is different, and it also gives me an error -- albeit a different one:
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
之间的差异以及此特定问题,均受到赞赏.干杯.
Guidance on GADTs, differences between the two eval
s, and this particular problem are all appreciated. Cheers.
推荐答案
类型'a env
用于表示名称/值绑定的列表,但列表中的值必须全部为同一类型.两种不同的值类型(例如bool value
和int value
)不是同一类型.如果eval b rho
返回Bool b
,则rho
必须是string * bool value
的列表.因此eval l rho
和eval r rho
将返回bool value
.但是您的注释说该函数返回a value
.
The type 'a env
is intended to represent a list of name/value bindings, but the values in a list must all be the same type. Two different value types (such as bool value
and int value
) are not the same type. If eval b rho
returns Bool b
, rho
must be a list of string * bool value
. So eval l rho
and eval r rho
will return bool value
. But your annotation says the function returns a value
.
这篇关于使用OCaml GADT编写解释器的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!