==================================
REDUCERON MEMO 2
Widening function bodies revisited
Colin R, 14 November
Discussion added 15 November
==================================

Yesterday, in Memo 1, Matt considered the question of how to achieve wider
function bodies for Reduceron.  The running example was

  data List a = Nil | Cons a (List a)

  rev xs acc =
    case xs of
      Nil -> acc
      Cons x xs -> rev xs (Cons x acc)

which currently gets compiled into the following equations.

  Nil n c       = n                        (1)
  Cons x xs n c = c x xs                   (2)
  rev  v acc    = v acc (rev' acc)         (3)
  rev' acc x xs = rev xs (Cons x acc)      (4)

Matt observes that if lambda-expressions could somehow be supported
then (4) could be in-lined in (3) like this

  rev v acc  = v acc (\x xs -> rev xs (Cons x acc))

but then points to several difficulties in the way of effective
support for lambda including the apparent need for some new
mechanism for dealing with variables such as x and xs.

The troublesome functional expression can be rewritten to avoid the
explicit lambda, by using the standard repertoire of small combinators
such as 'flip' and 'comp'.

    \x xs -> rev xs (Cons x acc)
  = \x xs -> flip rev (Cons x acc) xs
  = \x -> flip rev (Cons x acc)
  = \x -> flip rev (flip Cons acc x)
  = \x -> comp (flip rev) (flip Cons acc) x
  = comp (flip rev) (flip Cons acc)

Flipped constructors are simple enough.  They are no more
expensive than their originals -- but we might hope to eliminate
them anyway.

      snoc = flip Cons
  <=> snoc xs x n c = c x xs

Now define

      ver = flip rev
  <=> ver acc v = rev v acc
  <=> ver acc v = v acc (comp ver (snoc acc))

And

      verSnoc acc = comp ver (snoc acc)
  <=> verSnoc acc x = ver (snoc acc x)
  <=> verSnoc acc x v = ver (snoc acc x) v
  <=> verSnoc acc x v = v (snoc acc x) (comp ver (snoc (snoc acc x)))
  <=> verSnoc acc x v = v (snoc acc x) (verSnoc (snoc acc x))
  <=> verSnoc acc x v = v (Cons x acc) (verSnoc (Cons x acc))

So we obtain

  rev v acc = v acc (verSnoc acc)
  verSnoc acc x v = v (Cons x acc) (verSnoc (Cons x acc))
 
Discussion (added 15 November)
------------------------------

Matt points out another solution to the in-lining problem for
rev: instead of in-lining the rev' alternative "back into" the body
of rev, we can in-line rev at the point of the recursive call in rev'.
We obtain in a single step:

  rev v acc = v acc (rev' acc)
  rev' acc x xs = xs (Cons x acc) (rev' (Cons x acc))

What is more, upto renaming of rev'/verSnoc and xs/v, this is
*the same* solution as the one obtained before by in-lining the
other way followed by the argument-flipping transormations!

More generally, to achieve wider function bodies, here's one
simple rule:

  In-line saturated applications of functions that
  do not have directly recursive definitions.

For *single-level* constructor-case analysis this rule yields
a directly recursive function with a nice fat body for each
recursive alternative.  But what about nested cases, for example
when there is case analysis of more than one argument?  That's
a good question for another day.