在OCaml中使用GADT时,如何删除函数中的"不太通用的定义"错误消息？

Question

我最近在OCaml一直在与GADT挣扎.我正在尝试为一种简单的语言编写一个解释器,使用不同的术语:

type (_, _) term =
  | Const : lit -> (state, value) term
  | Var : ident -> (state, value) term
  | Plus : expr * expr -> (state, value) term
  | Equ : expr * expr -> (state, value) term
  | Neg : expr -> (state, value) term
  | Skip : (state, state) term
  | Asn : ident * expr -> (state, state) term
  | Seq : stat * stat -> (state, state) term
  | If : expr * stat * stat -> (state, state) term
  | While : expr * stat -> (state, state) term
and expr = (state, value) term
and stat = (state, state) term

('a,'b)项是一个术语,当用'a'计算时,返回'b'(通常,表达式用状态计算并返回一个值,而语句只是将给定状态修改为另一个状态) ).

我一直在尝试为解释器创建函数,我得到一个奇怪的错误消息,我无法理解.这是评估功能:

let rec eval : type a b. a -> (a, b) term -> b = fun state term ->
  match term with
  | Const lit -> eval_lit_int state lit
  | Var ident -> eval_var eval state ident
  | Plus(e1, e2) -> eval_add eval state e1 e2
  | Equ(e1, e2) -> eval_eq eval state e1 e2
  | Neg e -> eval_neg eval state e
  | Skip -> eval_skip eval state
  | Asn(ident, e) -> eval_asn eval state ident e
  | Seq(s1, s2) -> eval_seq eval state s1 s2
  | If(e, s1, s2) -> eval_if eval state e s1 s2
  | While(e, s) -> eval_while eval state e s

以下是模式匹配右侧部分中被调用函数的示例:

let eval_add f state e1 e2 =
  let x1 = f state e1 in
  let x1' =
    match is_int x1 with
    | None -> failwith ""
    | Some x1' -> x1'
  in
  let x2 = f state e2 in
  let x2' =
    match is_int x2 with
    | None -> failwith ""
    | Some x2' -> x2'
  in
  match add x1' x2' with
  | None -> failwith ""
  | Some x0 -> x0

不介意未记录的失败,目前仍在构建代码.对于'eval'函数,我收到此错误消息,我无法理解:

This definition has type 'a -> ('a, 'b) term -> 'b
which is less general than 'a0 'b0. 'a0 -> ('a0, 'b0) term -> 'b0

有人有相同的错误消息吗？我怎么能让它消失？我猜它来自对'eval'的递归调用,这是我无法避免的.谢谢你的帮助 !

Answer 1

首先,让我们添加一些假设来规避丢失的代码:

假设1:

你正在使用梅林.在这种情况下,错误消息

该定义的类型为'a - >('a,'b)term - >'b,它不如'a0'b0.'a0 - >('a0,'b0)术语 - >'b0

有时恰好掩盖了真正的错误信息

假设2:

你eval_if和eval_while功能样子

let eval_if eval state e s1 s2 =
  if (to_bool @@ eval state e) then
    eval state s1
  else
    eval state s2

和

let eval_while eval st e s =
  let st = ref st in
  while (to_bool @@ eval !st e) do
    st := eval !st s
  done; !st

回答:

然后真正的错误在于,使用这些定义eval_while并且eval_if返回值而不是状态.实际上,该行to_bool @@ eval !st e意味着函数参数eval必须返回一个值.因此,所有后续调用都eval state x返回一个值,因为函数参数不是多态的.

这可以通过提供两个evals函数来解决,一个用于值,一个用于状态eval_while,eval_if或者通过将参数包装在eval具有多态字段的记录中(这是OCaml方式来模拟更高级别的多态性,请参阅http:// caml. inria.fr/pub/docs/manual-ocaml/polymorphism.html#sec60):

type eval = { eval: 'a 'b. 'a -> ('a,'b) term -> 'b }
let eval_if {eval} state e s1 s2 =
  if (to_bool @@ eval state e) then
    eval state s1
  else
    eval state s2
let eval_while {eval} st e s =
  let st = ref st in
  while (to_bool @@ eval !st e) do
    st := eval !st s
  done; !st

然后以下略微修改的eval函数应该工作:

let rec eval : type a b. a -> (a, b) term -> b = fun state term ->
  match term with
  | Const lit -> eval_lit_int state lit
  | Var ident -> eval_var eval state ident
  | Plus(e1, e2) -> eval_add eval state e1 e2
  | Equ(e1, e2) -> eval_eq eval state e1 e2
  | Neg e -> eval_neg eval state e
  | Skip -> eval_skip eval state
  | Asn(ident, e) -> eval_asn eval state ident e
  | Seq(s1, s2) -> eval_seq eval state s1 s2
  | If(e, s1, s2) -> eval_if {eval} state e s1 s2
  | While(e, s) -> eval_while {eval} state e s