What are the redexes in this Haskell expression?

Question

I am learning Haskell for a university course and i have a question about reducible expressions (redexes). I understand the concept yet I still have some questions that I can't seem to figure out on my own.

Lets say you would want to find all the reducible expressions in an expression, like this:

head (map (+1) (3:repeat 3))

In this expression an obvious redex would be map (+1) (3:repeat 3)) because it matches to the definition of map, so Haskell would "reduce" the expression and map would increment the 3 and 4:map (+1) (repeat 3). would be reduced next.

The question I have is:

Is head (map (+1) (3:repeat 3)) already a redex, before map is evaluated?

Because the "input" of head does not match the constructor of a list (which is what head is looking for), I am confused about whether it still is a redex because logically it can't get reduced yet, but the definitions online seem to be saying that it would be.

Answer 1

Haskell's evaluation is lazy: it proceeds by topmost leftmost redex strategy (at least conceptually): it reduces the leftmost among the topmost redexes.

Presumably head is defined as

head xs = case xs of (x:_) -> x

so then its application to whatever expression is indeed a redex -- an expression in need of reducing. Which proceeds according to the definition of head,

head (map (+1) (3:repeat 3))
=
case (map (+1) (3:repeat 3)) of (x:_) -> x
=

(or we could say that head itself is the topmost leftmost redex, which reduces to its definition, first; and if we'd written the above as ((\xs -> case xs of (x:_) -> x) (map (+1) (3:repeat 3))) we'd get to the same outcome, just a bit more tediously).

A primary forcing primitive is case. Now it needs to perform the pattern match, so it must find out the value of its scrutinee expression (only to the extent that the pattern match becomes possible). To do that it must now work according to the definition of map which is presumably

map f xs = case xs of { (x:ys) -> f x : map f ys
                      ; [] -> [] }

so it becomes

case (map (+1) (3:repeat 3)) of (x:_) -> x
=
case (case (3:repeat 3) of 
         { (x:ys      ) -> (+1) x : map (+1) ys
                   ; [] -> [] } )
                             of (x:_) -> x
=

At this point the inner case expression can be reduced,

case (let { x=3 ; ys=repeat 3} in 
        (+1) x : map (+1) ys )
  of (x        : _                  ) -> x
=

and now the outer case's pattern matching becomes possible,

case (let { x=3 } in 
        (+1) x               )
  of (x                             ) -> x
=
      let { x=3 } in 
        (+1) x 
=
        (+1) 3 
=
        4