递归类型的嵌套构造函数内的证明

Question

我在使用下面的代码时遇到了一些问题。本质上我想创建一个切片类型。动机来自 Python，其中切片为[start:end:step]，用于从列表中切出子列表。这在概念上与索引序列[start, start+step, start+2*step, ..., end] 相同。

我尝试捕获它的方式是Slice n，可以应用于Vect (n+m) a。基本构造函数FwdS 将创建一个非零步长的切片（proof stepNZ）。 SLen 构造函数将现有切片的Vect 大小要求增加其step（使用stepOf 计算）。同样，SStart 将切片的 Vect 大小要求增加 1。

那么最终的值在概念上对应于：

start := # of SStart in slice
stop  := start + (# of SLen) * step 
step  := constructor argument in FwdS

如果切片是[start:stop:step]。

mutual
  data Slice : Nat -> Type where
    FwdS   : (step : Nat) -> {stepNZ  : Not (step = Z)} -> Slice Z
    SLen   : (x : Slice len) -> Slice (len + (stepOf x))
    SStart : Slice len -> Slice (S len)

  stepOf : Slice n -> Nat
  stepOf (FwdS step)    = step
  stepOf (SLen slice)   = stepOf slice
  stepOf (SStart slice) = stepOf slice

length : Slice n -> Nat
length (FwdS step )   = Z
length (SLen slice)   = let step = stepOf slice
                            len  = length slice
                         in len + step
length (SStart slice) = length slice

select : (slice: Slice n) -> Vect (n+m) a ->  Vect (length slice) a
select (FwdS step) xs           = []
select (SStart slice) (x :: xs) = select slice xs
select (SLen slice) (xs)        = ?trouble

问题在于最后一个模式。我不确定问题出在哪里 - 如果我尝试在 xs 上区分大小写，我会同时得到 [] 和 (_::_) 不可能。理想情况下，我想让这个案例读到这样的内容：

select (SLen slice) (x :: xs) = let rec = drop (stepOf slice) (x::xs)
                                 in x :: (select slice rec)

并让 Idris 认识到，如果第一个参数是 SLen 构造函数，则第二个参数不能是 []。我的直觉是，在SLen 级别，Idris 不明白它已经有证据证明stepOf slice 不是Z。但我不确定如何测试这个想法。

Answer 1

我的直觉是，在 SLen 级别，Idris 不明白它已经有一个 stepOf slice 不是 Z 的证明。

你是对的。使用:t trouble，您会看到编译器没有足够的信息来推断(plus (plus len (stepOf slice)) m) 不是0。

  a : Type
  m : Nat
  len : Nat
  slice : Slice len
  xs : Vect (plus (plus len (stepOf slice)) m) a
--------------------------------------
trouble : Vect (plus (length slice) (stepOf slice)) a

你必须解决两个问题：证明 stepOf slice 是 S k 对于某些 k 像 getPrf : (x : Slice n) -> (k ** stepOf x = (S k))，然后将 Vect (plus (plus len (stepOf slice)) m) a 重写为 Vect (S (plus k (plus len m))) a 这样编译器至少可以知道这个xs 不为空。但它并没有从那里变得更容易。 :-)

基本上，只要您有一个在参数中使用函数的函数，您可能可以将这些信息重写为类型。比如select 和length slice 或SLen 和stepOf x。这是一个示例实现：

data Slice : (start : Nat) -> (len : Nat) -> (step : Nat) -> (cnt : Nat) -> Type where
  FwdS : (step : Nat) -> Slice Z Z step Z
  SLen : Slice Z len step cnt -> Slice Z (S step + len) step (S cnt)
  SStart : Slice start len step cnt -> Slice (S start) len step cnt

您从中受益良多：您可以直接访问参数len 和step，而无需先证明函数length 和stepOf。您还可以更好地控制允许的数据。例如，在您的定义中，SLen $ SStart $ SLen $ SStart $ FwdS 3 将是有效的，混合步骤和开始增量。

select 可能如下所示：

select : Slice start len step cnt -> Vect (start + len + m) a -> Vect cnt a
select (FwdS k) xs = []
select (SStart s) (x :: xs) = select s xs
select (SLen s) [] impossible
select (SLen s {step} {len} {cnt}) (x::xs) {m} {a} =
  let is = replace (sym $ plusAssociative step len m) xs {P=\t => Vect t a} in
  (x :: select s (drop step is))

如果你想要一个带证明的练习，你可以尝试实现select : Slice start len step cnt -> Vect (len + start + m) a -> Vect cnt a，所以切换start + len。

并以 4 步从 1 开始获取两个元素：

> select (SStart $ SLen $ SLen $ FwdS 3) [0,1,2,3,4,5,6,7,8,9]
[1, 5] : Vect 2 Integer