我刚刚通过Real World OCaml了解了OCaml中的GADT,并且想尝试将那里的第一个小语言转移到解释器中,因此使用menhir。
ast 的定义与示例完全相同。如下:
type _ value =
| Int : int -> int value
| Bool : bool -> bool value
type _ expr =
| Value: 'a value -> 'a expr
| Eq : int expr * int expr -> bool expr
| Plus : int expr * int expr -> int expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
let eval_value : type a. a value -> a = function
| Int x -> x
| Bool x -> x ;;
let rec eval: type a. a expr -> a = function
| Value v -> eval_value v
| If (c, t, e) -> if eval c then eval t else eval e
| Eq (x, y) -> eval x = eval y
| Plus (x, y) -> eval x + eval y;
这是我的词法分析器和解析器规范
{
open Parser
exception Error of string
}
rule token = parse
| [' ' '\t'] {token lexbuf}
| '\n' {Lexing.new_line lexbuf; token lexbuf}
| "if" {IF}
| "then" {THEN}
| "else" {ELSE}
| '=' {EQ}
| '+' {PLUS}
| "true" {BOOL (true)}
| "FALSE" {BOOL (false)}
| ['0'-'9']+ as i {NUM (int_of_string i)}
| '-'['0'-'9']+ as i { NUM (int_of_string i) }
| eof {EOF}
| _ { raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
%{
open Ast
%}
%token <int> NUM
%token <bool> BOOL
%token PLUS
%token IF
%token THEN
%token ELSE
%token EQ
%token EOF
%left PLUS
%start <'a Ast.expr> expr_toplevel
%%
expr_toplevel:
| e = expr EOF {e}
expr:
| x = expr PLUS y = expr {Plus (x, y)}
| IF c = expr THEN x = expr ELSE y = expr {If (c, x, y)}
| x = expr EQ y = expr {EQ (x, y)}
| b = BOOL {Value (Bool b)}
| n = NUM {Value (Int n)}
就这样,上面的代码无法构建,得到的错误是:
File "bin/parser.mly", line 27, characters 18-26:
Error: This expression has type bool value
but an expression was expected of type int value
Type bool is not compatible with type int
指的是
| b = BOOL {Value (Bool b)}
这个错误与我们在 Real World OCaml 第
GADT, Locally Abstract Types, and Polymorphic Recursion
章第一个代码块中得到的错误完全相同,其中作者尝试将 GADT 视为普通方差。这里是同样的问题吗?如果是,我该如何解决这个问题以使其正常工作。
menhir 手册中没有太多关于 GADT 的内容。它在名为 --inspection 的标志中提到。我已经尝试过,但没有任何改变。
根本问题是您正在尝试编写类型的函数
val parse: (x:string) -> f(x) Ast.expr
其中解析的 ast 的类型取决于输入的值。 这只能在依赖类型语言中实现,而 OCaml 不是依赖类型的。
一个有价值的解决方案是让解析器返回一个表示
any Ast.expr
的类型,它可以用存在量化来定义:
type any_expr = Any: 'a Ast.expr -> any_expr [@@unboxed]
那么
expr
解析函数将具有类型:
val parse: string -> any_expr
并且仍然有可能有返回特定类型
expr
的子解析器。