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

问题描述

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

我正在尝试使节点定义与子节点的黑色高度有关。 NodeEq-两个孩子的bh相同，NodeLh表示左孩子的bh比右孩子的bh大1，而NodeRh是NodeLh的倒数。

orginalToolTipValue

我在设置NodeEq的黑色高度时遇到问题。我要实现的目标（可能在下面的代码中显而易见）是，如果两个子节点均为黑色节点，则黑色高度应为其bh + 1，否则黑色高度应等于其高度。但是，我不知道如何将其写入定义中。如您所见，我正在使用一般的{x：b | p}格式。

这是我遇到的错误

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

我还考虑过创建“ where”或“ let”块，但是我不确定该怎么做。

解决方法

语法

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混用。