gpt4 book ai didi

pattern-matching - 尽管案例拆分,但 Idris 无法解决约束

转载 作者:行者123 更新时间:2023-12-04 17:19:54 25 4
gpt4 key购买 nike

为了尝试学习 Idris,我决定尝试用它来实现红黑树。经过一番努力,我设法让树本身通过了类型检查器,现在我正在尝试定义一个 insert 函数,顾名思义,它会将一个元素插入到红黑树中。在当前,相当不完整的状态下,我的代码的相关部分如下所示:

data Color : Type where
Red : Color
Black : Color

mutual
data RedBlackTree : (Ord key_type) => Nat -> Color -> (key_type : Type) -> Type -> Type where
Empty : (impl : Ord key_type) => RedBlackTree @{impl} Z Black key_type v

BlackNode : (impl : Ord key_type) => (k : key_type) -> value_type ->
(left : RedBlackTree @{impl} black_height c_1 key_type value_type) ->
(right : RedBlackTree @{impl} black_height c_2 key_type value_type) ->
{auto left_legal : legal_child_of_key left k LT} ->
{auto right_legal : legal_child_of_key right k GT} ->
RedBlackTree @{impl} (S black_height) Black key_type value_type

RedNode : (impl : Ord key_type) => (k : key_type) -> value_type ->
(left : RedBlackTree @{impl} black_height Black key_type value_type) ->
(right : RedBlackTree @{impl} black_height Black key_type value_type) ->
{auto left_legal : legal_child_of_key left k LT} ->
{auto right_legal : legal_child_of_key right k GT} ->
RedBlackTree @{impl} black_height Red key_type value_type

legal_child_of_key : (impl : Ord k_type) => RedBlackTree @{impl} _ _ k_type _ -> k_type -> Ordering -> Type
legal_child_of_key Empty _ _ = Unit
legal_child_of_key (BlackNode child_key _ _ _) parent_key ord = ord = (compare @{impl} child_key parent_key)
legal_child_of_key (RedNode child_key _ _ _) parent_key ord = ord = (compare @{impl} child_key parent_key)

TreeMap : (Ord k) => (k : Type) -> Type -> Type
TreeMap @{impl} k v = DPair (Nat, Color) $ \case (d, c) => RedBlackTree @{impl} d c k v

insert : (impl : Ord k) => TreeMap @{impl} k v -> k -> v -> TreeMap @{impl} k v
insert (((S d), Black) ** (BlackNode @{impl} p_k p_v left right)) k v = case compare @{impl} k p_k of
LT => case left of
Empty => MkDPair (S d, Black) (BlackNode @{impl} p_k p_v (RedNode @{impl} k v Empty Empty) right {left_legal = ?left_legal_prf})
real_node => ?insert_left_black

我面临的问题是 Idris 不让我用 left_legal = Refl 填充那个 ?left_legal_prf 洞,声称它不能解决约束在 compare k p_kLT 之间。尽管只是在 compare k p_k 上匹配了模式并发现它是 LT。显式提供类似 the (LT = compare @{impl} key p_k) Refl 的类型似乎也无济于事。

:t left_legal_prf 输出

Data.RedBlackTree> :t left_legal_prf
impl : Ord k
right : RedBlackTree 0 c_2 k v
p_k : k
p_v : v
k : k
v : v
left : RedBlackTree 0 Black k v
d : Nat
------------------------------
left_legal_prf : LT = compare k p_k

我认为这对解决这个特定问题没有太大帮助。

当我声称约束应该成立时,我错了吗?如果是这样,我错过了什么?如果不是,我如何说服编译器?

最佳答案

您可以使用 with ... proof ... 来捕获证明。这是 Idris 2 的测试示例:

filterSquared p (x :: xs) with (p x) proof eq
filterSquared p (x :: xs) | False = filterSquared p xs -- easy
filterSquared p (x :: xs) | True
= rewrite eq in cong (x ::) (filterSquared p xs)

关于pattern-matching - 尽管案例拆分,但 Idris 无法解决约束,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/66840300/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com