wren ng thornton wren at freegeek.org
Mon Jun 7 18:13:25 EDT 2010

```R J wrote:
> Can someone provide a hand calculation of:
>     span (< 0) [-1, -2, -3, 0, 1, 2, -3, -4, -5]?
> I know the result is ([-1, -2, -3], [0, 1, 2, -3, -4, -5]), but the recursion flummoxes me.
> Here's the Prelude definition:

First, let's simplify the definition.

span _ []         = ([], [])
span p xs@(x:xs')
| p x         = (x:ys, zs)
| otherwise   = ([], xs)
where
(ys, zs) = span p xs'

===

span _ []         = ([], [])
span p xs@(x:xs')
| p x         = let (ys, zs) = span p xs' in (x:ys, zs)
| otherwise   = ([], xs)

===

span p xs =
case xs of
[]      -> ([], [])
(x:xs') ->
if   p x
then let (ys, zs) = span p xs' in (x:ys, zs)
else ([], xs)

And finally we can pretty up that recursive call (possibly changing
strictness, but otherwise keeping the same meaning).

span = \p xs ->
case xs of
[]      -> ([], [])
(x:xs') ->
if   p x
then first (x:) (span p xs')
else ([], xs)

And now, the reduction:

span (< 0) (-1:-2:-3:0:1:2:-3:-4:-5:[])

== {delta: unfold the definition of span}
(\ p xs ->
case xs of
[]      -> ([], [])
(x:xs') ->
if   p x
then first (x:) (span p xs')
else ([], xs)) (< 0) (-1:-2:-3:0:1:2:-3:-4:-5:[])

== {beta: reduction of application}
(let p = (< 0) in \ xs ->
case xs of
[]      -> ([], [])
(x:xs') ->
if   p x
then first (x:) (span p xs')
else ([], xs)) (-1:-2:-3:0:1:2:-3:-4:-5:[])

N.B. this next step isn't entirely accurate in Haskell since it looses
sharing.

== {zeta: reduction of let-binding}
(\ xs ->
case xs of
[]      -> ([], [])
(x:xs') ->
if   (< 0) x
then first (x:) (span (< 0) xs')
else ([], xs)) (-1:-2:-3:0:1:2:-3:-4:-5:[])

== {beta, zeta}
case (-1:-2:-3:0:1:2:-3:-4:-5:[]) of
[]      -> ([], [])
(x:xs') ->
if   (< 0) x
then first (x:) (span (< 0) xs')
else ([], (-1:-2:-3:0:1:2:-3:-4:-5:[])))

== {iota: reduction of case matching}
let x   = -1
xs' = (-2:-3:0:1:2:-3:-4:-5:[])
in
if   (< 0) x
then first (x:) (span (< 0) xs')
else ([], (-1:-2:-3:0:1:2:-3:-4:-5:[])))

== {zeta, zeta}
if   (< 0) (-1)
then first (-1:) (span (< 0) (-2:-3:0:1:2:-3:-4:-5:[]))
else ([], (-1:-2:-3:0:1:2:-3:-4:-5:[])))

== {beta}
if   -1 < 0
then first (-1:) (span (< 0) (-2:-3:0:1:2:-3:-4:-5:[]))
else ([], (-1:-2:-3:0:1:2:-3:-4:-5:[])))

Just to be pedantic :)
== {delta}
if   -1 <# 0
then first (-1:) (span (< 0) (-2:-3:0:1:2:-3:-4:-5:[]))
else ([], (-1:-2:-3:0:1:2:-3:-4:-5:[])))

== {primitive}
if   True
then first (-1:) (span (< 0) (-2:-3:0:1:2:-3:-4:-5:[]))
else ([], (-1:-2:-3:0:1:2:-3:-4:-5:[])))

== {iota}
first (-1:) (span (< 0) (-2:-3:0:1:2:-3:-4:-5:[]))

We'll ignore that `first` and evaluate under it for clarity, even though
this isn't accurate for Haskell's call-by-need strategy. Technically
we'd unfold the definition of `first`, do beta/zeta reduction, and then
do the following since we'd need to evaluate the scrutinee of the case
match. I'll go a bit faster now since it's the same.

== {delta, beta, beta, iota, zeta, zeta, beta, delta, primitive, iota}
first (-1:) (first (-2:) (span (< 0) [-3,0,1,2,-3,-4,-5]))

== {delta, beta, beta, iota, zeta, zeta, beta, delta, primitive, iota}
first (-1:) (first (-2:) (first (-3:) (span (< 0) [0,1,2,-3,-4,-5])))

Now things are a little different, so we'll slow down.

== {delta, beta, beta}
first (-1:) (first (-2:) (first (-3:) (
case [0,1,2,-3,-4,-5] of
[]      -> ([], [])
(x:xs') ->
if   (< 0) x
then first (x:) (span (< 0) xs')
else ([], [0,1,2,-3,-4,-5]) )))

== {iota, zeta, zeta, beta}
first (-1:) (first (-2:) (first (-3:) (
if   0 < 0
then first (0:) (span (< 0) [1,2,-3,-4,-5])
else ([], [0,1,2,-3,-4,-5]) )))

== {delta, primitive, iota}
first (-1:) (first (-2:) (first (-3:) ([], [0,1,2,-3,-4,-5])))

Now for those `first`s. Again, with pure call-by-need evaluation we'll
have already done most of this, and will have done it in reverse order.
For clarity we'll do it inside-out a la call-by-value. (Because of
strictness analysis, Haskell could perform a hybrid CBN/CBV strategy and
could actually follow this order if it determined that `first` was
strict in its second argument.)

== {delta}
first (-1:) (first (-2:) (
(\ f p -> case p of (x,y) -> (f x, y))
(-3:) ([], [0,1,2,-3,-4,-5])))

== {beta, zeta}
first (-1:) (first (-2:) (
(\ p -> case p of (x,y) -> ((-3:) x, y))
([], [0,1,2,-3,-4,-5])))

== {beta, zeta}
first (-1:) (first (-2:) (
case ([], [0,1,2,-3,-4,-5]) of (x,y) -> ((-3:) x, y)))

== {iota, zeta, zeta}
first (-1:) (first (-2:)
((-3:) [], [0,1,2,-3,-4,-5]))

Note that since the case match is only head-strict, we don't need to
evaluate that application of (-3:) to []. That'll be done later in the
call to `show` that's implicit on the ghci REPL.

== {delta, beta, zeta, beta, zeta, iota, zeta, zeta, beta}
first (-1:) ((-2:) ((-3:) []), [0,1,2,-3,-4,-5])

== {delta, beta, zeta, beta, zeta, iota, zeta, zeta, beta}
((-1:) ((-2:) ((-3:) [])), [0,1,2,-3,-4,-5])

--
Live well,
~wren
```