idris - 尝试为两人游戏键入决策树

Question

我想为一个两人游戏（例如井字游戏）构建一个决策树，它的类型确保它是完整的。也就是说，我希望树节点的类型能够确保它的子节点恰好是它的所有后继节点。

这是我在伊德里斯的尝试。Tic-Tac-Toe 很复杂，所以我做了一个简单得多的游戏：在 ( A | B | C) 处移动三个位置，并且游戏在移动后结束。

DTNode是“决策树节点”。

data Player = Computer | Human
Eq Player where
  Computer == Computer = True
  Human == Human = True
  _ == _ = False
Show Player where
  show Computer = "Computer"
  show Human = "Human"
opponent : Player -> Player
opponent Computer = Human
opponent Human = Computer

data Position = A | B | C
Move : Type
Move = (Player, Position)

State : Type
State = List Move
isFinal : State -> Bool
isFinal (a::_) = True
isFinal _ = False
successorStates : State -> (toMove: Player) -> List State
successorStates s toMove = case (isFinal s) of
  True =>
    []

  False =>
    [(toMove, A)::s, (toMove, B)::s, (toMove, C)::s]

mutual
  SuccessorDTNodeType : (s : State) -> (toMove: Player) -> (successors: List State) -> Type
  SuccessorDTNodeType _ _ [] = the Type ()
  SuccessorDTNodeType s toMove (successor::rest) = DTNode successor (opponent toMove) oneLevelDownNodeType -> SuccessorDTNodeType s toMove rest where
    oneLevelDownNodeType = SuccessorDTNodeType successor (opponent $ opponent toMove) (successorStates successor toMove)

  data DTNode : (s: State) -> (toMove: Player) -> SuccessorDTNodeType s toMove (successorStates s toMove) -> Type where

我收到以下类型错误：

   |
45 |     oneLevelDownNodeType = SuccessorDTNodeType successor (opponent $ opponent toMove) (successorStates successor toMove)
   |                            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of Main.SuccessorDTNodeType, oneLevelDownNodeType with expected type
        SuccessorDTNodeType successor (opponent toMove) (successorStates successor (opponent toMove))

Type mismatch between
        Type (Type of SuccessorDTNodeType successor (opponent (opponent toMove)) (successorStates successor toMove))
and
        SuccessorDTNodeType successor
                            (opponent toMove)
                            (case isFinal successor of
                               True => []
                               False => [(toMove, A) :: s, (toMove, B) :: s, (toMove, C) :: s]) (Expected type)

我只是略懂；我的猜测是Type, 的返回类型SuccessorDTNodeType不够具体，无法满足我的DTNode构造函数的要求。

是这样吗，如果是这样，我可以做些什么来解决它吗？

标签： idris