Проблема компиляции функтора: несоответствие подписи: модули не совпадают

Сначала код:

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

Чего я не понимаю, так это того, как более конкретный тип не включается в более общий тип?


functor ocaml
person aneccodeal    schedule 20.04.2012    source источник

Ответы (1)


arrow_upward
5
arrow_downward

Сообщение об ошибке на самом деле довольно точное:

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 теперь работает с логическими выражениями над фиксированным типом 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.

person Stefan Holdermans    schedule 20.04.2012