何时在OCaml中删除类型错误

Question

下面的代码显示val refl : ('a, 'a) eq组件的不匹配错误

Error: Signature mismatch:
       ...
       Values do not match:
         val refl : ('_a, '_a) eq
       is not included in
         val refl : ('a, 'a) eq
       File "lib/SO_typenoarg.ml", line 38, characters 2-24:
         Expected declaration
       File "lib/SO_typenoarg.ml", line 62, characters 6-10:
         Actual declaration

module Leibniz_ERROR : sig
  type ('a, 'b) eq

  val refl : ('a, 'a) eq
end = struct
  module type m = sig
    type 'a m
  end

  module type TyEq = sig
    type a
    type b
  end

  module Refl (X : sig
    type x
  end) : TyEq with type a = X.x and type b = X.x = struct
    type a = X.x
    type b = X.x
  end

  type ('a, 'b) eq = (module TyEq with type a = 'a and type b = 'b)

  module R = Refl (struct
    type x = int
  end)

  let refl (type a) : (a, a) eq =
    (module Refl (struct
      type x = a
    end))
end

它是通过延迟refl来解决的(对我来说有点神秘)

module Leibniz : sig
  type ('a, 'b) eq

  val refl : unit -> ('a, 'a) eq
end = struct
  module type m = sig
    type 'a m
  end

  module type TyEq = sig
    type a
    type b
  end

  module Refl (X : sig
    type x
  end) : TyEq with type a = X.x and type b = X.x = struct
    type a = X.x
    type b = X.x
  end

  type ('a, 'b) eq = (module TyEq with type a = 'a and type b = 'b)

  module R = Refl (struct
    type x = int
  end)

  let refl (type a) : unit -> (a, a) eq =
   fun _ ->
    (module Refl (struct
      type x = a
    end))
end

你有什么实用的经验法则，什么时候添加一个雷击？

Answer 1

它被称为eta-展开，它的目的是将一个值(它可以是任何值，包括做一些令人讨厌的事情的闭包)转换成一个语法值，并保证它在静态时间中被完全定义(也就是说，它不是一个计算的问题)。

换句话说，当一个类型变量没有一个基本类型，并且它被归因于一个非句法的值(即计算的结果)或一个不适用于放宽的值限制的值时，就引入了弱变量。放松的价值限制部分是相当有趣的，但令人费解。它允许对非句法常量的值进行泛化(将类型变量转换为多态类型)。关于弱变量的高层概述，请参阅本文中关于值限制及其与子类型和协方差的交互的部分。下面是关于这个主题的更多学术阅读。

最后，您的eq类型可以很容易地定义，而无需使用常量的语法值进行计算，例如，使用GADT、type ('a,'b) eq = T : ('a,'a) eq，例如，

module Leibniz : sig
  type ('a, 'b) eq

  val refl : ('a, 'a) eq
end = struct
  module type m = sig
    type 'a m
  end

  module type TyEq = sig
    type a
    type b
  end

  module Refl (X : sig
      type x
    end) : TyEq with type a = X.x and type b = X.x = struct
    type a = X.x
    type b = X.x
  end

  type ('a,'b) eq = T : ('a,'a) eq


  module R = Refl (struct
      type x = int
    end)

  let refl (type a) : (a, a) eq = T
end

Answer 2

这就是工作中的价值限制。

   (module Refl (struct
      type x = a
    end))

是一个计算而不是一个句法值，因此它不能用let绑定来概括。