OCaml中的高阶类型（幻象类型子类型化）

Question

OCaml中的高阶类型（幻象类型子类型化）

4

我正在使用虚拟类型来模拟堆栈的状态，作为ocaml-lua的包装模块（Lua通过堆栈与C/OCaml通信）。以下是一个小的代码示例:

type 's t
type empty
type 's table
type top

val newstate : unit -> empty t           (* stack empty *)
val getglobal : empty t -> top table t   (* stack: -1 => table *)

在Lua中，表和数组表（没有真正的数组）都可以进行某些堆栈操作，但有些操作是不可行的。因此，如果我有以下类型：

type 's table
type 's array

我希望有一种类似于表格或数组的函数类型，可以同时操作两种类型，但仍能禁止如rawgeti（数组操作）在表格上的使用。 objlen是一个堆栈操作，返回堆栈顶部元素的“长度”。该元素可以是表格或数组表格。目前，封装函数定义如下：

val objlen : (top table) t -> int

What I want is

val objlen : (top table-or-array) t -> int

那么，array和table是table-or-array的子类型。

有什么想法吗？

谢谢 Olle

编辑

经过考虑，我得出了以下结论：

module M : sig
  type ('s, 't) t

  (* New Lua state with empty stack *)
  val newstate : unit -> (unit, unit) t

  (* Get table *)
  val getglobal : ('a) t -> ([< `table | `string | `number | `fn], 'a) t

  (* Get array index and put "anything" on top of stack *)
  val rawgeti : ([`table], 'a) t -> ([< `table | `string | `number | `fn], [`table] * 'a) t

  (* String on top of stack *)
  val tostring : ([`string], _) t -> string

  (* Table or array-table on top of stack *)
  val objlen : ([`table], _) t -> int

  val pop : ('a, 'b * 'c) t -> ('b, 'c) t
end = struct
  type top
  type ('s, 't) t = string      (* Should really be Lua_api.Lua.state *)

  (* Dummy implementations *)
  let newstate () = "state"
  let gettable s = s
  let getarray s = s
  let rawgeti s = s
  let tostring s = "Hello phantom world!"
  let objlen s = 10
  let pop s = s
end

在类型级别上的堆栈现在不应该比堆栈本身多也不应该比堆栈本身少。例如，rawgeti将在堆栈上推送任何类型。

- Olle Härstedt

1

type ('s, 't) t val objlen : (top, [< \table | `array]) t -> int` 是什么意思？ - lukstafi

实际上类型 [< \table | `array]与[`table | `array]` 是相同的。 - lukstafi

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- gasche · Accepted Answer

以下结构怎么样？

type ('data, 'kind) t
type array_kind
type stack_kind

(* use tuples as type-level lists:
   (a * (b * (c * unit))) for the stack of type-shape [a;b;c] *)
val newstate : unit -> (unit, stack) t
val getglobal : (unit, stack) t -> (top * unit, stack) t

val objlen : (top * 'a, 'k) t -> int

这里使用多态性（在'k上）表达“任何类型都可以”。使用多态变体，可以改用子类型，但我更建议不要这样做，因为它更复杂，而且与GADTs的交互（您想在内部使用实现您的幻影类型签名，或者直接公开GADTs）更有问题。

PS：这正是标准Bigarray模块使用“类型种类”以实现类似功能的方式。

编辑：上述表述有点笨拙，因为多态变体也使用多态性（子类型仅用于特定受限情况），并且可以仅在类型级别变量中使用多态性。我对这种解决方案过于复杂的评论仍然成立。