[Agda] vector foldl Miller magic?

[Andreas Abel]

[This is a reply to an old post, but the Agda list does not forget...]

Hi Conor,

making implicits explicit, I get

foldl : (S : Set)(T : Nat -> Set) ->
         ((n : Nat) -> T n -> S -> T (suc n)) ->
         T zero ->
         (n : Nat) -> Vec S n -> T n
foldl S T0  f t ._ [] = t
foldl S Tsn f t ._ (cons m s ss) =
   foldl S _1 (\ n -> f _2) (f _3 t s) _4 ss

giving away the solutions

_1 = \ n -> Tsn (suc n)
_2 = suc n
_3 = zero
_4 = m

Agda basically gets stuck on _2, with constraints (after pruning)

_2 m zero    = suc zero
_2 m (suc n) = suc (_2 m n)
_2 m m       = suc m

This is not solvable by Miller, but a heuristics could (after making 
sure that no meta-variable escapes -- but that would require a dead code 
analysis) try

   _2 x y = suc x  (failing)
   _2 x y = suc y  (succeeding)

by linearizing the last equation.

Another path to the goal is to see that the first to equations give a 
complete recursive definition of _2.  A dead code analysis then sees 
that the first argument is unused.  Which allows to prune and solve the 
third equation, and then verify the first two equations.

All not so trivial... ;-)

Cheers,
Andreas


On 07.04.08 4:56 PM, Conor McBride wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/