使用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 evals, 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屋！