如何解决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混用。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。