OCaml 的 GADT 和很多类型变量

Question

我正在尝试在 OCaml 中模拟纸牌游戏（为简单起见，我们假设它是纸牌游戏）。该游戏的给定状态由 game 类型的值表示。然后我将定义一个函数 moves : game -> move list 来给出给定游戏状态的有效移动列表；函数 apply: game -> move -> game 给出了进行给定移动后的状态。（此处显示的类型实际上可能会被多态类型替换，如下所述。）

碰巧这个游戏有两种性质不同的走法。在游戏的某些时刻，需要决定出价或不出价。在游戏的其他时间点，玩家只需要打一张牌。例如，将 apply g 应用到 m 应该是错误的，其中 g 需要（非）叫牌动作，而 m 是打牌动作。

我希望这个错误是静态错误。所以我想到了使用 GADT。我是这样开始的：

type card = int * int
type common = { cards : card list }
type play_phase = Play_phase
type bid_phase = Bid_phase
type _ game = Play_game :  common ->  play_phase game | Bid_game :  common ->  bid_phase game
type _ move =
  | Play : card -> play_phase move
  | Bid : bid_phase move
  | NoBid : bid_phase move

let moves : type a. a game -> a move list = function
  | Bid_game _ -> [Bid; NoBid]
  | Play_game _ ->  [Play (0,0)]

到目前为止所有这些类型检查。但是，以下内容不是：

let apply : type a b. (a game * a move) -> b game = function
  | (Bid_game g, _) -> Play_game g
  | (Play_game ({ cards = [] } as g), _) -> Bid_game g
  | (Play_game g, _) -> Play_game g

函数的内容现在是废话，但关键是它需要非平凡的（运行-time）计算来确定新的游戏状态是否需要（非）叫牌移动或打牌动作。在这里，我不知道正确的类型声明。

此外，函数 apply 在正确定义时必须具有类似于以下类型检查的内容：

(* ... *)
let rec loop g (* more parameters *) =
   let ms = moves g in
   let m = (* choose an element of ms somehow *) in
   loop (apply g m) (* more parameters *)
(* ... *)

这可以用 GADT 实现吗？如果不是，是否可以通过使用 first-class 模块对 GADT 进行编码来规避？还是必须求助于对象系统？

（如果这是相关的，我将在使用 js_of_ocaml 编译的代码的最内层循环中使用这些函数。）

编辑：回应 PatJ 的回答：

module type Exist = sig type t val x : t game end

let apply' : type a. a game -> a move -> (module Exist)
  = fun { data = cs }  m ->
  match cs with
  | [] ->
     let module M =  struct
         type t = bid_phase 
         let x = { phase = Bid_phase; data = [] }
       end in
     (module M)
  | cs ->
     let module M = struct
         type t = play_phase
         let x = { phase = Play_phase; data = cs}
       end in
     (module M)

Answer 1

首先，这对于第一次尝试 GADT 来说非常好。您的问题确实是您的 b 类型变量无法静态知道。

现在您可以根据自己的需要使用多种方法来避免这种情况。

最简单的解决方案是创建一个隐藏类型信息的 ADT：

type game2 = P of play_phase game | B of bid_phase game

请注意，您将无法在 game2 值的模式匹配之外访问这些类型。您基本上必须将 play_phase game 和 bid_phase game 视为两种不同且不兼容的类型。

另一种给您更多回旋余地（但可能不是您想要的）的可能性是将您的数据与类型证明分开：

(* Same types as yours, except for the game definition *)
type _ game_phase = Play_game : play_phase game_phase | Bid_game :  bid_phase game_phase
type 'a game = { data: common; phase: 'a game_phase; }


let moves : type a. a game -> a move list = function
  | { phase = Bid_game; _ } -> [Bid; NoBid]
  | { phase = Play_game; _ } ->  [Play (0,0)]

let apply : type a. (a game * a move) -> common = function
(* ... *)

请注意，第二种方法允许您在不知道我们所处阶段的情况下访问 common。您可能不希望这样。也适用不绑定下一阶段。如果要这样做，则必须将此方法与前面的方法结合使用。

GADT 可能非常令人恼火，但与它们一起工作非常有趣。如您所见，您通常需要有专门用于操作类型信息的构造函数，而无需任何实际数据与之关联。一旦你掌握了这种思维方式，你就可以做一些非常棒的~~类型错误消息~~类型安全代码。

编辑：

您现在想使用第一个 class 模块来隐藏类型信息，这不是一个好主意。您获得的结果与使用 game2 技巧完全相同，但语法要痛苦得多。

此外，@Drup 的解决方案比我的好。

Answer 2

@PatJ 的解决方案是隐藏类型并尝试继续这样做。我认为这是一个糟糕的解决方案，因为最终它并没有真正给你任何东西，而是迫使你与存在主义玩捉迷藏。

相反，您应该接受这样一个事实，即您在类型系统中对状态机进行编码，其中游戏是状态，移动是过渡。如果这样做，路径似乎更清晰：转换总是从一种状态到另一种状态：

type card = int * int
type common = { cards : card list }
type play = Play
type bid = Bid
type _ game = Play_game :  common ->  play game | Bid_game :  common ->  bid game
type (_,_) move =
  | Play : card -> (play, play) move
  | StartBid : (play, bid) move
  | Bid : (bid, play) move
  | NoBid : (bid, play) move

type 'a any_move = Ex : ('a, 'b) move -> 'a any_move

let moves : type a. a game -> a any_move list = function
  | Bid_game _ -> [Ex Bid; Ex NoBid]
  | Play_game _ ->  [Ex (Play (0,0))]

let apply : type a b. a game -> (a, b) move -> b game =
  fun g m -> match m, g with
    | Bid, Bid_game g -> Play_game g
    | NoBid, Bid_game g -> Play_game g
    | StartBid, Play_game g -> Bid_game g
    | Play _c, Play_game g -> Play_game g

let rec loop : type a . a game -> _ =
  function g ->
    let ms = moves g in
    let Ex m = List.hd ms (* choose an element of ms somehow *) in
    loop (apply g m) (* more parameters *)

请注意此处输入出价的明确举动。您可以仅根据其他类型信息决定类型。特别是你不能说 "the game is now bidding because the list of cards is empty" 而不是将卡片列表为空的事实提升到类型级别。

如果你问我，我认为这太过分了，但是嗯。 :p

OCaml 的 GADT 和很多类型变量

OCaml's GADT and many type variables

ocaml

types

gadt