3

我正在使用幻像类型来模拟堆栈的状态，作为 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

我想要一种类似 table-or-array 的函数，用于在这两种类型上运行的函数，但仍然能够rawgeti在表上禁止例如（数组操作）。objlen是一个堆栈操作，它返回堆栈顶部元素的“长度”。该元素可以是表或数组表。目前，包装函数定义如下：

val objlen : (top table) t -> int

我想要的是

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 将推送任何类型的堆栈。

4

1 回答 1

4

那么下面的结构呢？

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

这使用多态性 (on 'k) 来表达“任何种类都可以”。使用多态变体，可以改用子类型，但我宁愿反对它，因为它更复杂并且它与 GADT 的交互（您希望在内部使用它来实现您的幻像类型签名，或者可能直接公开 GADT ) 问题更大。

PS：这正是标准Bigarray模块出于类似目的使用“种类类型”的方式。

编辑：上面的公式有点尴尬，因为多态变体也使用多态性（在受限的特定情况下使用子类型），并且可以只在类型级变体中使用多态性。我对这个解决方案过于复杂的评论仍然有效。

于 2013-06-08T09:47:23.950 回答