functional-programming - 在签名中隐藏类型参数

Question

OCaml 无法在签名中展开中间参数化类型是否有原因？

例如：

(* foo.ml *)
type 'a internal = Foo of 'a
type t = string internal

和：

(* foo.mli *)
type t = Foo of string

给一个错误。

我想这与内存表示有时可能不同的事实有关，但我想知道在向 OCaml 错误跟踪器提交错误报告之前是否有任何更深层次的原因......

Answer 1

只要类型是结构类型，它就可以，例如：

type 'a t = 'a * int
type u = string t

将匹配

type u = string * int

但是，变体（和记录）是OCaml 中的名义类型。也就是说，这种类型的每个声明都会引入一个新的类型名称。并且签名中的名义类型规范只能与名义类型声明匹配，并且它们必须具有等效的定义。您的示例中也不是这种情况，因此不被接受。（这是 OCaml 的一个微妙角落。结构类型别名和名义类型定义共享相同语法的事实无济于事。）

FWIW，您还可以重新绑定名义类型：

type 'a t = Foo of 'a
type 'a u = 'a t = Foo of 'a

将匹配

type 'a u = Foo of 'a

但这也不允许您更改结构或参数，因此对您的情况没有帮助。

Answer 2

这不是一个内存表示问题。在将类型声明与类型签名匹配时，或者更一般地，在检查声明t1是否不如声明一般时t2，类型检查器当前仅考虑这三种情况：

• t2是抽象类型或类型缩写
• t1并且t2都是总和类型
• t1并且t2都是记录

其他情况因错误而失败。在您的情况下，t1（被检查的类型）是类型缩写，t2（规范）是总和类型。这失败并出现类型错误。

查看源代码：type_declarations在typing/includemod.ml中。

这不是内存表示考虑，因为foo.ml这也会失败：

type u = Foo of string
type t = u

也许这个检查可以改进。您应该在 bugtracker 上询问。

编辑：说出这个检查应该改进到什么程度并非易事。在检查签名匹配时，通常在签名侧扩展缩写是不正确的，例如不应接受以下内容：

module Test : sig
  type t = Foo
  type u = t (* to the outside, t and u would be equal *)
end = struct
  type t = Foo (* while internally they are different *)
  type u = Foo (* sum/records are generative/nominative *)
end

反过来（内部相等对外部隐藏）是正确的并且已经可能：

module Test : sig
  type t = Foo
  type u = Foo
end = struct
  type t = Foo
  type u = t = Foo
end;;

fun (x : Test.t) -> (x : Test.u);;
(* Error: This expression has type Test.t but an expression
   was expected of type Test.u *)

现在，在考虑缩写扩展时，内存表示也被考虑在内，因为这种扩展不会保留类型系统的动态语义（内存表示选择）：

module Test : sig
  type r = { x : float; y : float; z : float } (* boxed float record *)
end = struct
  type 'a t = { x : 'a; y : 'a; z : 'a } (* polymorphic record *)
  type r = float t
end