如何在线性时间内通过`Fin`枚举列表的元素？

Question

我们可以枚举列表的元素,如下所示:

-- enumerate-? = zip [0..]
enumerate-? : ? {?} {A : Set ?} -> List A -> List (? × A)
enumerate-? = go 0 where
  go : ? {?} {A : Set ?} -> ? -> List A -> List (? × A)
  go n  []      = []
  go n (x ? xs) = (n , x) ? go (?.suc n) xs

Eg enumerate-? (1 ? 3 ? 2 ? 5 ? [])等于(0 , 1) ? (1 , 3) ? (2 , 2) ? (3 , 5) ? [].假设在Agda中有共享,则函数是线性的.

但是,如果我们尝试用Fins而不是?s 枚举列表的元素,则该函数变为二次方:

enumerate-Fin : ? {?} {A : Set ?} -> (xs : List A) -> List (Fin (length xs) × A)
enumerate-Fin  []      = []
enumerate-Fin (x ? xs) = (zero , x) ? map (pmap suc id) (enumerate-Fin xs)

是否有可能Fin在线性时间内用s 枚举？

Answer 1

将此视为首次尝试:

go : ? {m ?} {A : Set ?} -> Fin m -> (xs : List A) -> List (Fin (m + length xs) × A)
go i  []      = []
go i (x ? xs) = (inject+ _ i , x) ? {!go (suc i) xs!}

i 在每次递归调用时都会增长,但是存在不匹配:

目标的类型是 List (Fin (.m + suc (length xs)) × .A)

洞的表达类型是什么 List (Fin (suc (.m + length xs)) × .A)

很容易证明两种类型是相同的,但它也很脏.这是一个常见的问题:一个参数增长而另一个参数降低,因此我们需要定义上可交换_+_来处理这两种情况,但是没有办法定义它.解决方案是使用CPS:

go : ? {?} {A : Set ?} -> (k : ? -> ?) -> (xs : List A) -> List (Fin (k (length xs)) × A)
go k  []      = []
go k (x ? xs) = ({!!} , x) ? go (k ? suc) xs

(k ? suc) (length xs)是一回事k (length (x ? xs)),因此不匹配是固定的,但现在是i什么？洞的类型是,Fin (k (suc (length xs)))并且它在当前环境中无人居住,所以让我们介绍一些居民:

go : ? {?} {A : Set ?}
   -> (k : ? -> ?)
   -> (? {n} -> Fin (k (suc n)))
   -> (xs : List A)
   -> List (Fin (k (length xs)) × A)
go k i  []      = []
go k i (x ? xs) = (i , x) ? go (k ? suc) {!!} xs

新洞的类型是{n : ?} ? Fin (k (suc (suc n))).我们可以填写它i,但i必须在每次递归调用时增长.不过suc和k不上班,所以suc i是Fin (suc (k (suc (_n_65 k i x xs)))).所以我们在sucs下添加另一个参数,k最终的定义是

enumerate-Fin : ? {?} {A : Set ?} -> (xs : List A) -> List (Fin (length xs) × A)
enumerate-Fin = go id suc zero where
  go : ? {?} {A : Set ?}
     -> (k : ? -> ?)
     -> (? {n} -> Fin (k n) -> Fin (k (suc n)))
     -> (? {n} -> Fin (k (suc n)))
     -> (xs : List A)
     -> List (Fin (k (length xs)) × A)
  go k s i  []      = []
  go k s i (x ? xs) = (i , x) ? go (k ? suc) s (s i) xs

哪个有效,因为s : {n : ?} ? Fin (k n) ? Fin (k (suc n))可以视为{n : ?} ? Fin (k (suc n)) ? Fin (k (suc (suc n))).

测试:C-c C-n enumerate-Fin (1 ? 3 ? 2 ? 5 ? [])给出

(zero , 1) ?
(suc zero , 3) ?
(suc (suc zero) , 2) ? (suc (suc (suc zero)) , 5) ? []

现在请注意,在类型中enumerate-Fin k始终如下Fin.因此,我们可以抽象Fin ? k并获得与工作两者的功能的通用版本?和Fin:

genumerate : ? {? ?} {A : Set ?}
           -> (B : ? -> Set ?)
           -> (? {n} -> B n -> B (suc n))
           -> (? {n} -> B (suc n))
           -> (xs : List A)
           -> List (B (length xs) × A)
genumerate B s i  []      = []
genumerate B s i (x ? xs) = (i , x) ? genumerate (B ? suc) s (s i) xs

enumerate-? : ? {?} {A : Set ?} -> List A -> List (? × A)
enumerate-? = genumerate _ suc 0

enumerate-Fin : ? {?} {A : Set ?} -> (xs : List A) -> List (Fin (length xs) × A)
enumerate-Fin = genumerate Fin suc zero