Idris 在类型定义中使用 if 语句返回依赖类型签名错误

Question

我正在研究 Idris 中的红黑树实现。在这个实现中，节点除了携带关于它的值和颜色的信息外，还携带关于它的黑色高度的信息（这是从该节点到任何叶子的黑色节点的数量，不包括它自己）。

我想具体说明节点定义与其 children 的黑色高度的关系。 NodeEq - children 都具有相同的 bh，NodeLh 表示左侧 child 的 bh 比右侧 child 大 1，NodeRh 与 NodeLh 相反。

data Colour = Red | Black

data RBTree : Nat -> Colour -> Type -> Type where
      Empty : Ord elem => RBTree Z Black elem
      NodeEq : Ord elem => (left: RBTree p X elem) -> (val: elem) -> (col: Colour) ->
                          (h: Nat) -> (right: RBTree p Y elem) -> RBTree {h: Nat | if X == Black && Y == Black then (S p) else p} col elem
      NodeLh : Ord elem => (left: RBTree (S p) _ elem) -> (val: elem) -> (col: Colour) ->
                            (h: Nat) -> (right: RBTree p _ elem) -> RBTree (S (S p)) col elem
      NodeRh : Ord elem => (left: RBTree p _ elem) -> (val: elem) -> (col: Colour) ->
                            (h: Nat) -> (right: RBTree (S p) _ elem) -> RBTree (S (S p)) col elem

我在为 NodeEq 设置黑色高度时遇到问题。我想要实现的，在下面的代码中可能很明显，如果两个 children 都是黑色节点，那么黑色高度应该是它们的 bh + 1，否则黑色高度应该等于它们的高度.但是，我不知道如何将其写入定义。如您所见，我使用的是一般 {x:b|p} 格式。

这是我遇到的错误

  |
9 |                           (h: Nat) -> (right: RBTree p Y elem) -> RBTree {h: Nat | if X == Black && Y == Black then (S p) else p} col elem
  |                                                                            ^
unexpected ':'
expecting dependent type signature

我也考虑过创建一个 'where' 或 'let' 块，但我不确定如何去做。

Answer 1

中的语法

RBTree {h: Nat | if X == Black && Y == Black then (S p) else p} col elem

不正确。 RBTree 的第一个索引的类型为 Nat，因此您只想在此处放置一个 Nat 类型的术语：

RBTree (if X == Black && Y == Black then (S p) else p) col elem

您可能混淆了优化类型语法（来自类似 Liquid Haskell 的语法）与 Idris。

Idris 在类型定义中使用 if 语句返回依赖类型签名错误

Idris returning dependent type signature error with if statement in type definition

functional-programming

idris

dependent-type

red-black-tree