Functor编译问题:签名不匹配:模块不匹配

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的类型.booleanBoolean

最快的解决方法是将您的签名定义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现在对固定类型的布尔表达式进行操作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.