我可以用右折叠的依赖左折吗？

Question

我们拥有

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)

非依赖性（严格）左折时，可以使用非依赖性右褶皱来定义：

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)

但是左折呢？我们可以用依赖的右折叠定义它吗？

there是依赖的右折：

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)

这是我们想要的依赖的左折（从

vec

软件包中被盗）：

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

到目前为止，我自己还没有找到合适的方法。是否可以？我以前有过关于这个问题的感觉，有人向我展示了一种方法（可能在Haskell；可能在Agda中），但我无法解决。我可能会想到这个隐约相关的问题。

concontion conconte comply@@@有效的解决方案，拥有一个在操作上等效的解决方案是很不错的：

Answer 1

（在上面的解决方案中，h采取额外的论点，尽管它只从一个呼叫到下一个呼叫被强制强制。）

索引左折的版本很容易根据

ifoldr

降低累加器的索引，而不是增加它：

ifoldl' :: forall a b n. (forall m. b (S m) -> a -> b m) -> b n -> Vec n a -> b Z
ifoldl' f n xs = unIFoldlMotive (ifoldr fm zm xs) n where
    fm :: forall m. a -> IFoldlMotive a b m -> IFoldlMotive a b (S m)
    fm x (IFoldlMotive h) = IFoldlMotive $ \ n -> h $! f n x
    zm = IFoldlMotive $ \z -> z

newtype IFoldlMotive a b n = IFoldlMotive
    { unIFoldlMotive :: b n -> b Z
    }

将其绕开似乎更具挑战性。我只能通过将累加器包裹在GADT中来做到这一点（不幸的是，它不能是newtype），因为它依赖于减法的属性，在下面我已经对其进行了助理；证明它们意味着单身人士对所有内容进行全面的态度并在运行时评估证据（如果天气迅速完成，则需要二次的时间）。

data IFoldl2Motive b n m where
    IFoldl2Motive :: ((m <=? n) ~ True) => b (n - m) -> IFoldl2Motive b n m

ifoldl2' :: forall a b n. (forall m. b m -> a -> b (S m)) -> b Z -> Vec n a -> b n
ifoldl2' f z xs = case ifoldl' fm zm xs of { IFoldl2Motive y -> y } where
    fm :: forall m. IFoldl2Motive b n (S m) -> a -> IFoldl2Motive b n m
    fm (IFoldl2Motive b) x
        | Dict <- lemma1 @n @m
        , Dict <- lemma2 @n @m
        = IFoldl2Motive (f b x)
    zm
        | Dict <- ltRefl @n
        , Dict <- minusRefl @n
        = IFoldl2Motive z

Full代码

{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module B where

import           Data.Kind (Constraint)
import           Data.Coerce
import           Data.Functor.Compose
import           Unsafe.Coerce (unsafeCoerce)

data Nat = Z | S Nat

data Vec n a where
    Nil  :: Vec 'Z a
    Cons :: a -> Vec n a -> Vec ('S n) a

deriving instance Foldable (Vec n)

ifoldr :: forall b n a. (forall m. a -> b m -> b ('S m)) -> b 'Z -> Vec n a -> b n
ifoldr f z = go where
    go :: Vec m a -> b m
    go Nil         = z
    go (Cons x xs) = f x $ go xs
{-# INLINE ifoldr #-}

newtype IFoldlMotive a b n = IFoldlMotive
    { unIFoldlMotive :: b n -> b Z
    }

ifoldl' :: forall a b n. (forall m. b (S m) -> a -> b m) -> b n -> Vec n a -> b Z
ifoldl' f n xs = unIFoldlMotive (ifoldr fm zm xs) n where
    fm :: forall m. a -> IFoldlMotive a b m -> IFoldlMotive a b (S m)
    fm x (IFoldlMotive h) = IFoldlMotive $ \ n -> h $! f n x
    zm = IFoldlMotive $ \z -> z

data IFoldl2Motive b n m where
    IFoldl2Motive :: ((m <=? n) ~ True) => b (n - m) -> IFoldl2Motive b n m

ifoldl2' :: forall a b n. (forall m. b m -> a -> b (S m)) -> b Z -> Vec n a -> b n
ifoldl2' f z xs = case ifoldl' fm zm xs of { IFoldl2Motive y -> y } where
    fm :: forall m. IFoldl2Motive b n (S m) -> a -> IFoldl2Motive b n m
    fm (IFoldl2Motive b) x
        | Dict <- lemma1 @n @m
        , Dict <- lemma2 @n @m
        = IFoldl2Motive (f b x)
    zm
        | Dict <- ltRefl @n
        , Dict <- minusRefl @n
        = IFoldl2Motive z

type family (-) (n :: Nat) (m :: Nat) :: Nat where
    n - Z = n
    S n - S m = n - m

type family (<=?) (n :: Nat) (m :: Nat) :: Bool where
    Z <=? m = True
    S n <=? Z = False
    S n <=? S m = n <=? m

type n <= m = (n <=? m) ~ True

data Dict (c :: Constraint) where
    Dict :: c => Dict c

lemma1 :: forall n m. (S m <= n) => Dict (m <= n)
lemma1 = axiom

lemma2 :: forall n m. (S m <= n) => Dict ((n - m) ~ S (n - S m))
lemma2 = axiom

ltRefl :: forall n. Dict (n <= n)
ltRefl = axiom

minusRefl :: forall n. Dict ((n - n) ~ Z)
minusRefl = axiom

axiom :: forall i j. Dict (i ~ j)
axiom = unsafeCoerce (Dict @(i ~ i))

---