Idris - 向量队列和重写规则

Question

我正在尝试在 Idris 中实现类似功能队列的东西，但它携带类型中的元素数量 - 例如 Queue ty n m (n+m) 其中n 是一个 Vect n ty、@987654325 中的元素数量@ 是第二个Vect m ty 中的元素，(n+m) 是总元素。

问题是，在将这些大小作为隐式参数进行操作时，我遇到了应用重写规则的问题：

module Queue

import Data.Vect as V

data Queue : Type -> Nat -> Nat -> Nat -> Type where
    mkQueue : (front : V.Vect n ty)
           -> (back : V.Vect m ty)
           -> Queue ty n m (n + m)

%name Queue queue

top : Queue ty n m (S k) -> ty
top {n = S j} {m} {k = j + m} (mkQueue front back) =
    V.head front
top {n = Z} {m = S j} {k = j} (mkQueue front back) =
    V.head $ V.reverse back

bottom : Queue ty n m (S k) -> ty
bottom {m = S j} {n} {k = n + j} (mkQueue front back) = 
    ?some_rewrite_1 (V.head back)
bottom {m = Z} {n = S j} {k = j} (mkQueue front back) = 
    ?some_rewrite_2 (V.head $ V.reverse front)

top 有效，但 bottom 无效。看来我需要以某种方式提供plusZeroRightNeutral 和plusRightSuccRight 重写，但我不确定将它们放在哪里，或者是否有其他选择。以下是错误消息：

bottom 第一行出错：

         Type mismatch between
                 Queue ty n (S j) (n + S j) (Type of mkQueue front back)
         and
                 Queue ty n (S j) (S (n + j)) (Expected type)

         Specifically:
                 Type mismatch between
                         plus n (S j)
                 and
                         S (n + j)

bottom第二行出错：

         Type mismatch between
                 Queue ty (S j) 0 (S j + 0) (Type of mkQueue front back)
         and
                 Queue ty (S j) 0 (S j) (Expected type)

         Specifically:
                 Type mismatch between
                         plus (S j) 0
                 and
                         S j

单个尺寸告诉我何时需要旋转两个Vects，而整体尺寸告诉我何时我有一个空的和非空的Queue，所以我确实想跟踪所有信息，如果可能。

Answer 1

解决此问题的一种可能方法是同时破坏n。这次伊德里斯明白最后一个参数不为零，这基本上是在抱怨：

total
bottom : Queue ty n m (S k) -> ty
bottom {m = S m} {n = S n} (MkQueue _ back) = V.head back
bottom {m = S m} {n = Z}   (MkQueue _ back) = V.head back
bottom {m = Z}   {n = S n} (MkQueue front _) = V.head $ V.reverse front
bottom {m = Z}   {n = Z}   (MkQueue _ _) impossible

作为旁注，我建议将 top 函数设为总计：

total
top : Queue ty n m (S k) -> ty
top {n = S n}           (MkQueue front _) = V.head front
top {n = Z}   {m = S m} (MkQueue _ back) = V.head $ V.reverse back
top {n = Z}   {m = Z}   (MkQueue _ _) impossible