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。

何か案は？

よろしくオーレ

編集

検討の結果、私はこれを思いつきました：

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 に答える