ocaml - 仿函数编译问题 : Signature mismatch: Modules do not match

Question

首先是代码:

module Boolean = struct
  exception SizeMismatch
  type boolean = T | F | Vec of boolean array 

  let to_bool v = match v with 
    T -> true
  | F -> false 
  | _ -> raise SizeMismatch
end

module Logic = struct
  type 'a var_t = { name: string; mutable value: 'a }
  type 'a bexp  = Const of 'a
  |             Var of 'a var_t

  let eval exp = match exp with
    Const x -> x
  | Var x   -> x.value

  let make_var s v = { name = s; value = v }
  let set v n = v.value <- n
  let get_var_name v = v.name
  let get_var_val  v = v.value
end

module type EXP =
  sig
    type  'a var_t
    type  'a bexp
    val eval_exp     : 'a bexp -> bool
    val get_var_name : 'a var_t -> string
    val get_var_val  : 'a var_t -> 'a
  end

module LogicExp = 
  struct
    include Logic
    let eval_exp exp = Boolean.to_bool (Logic.eval exp)
  end

module FSM ( Exp : EXP ) = 
  struct
    let print_var v = Printf.printf "%s = %d\n" (Exp.get_var_name v)
    (Exp.get_var_val v)

  end

module MyFSM = FSM(LogicExp) 

let myvar = Logic.make_var "foo" 1;;

MyFSM.print_var myvar ;;

编译时出现以下错误:

File "test.ml", line 57, characters 19-27:
Error: Signature mismatch:
   Modules do not match:
     sig
       type 'a var_t =
         'a Logic.var_t = {
         name : string;
         mutable value : 'a;
       }
       type 'a bexp = 'a Logic.bexp = Const of 'a | Var of 'a var_t
       val eval : 'a bexp -> 'a
       val make_var : string -> 'a -> 'a var_t
       val set : 'a var_t -> 'a -> unit
       val get_var_name : 'a var_t -> string
       val get_var_val : 'a var_t -> 'a
       val eval_exp : Boolean.boolean Logic.bexp -> bool
     end
   is not included in
     EXP
   Values do not match:
     val eval_exp : Boolean.boolean Logic.bexp -> bool
   is not included in
     val eval_exp : 'a bexp -> bool

我不明白的是，更具体的类型为何不包含在更一般的类型中？

Answer 1

错误信息实际上是相当准确的:

Values do not match:
  val eval_exp : Boolean.boolean Logic.bexp -> bool
is not included in
  val eval_exp : 'a bexp -> bool

MyFSM仿函数需要一个模块参数，除其他外，应该包含一个函数 eval_exp类型 'a bexp -> bool .这意味着给定类型的值 'a bexp对于 'a 的任何选择该函数应产生 bool 类型的值.但是，您提供的模块包含一个函数，该函数仅针对 'a 的一个特定选择执行此操作。 ，即'a是类型 boolean来自模块 Boolean .

最快的解决方法是定义您的签名 EXP作为

module type EXP =
  sig
    type  b  (* added *)
    type  'a var_t
    type  'a bexp
    val eval_exp     : b bexp -> bool  (* changed *)
    val get_var_name : 'a var_t -> string
    val get_var_val  : 'a var_t -> 'a
  end

所以eval_exp现在对固定类型的 bool 表达式进行运算 b然后定义 LogicExp作为

module LogicExp =
  struct
    type b = Boolean.boolean  (* added *)
    include Logic
    let eval_exp exp = Boolean.to_bool (Logic.eval exp)
  end

以便修复 b至 Boolean.boolean .

实现这些更改将使您的代码编译通过。

现在，让我们看看您的问题“更具体的类型为何不包含在更一般的类型中？”。这假设 'a bexp -> bool确实比boolean bexp -> bool更通用，但实际上并非如此。函数类型A -> B被认为比函数类型更通用 C -> D如果C比 A 更通用和 B比 D 更通用:

A <: C        D <: B
--------------------
  C -> D <: A -> B

注意 C 的“翻转”和 A在前提下。我们说函数空间构造函数 ... -> ...在其参数位置是逆变(相对于在其结果位置是协变)。

直觉上，如果一种类型包含更多值，则它比另一种类型更通用。要了解为什么函数空间构造函数在其参数位置是逆变的，请考虑一个函数 f类型 A -> C对于某些类型 A和 C .现在，考虑一个类型 B这比 A 更一般，即 A 中的所有值也在B ，但是B包含一些不在 A 中的值.因此，至少有一个值b。我们可以为其分配类型 B , 但不输入 A .它的类型告诉我们 f知道如何对 A 类型的值进行操作.但是，如果我们要(错误地!)从 A <: B 得出结论那A -> C <: B -> C , 那么我们可以使用 f就好像它有类型 B -> C因此，我们可以传递值 b作为 f 的参数.但是b不是 A 类型和 f只知道如何操作 A 类型的值!

很明显，... -> ... 的协方差在争论的立场上是行不通的。要查看逆变性是否有效，请考虑相同的类型 A , B , 和 C现在还考虑一个函数 g类型 B -> C .即 g知道如何对 B 类型的所有值进行操作.函数空间构造函数在其参数位置的逆变允许我们得出结论 g也可以安全地分配类型 A -> C .我们知道 A 中的所有值也在B和 g知道如何处理所有B这不会造成任何问题，我们可以安全地传递 A 中的值。至 g .