Как использовать менгир для анализа выражения GADT?

Я только что узнал кое-что о GADT в OCaml через Real World OCaml и хочу попробовать перенести первый небольшой язык там в интерпретатор, используя таким образом менгир.

Определение 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)}

Эта ошибка полностью аналогична той, которую мы получаем в первом блоке кода главы GADT, Locally Abstract Types, and Polymorphic Recursion Real World OCaml, где автор пытается рассматривать GADT как обычное отклонение. Здесь та же проблема? Если да, то как я могу это исправить, чтобы все заработало.

В руководстве по менгиру нет ничего особенного о GADT. Это упоминается во флаге --inspection. Я попробовал это, и ничего не меняется.


57
1

Ответ:

Решено

Основная проблема заключается в том, что вы пытаетесь написать функцию типа

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.