[SOLVED] Can I write a dependent left fold in terms of a dependent right fold?

Can I write a dependent left fold in terms of a dependent right fold?

Suppose we have

data Nat = Z | S Nat

type Vec :: Nat -> Type -> Type
data Vec n a where
  Nil :: Vec Z a
  (:::) :: Vec n a -> Vec (S n) a

infixr 4 :::

deriving instance Foldable (Vec n)

The non-dependent (strict) left fold can of course be defined using the non-dependent right fold, in the usual way:

foldlv' :: forall n a b. (b -> a -> b) -> b -> Vec n a -> b
foldlv' f b as = foldr go id as b
  where
    go :: a -> (b -> b) -> b -> b
    go a r !b = r (f b a)

But what about the dependent left fold? Can we define it in terms of the dependent right fold?

Here's the dependent right fold:

dfoldr :: forall n a f. (forall m. a -> f m -> f (S m)) -> f Z -> Vec n a -> f n
dfoldr c n = go where
  go :: Vec m a -> f m
  go Nil = n
  go (x ::: xs) = c x (go xs)

And here's the dependent left fold we want, operationally (stolen from the vec package):

dfoldl' :: forall n a f. (forall m. f m -> a -> f ('S m))-> f 'Z -> Vec n a -> f n
dfoldl' _ !n Nil       = n
dfoldl' c !n (x ::: xs) = unwrapSucc (dfoldl' c' (WrapSucc (c n x)) xs)
  where
    c' :: forall m. WrappedSucc f m -> a -> WrappedSucc f ('S m)
    c' = coerce (c :: f ('S m) -> a -> f ('S ('S m)))

newtype WrappedSucc f n = WrapSucc { unwrapSucc :: f ('S n) }

So far, I haven't been able to figure out a suitable approach myself. Is it possible? I have the feeling I've asked about this before, and that someone showed me a way (possibly in Haskell; possibly in Agda) but I can't work it out. It's possible that I'm thinking of this vaguely related question.

Solution

Here's an Agda version which I think is the simplest; it doesn't rely on subtraction but it does rely on properties of addition.

open import Relation.Binary.PropositionalEquality
  renaming (trans to infixr 5 _◼_; sym to infix 6 _⁻¹; subst to tr)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Vec hiding (foldr; foldl)
open import Function

foldr : {A : Set}(B : ℕ → Set) → (∀ n → A → B n → B (suc n)) → B zero → ∀ {n} → Vec A n → B n
foldr B f b []             = b
foldr B f b (_∷_ {n} a as) = f n a (foldr B f b as)

foldl : {A : Set}(B : ℕ → Set) → (∀ n → B n → A → B (suc n)) → B zero → ∀ {n} → Vec A n → B n
foldl {A} B f b {n} as =
   foldr {A} (λ m → ∀ k → k + m ≡ n → B k → B n)
         (λ m a hyp k p b → hyp (suc k) (+-suc k m ⁻¹ ◼ p) (f k b a))
         (λ k p b → tr B (+-identityʳ k ⁻¹ ◼ p) b)
         as 0 refl b