我正在尝试在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
该功能的内容现在是无稽之谈，但关键在于它需要非平凡（运行时）计算来确定新游戏状态是否需要（非）出价移动或纸牌移动。在这里，我不知道正确的类型声明。
此外，正确定义时，函数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有关吗？如果没有，可以通过使用一流的模块编码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)
@ 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 *)
请注意这里输入出价的明确举动。您只能根据其他类型信息确定类型。特别是你不能说“游戏现在正在竞标，因为卡片列表是空的”而没有解除卡片列表在类型级别为空的事实。
如果你问我，我认为这是非常矫枉过正的，但是呃。 ：p
首先，这对第一次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
(* ... *)
请注意，第二种方法允许您在不知道我们所处的阶段的情况下访问公共。您可能不希望这样。同样适用不会束缚下一阶段。如果你想这样做，你必须将这个方法与前一个方法结合起来。
GADT可能非常令人愤怒，但与他们合作非常有趣。如您所见，您经常需要具有专用于操作类型信息的构造函数，而不需要与之关联的任何实际数据。一旦你掌握了这种思维方式，你就可以做得非常棒 输入错误消息 类型安全的代码。
编辑：
您现在想要使用第一类模块来隐藏类型信息，这不是一个好主意。你获得了与game2技巧完全相同的东西，但语法更加痛苦。
另外，@ Drup的解决方案比我的好。