================================== 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.