Comment énumérer les éléments d'une liste par `Fin`s en temps linéaire?

Question

Nous pouvons énumérer les éléments d'une liste comme ceci:

-- 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 

Par ex enumerate-ℕ (1 ∷ 3 ∷ 2 ∷ 5 ∷ []) est incroyablement similaire à (0 , 1) ∷ (1 , 3) ∷ (2 , 2) ∷ (3 , 5) ∷ []. En supposant qu'il y ait un partage dans Agda, la fonction est linéaire.

Cependant, si nous essayons d'énumérer les éléments d'une liste par Fin s plutôt que ℕ s, la fonction devient quadratique:

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) 

Est-il possible d'énumérer par Fin s dans le temps linéaire?

Answer 1

Considérez ceci comme une première tentative:

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 pousse à chaque appel récursif comme il se doit, mais il y a un décalage:

le type de l'objectif est List (Fin (.m + suc (length xs)) × .A)

la type de l'expression insise le trou est List (Fin (suc (.m + length xs)) × .A)

Il est facile de prouver que deux types sont eq ual, mais c'est aussi sale. C'est un problème commun: un argument croît et l'autre diminue, donc nous avons besoin de _+_ commutatif pour gérer les deux cas, mais il n'y a aucun moyen de le définir. La solution consiste à utiliser 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) est la même chose que k (length (x ∷ xs)), d'où le décalage est fixe, mais ce qui est i maintenant? Le type du trou est Fin (k (suc (length xs))) et il est inhabitée dans le contexte actuel, alors Introduisons certains habitant:

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 

Le type du nouveau trou est {n : ℕ} → Fin (k (suc (suc n))). Nous pouvons le remplir avec i, mais i doit croître à chaque appel récursif. Cependant suc et k ne commutent pas, donc suc i est Fin (suc (k (suc (_n_65 k i x xs)))). Nous ajoutons donc un autre argument selon lequel suc s sous k, et la définition finale est

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 

qui fonctionne, car s : {n : ℕ} → Fin (k n) → Fin (k (suc n)) peuvent être traités comme {n : ℕ} → Fin (k (suc n)) → Fin (k (suc (suc n))).

Un test: C-c C-nenumerate-Fin (1 ∷ 3 ∷ 2 ∷ 5 ∷ []) donne

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

---

noter maintenant que enumerate-Fink suit toujours Fin dans les types. Par conséquent, nous pouvons abstraite Fin ∘ k et obtenir une version générique de la fonction qui fonctionne avec les ℕ et 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