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

【问题标题】：Idris returning dependent type signature error with if statement in type definitionIdris 在类型定义中使用 if 语句返回依赖类型签名错误
【发布时间】：2020-09-10 14:37:49
【问题描述】：

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

我正在尝试具体说明节点定义与其子节点的黑色高度的关系。 NodeEq - 两个孩子的 bh 相同，NodeLh 表示左孩子的 bh 比右孩子大 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 的黑色高度时遇到问题。我想要实现的，这在下面的代码中可能很明显，如果两个孩子都是黑色节点，那么黑色高度应该是它们的 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”块，但我不确定如何去做。

【问题讨论】：

标签： functional-programming idris dependent-type red-black-tree

【解决方案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 混为一谈。

【讨论】：