How does one use dfold again?

[peter.t...@gmail.com]

I wanted to make a general version of sequence that puts together any k-vector of monad elements of type a->m a in sequence, recording the output, to give a->m(Vec k a). This works but is uly:

sequenceS :: forall (k::Nat) m a  . (KnownNat k, Monad m) => Vec k (a -> m a) -> a -> m (Vec k a)
sequenceS =   ifoldl (\g i f -> \a -> do a' <- f a; v <- g a'; return (replace i a' v))  (const $ return (repeat undefined))
                       

For those dazzled by the parens, the g is the a->m(Vec k a) function that is being built, the f is the new sequent of type a->m(a) to be incorporated into it as the ifoldl bites off a bit more of the vector of fs. If you number the f as f0,f1,f2, one can imagine writing

                  \a -> do a0 <- f0 a; a1 <- f1 a0; a2 <- f2 a0; ... ; return (a0:>a1:>a2:>...)

and i've put the g for the ifold in bold.

Modulo the index i, the ifoldl has \a -> do a0 <- f0 a; v <- g a0; return (a0:>v) just like the above EXCEPT that I can't write a0:>v because that would make g deliver a vector that changes in size. At the far right it would need to be zero length, then length 1, then length 2, etc. moving left. That's why I had to use an index i and  use ifoldl instead of foldl, and instead of cramming a0 onto the bottom of a short vector v, instead shove it midway into a long vector v that is already and always full size. And I started with a full length vector at right that contains all undefineds. They get replaced one by one by the ifold, in each successive position i and one ends up with a full size vector that is safely populated.

But that's ugly, so I thought I'd try dfold and really do what I set out first above, build up an increasingly long vector to be returned finally via the monad.  In my opinion the proper construction is

sequenceS'  =  dfold (Proxy @(Append k m a))  combi  (const(return (Nil :: Vec 0 a)))
    where combi :: forall l . SNat l -> (a->m a) -> (a->m(Vec l a)) -> (a->m(Vec (l+1) a))
                combi _ f g a = do a' <- f a; v <- g a' ; return (a':>v)

and here I have the thing "combi" that goes inside the fold just as I want to write it, putting a new element on the bottom of and thereby extending a vector for return. The starter element is now a zero length vector, not a full length vector full of undefineds.

I believe I have guessed the Append proxy correctly as

data Append (k :: Nat) (m :: Type->Type) (a :: Type) (f :: TyFun Nat Type) :: Type
type instance Apply (Append k m a) l = a -> m (Vec (l + k) a)

but I admit the description in the manual has me completely fubared. The description of the proxy for dtfold makes sense to me, but not the one for dfold. What is "l"? It's declared as f a "Tyfun Nat Type" (what that?) but it ends up as a Nat, and why am I adding k to it and not just 1? I might guess it is supposed to be a Nat functionally dependent on some hole that is to be filled by a type, but is that type supposed to follow it on the line like an argument? I am totally confused. Am I supposed to be writing k+l not l+k or does it not matter? And doesn't dfold just want a "+1" instance of it, whatever it is, not a "+k"? (or "+l"). So why is there a k or l there at all! Maybe I am supposed to be writing Vec l and no k, or Vec k and no l. I'm guessing that it is maybe supposed to represent the situation k from the left and l from the right ... or maybe not.

Anyway, the above does not work. Functionally, I am sure it should. So it is a type problem. Not surprising given my nonunderstanding of the "Proxy". The error is always nonspecific to a line, 

 error:
    solveSimpleWanteds: too many iterations (limit = 160)
      Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
      Simples = {[WD] $dKnownNat_a1Fej {0}:: KnownNat k0 (CNonCanonical),
                 [WD] $dMonad_a1Fev {0}:: Monad m0 (CNonCanonical),
                 [WD] hole{co_a1FeC} {0}:: (b0 -> a0) ~ Apply p0 0 (CNonCanonical),
                 [WD] hole{co_a1FeD} {0}:: Apply p0 k0
                                           ~ (a -> m (Vec k a)) (CNonCanonical)}
      WC = WC {wc_simple =
                 [WD] hole{co_a50m} {160}:: k ~ 0 (CNonCanonical)
                 [W] hole{co_a1IFy} {160}:: (k + k) ~ k (CNonCanonical)}
 

I would be grateful for what is likely the extremely simple correction required to get out of this misery!

Regards

PTB

[peter.t...@gmail.com]

The answer was to change the proxy type to

  data Append (m :: Type->Type) (a :: Type) (f :: TyFun Nat Type) :: Type
  type instance Apply (Append m a) l = a -> m (Vec l a)

from

  data Append (k :: Nat) (m :: Type->Type) (a :: Type) (f :: TyFun Nat Type) :: Type
  type instance Apply (Append k m a) l = a -> m (Vec (l + k) a)

That  removes the extra k references from the manual's example, which is as follows:

  data Append (k :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type

  type instance Apply (Append k a) l = Vec (l + k) a

 

There is really only an additional type parameter m:Type->Type in my own non-working try at it, with refererence to the manual's example. That and the a->m(- ) wrapper on the result type. I really could not figure the what or why of things in that example! Is that k in it  surplus to working requirements? Is something wrong with the example in the manual? I suppose I should try the manual example exactly to find out ...

[peter.t...@gmail.com]

The manual example is OK, but why I couldn't understand  is now clear (to me). I just record it here.  The example's "Vec(l+m)a" type  proxy sets l and m on an equal footing but in fact, no, the m is an external parameter to an operator on the Vec l a type that changes it to Vec (l+m). It's "higher level" than l. One can see that when one conpares the example's proxy definition with my eventually working definition for my recursion:

data Append (m :: Type->Type) (a :: Type) (f :: TyFun Nat Type) :: Type  -- example              
data Append (m :: Nat)              (a :: Type) (f :: TyFun Nat Type) :: Type   -- me

type instance Apply (Append m a) l = Vec (l + m) a                   -- example
type instance Apply (Append m a) l = a -> m (Vec l a)               -- me

The m is  parameter to the constructor that makes a new type from old, in the one case making Vec (l+m) a from Vec l a, and in the other making a->m(Vec l a) from Vec l a. It's not at the same level as l at all. Mystery over.