是否可以在Idris中将相关类型变量连接到该数据类型的属性

问题描述

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

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

data Colour = Red | Black

eq_color : Colour -> Colour -> Bool
eq_color Red Red = True
eq_color Black Black = True
eq_color _ _ = False

Eq (Colour) where
  (==) = eq_color

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 (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 p) col elem
      NodeRh : Ord elem => (left: RBTree p _ elem) -> (val: elem) -> (col: Colour) ->
                            (h: Nat) -> (right: RBTree (S p) _ elem) -> RBTree (S p) col elem

我想知道的是，是否可以将RBTree的h属性连接到RBTree类型的height变量中。 因此，例如，对于NodeRh和NodeLh，基于if语句，h =（S p），对于NodeEq，对于h =（S p）或h = p。 >

基本上是给定的

(left: RBTree _ _ elem) -> (val: elem) -> (col: Colour) -> (h: Nat) -> (right: RBTree _ _ elem) -> RBTree h col elem

如何确保h中的(h: Nat)与h中的RBTree h col elem相同？

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）