[Agda] vector foldl Miller magic?

[Conor McBride]

Dear Agdans

I was giving a lecture this afternoon in which a
student suggested that writing foldl for vectors
might prove an interesting challenge. Indeed it
was. If you want to have a go yourself, don't
scroll down too soon...

10

9

8

7

6

5

4

3

2

1

0

Here's one way:

data Nat : Set where
   zero  : Nat
   suc   : Nat -> Nat

data _^_ (X : Set) : Nat -> Set where
   [] : X ^ zero
   _::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n

foldl : {S : Set}{T : Nat -> Set} ->
         ({n : Nat} -> T n -> S -> T (suc n)) ->
         T zero ->
         {n : Nat} -> S ^ n -> T n
foldl {T = T0} f t [] = t
foldl {T = Tsn} f t (s :: ss) =
   foldl {T = \ n -> Tsn (suc n)} f (f t s) ss

Now, if you think about what's going on here,
you should just take a moment to be impressed
that f is acceptable as the relevant argument
to the recursive call. That's a nice piece of
higher-order implicit syntax.

Maybe I'm getting my calculations wrong, but
I was hoping that Agda might do even better.
By my reckoning, the constraints on T in the
recursive call are (before lambda-lifting)

  * from argument (f t s),
      T zero = Tsn (suc zero)
  * from the type pushed in,
      T n = Tsn (suc n)

Is that so? It's hard to tell.

The former is suggestive, but does not
determine T; but the latter does, doesn't it?

Should we hope that foldl works even without
the extra hinting. Hang on a minute or
twelve... nope, Epigram 1 doesn't get it
either. How annoying!

I'm not sure I see what the problem is
exactly, but it looks like Agda infers T, but
then can't see why the call to f is ok. Maybe
it's a question of the order of constraints.

So, is there really a problem here? Or is
there an oppportunity?

All the best

Conor