尽管案例拆分，但 Idris 无法解决约束

如何解决尽管案例拆分，但 Idris 无法解决约束

为了尝试学习 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_prf 填充 left_legal = Refl 孔，声称它无法解决 compare k p_k 和 {{ 之间的约束1}}。尽管只是在 LT 上匹配了模式并发现它是 compare k p_k。显式提供 LT 之类的类型似乎也无济于事。

the (LT = compare @{impl} key p_k) Refl 输出

:t left_legal_prf

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

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

解决方法

您可以使用 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)