我使用幻影类型来模拟堆栈的状态,作为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
的亚型。
任何想法?
的问候大车
编辑
经过考虑,我想到了这个:
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将在堆栈上推送任何类型
下面的结构呢?
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
上)来表示"any kind is"好"。使用多态变体,可以使用子类型但是我宁愿建议不要使用,因为它更以及它与您想要使用的gadt的交互在内部实现您的幻影类型签名,或者直接暴露gadt)更有问题。
PS:这正是标准Bigarray模块使用"kind types"来达到类似目的的方式。
编辑:上面的公式有点尴尬,因为多态变体也使用多态性(在有限的特定情况下使用子类型),并且可能仅在类型级变体中使用多态性。我关于这个解决方案过于复杂的评论仍然成立。