主页 / coding / 问题 / 77105070
Accepted
glennsl
Asked: 2023-09-14 20:52:49 +0800 CST

使用一流模块进行子类型强制

  • 772

给定以下模块签名，其中B包含A：

module type A = sig
  type t
end

module type B = sig
  type t
  val x: t
end

通常，任何满足 的模块B也将满足A。然而，这不会自动扩展到一流模块，因为它当然是一种不同的类型语言，不允许与子类型自动统一。但手动强制应该仍然有效，不是吗？（事实上​​，如果模块签名仅包含类型定义，则确实如此，但如果它包含值则不然。）

let f (_: (module A)) = ()
let g (b: (module B)) = f (b :> (module A)) (* Error: Type (module B) is not a subtype of (module A) *)

这是一流模块的基本限制吗？在核心类型语言中，确定一个模块类型是否是另一个模块类型的子类型的规则是什么？有没有实际的解决方法？

types

2 个回答

  1. Best Answer

    类型强制是 OCaml 中仅类型级别的操作。换句话说，它预计在运行时是无操作的。

    为了保留此属性，第一类模块的子类型需要使用受限模块子类型关系：(module A)<：(module B)当且仅当 A<:B两种模块类型的所有运行时组件出现在相同位置。

    例如，这很好：

    module type A = sig
  type x = int
  type y = float
  val x : x
  val y :y
end
module type B = sig
  val x:int
  val y:float
end
let f (x:(module A) list) = (x:>(module B) list)

    因为两种模块类型都同意第一个运行时组件是x，第二个运行时组件是y。恰恰相反

    module type C = sig
  val y:int
  val x:float
end
let f (x:(module C) list) = (x:>(module B) list)

    x失败，因为两种模块类型在字段和的位置上不一致y。

    • 1

  2. 为了回答我自己关于实际解决方法的问题，当然可以解压并重新打包模块。在这个简单的例子中，这非常方便：

    let g (module B: B) = f (module B)

    然而，当一流模块嵌入到某些数据结构中时，这有点不太方便。

    • 0

相关问题