Haskell's reducing rule

How does lengthGT4 $ produce id 1 reduced to True in Haskell?

lengthGT4 :: List a -> Bool
lengthGT4 (_ :. _ :. _ :. _ :. _ :. _) = True
lengthGT4 (_ :. _) = False    -- deliberately doing this

produce :: (a -> a) -> a -> List a
produce f i = i :. produce f (f i)

lengthGT4 $ produce id 1

$ puts right-hand statement as left first parameter.

1. On reducing, when $ takes right-hand to left for matching? Why right-hand product doesn't expand infinitely and doesn't prevent $ from taking and matching?
2. Why following not jump doesn't match lengthGT4 (_ :. _) = False and turns out False? While here jump out matchs lengthGT4 (_ :. _ :. _ :. _ :. _ :. _) = True and turns out True?

lengthGT4 $ 1 :. (produce id 1)  -- not jump
lengthGT4 $ 1 :. 1:. (produce id 1)
lengthGT4 $ 1 :. 1:. 1:. (produce id 1)
lengthGT4 $ 1 :. 1:. 1:. 1:. (produce id 1)  -- here jump out

Coming from fp-course https://github.com/Nero5023/fp-course-solution/blob/f95a1a8c1b95dbe63015168f4fe4388854cd4a32/src/Course/List.hs#L280

1. On reducing, when $ takes right-hand to left for matching? Why right-hand product doesn't expand infinitely and doesn't prevent $ from taking and matching?

You can pretend that the $ in the expression e1 $ e2 does not evaluate the expressions e1 and e2 before reducing. Effectively, e1 $ e2 reduces to the function application e1 e2, and that will then evaluate and apply the function e1 to the unevaluated expression e2.

Note that it's the function e1 that decides how much e2 gets evaluated. That's how laziness works. For example, take 3 (1:2:3:4:error "urk") does not evaluate the error, so the program does not crash and evaluates to [1,2,3]. By contrast, take 7 (1:2:3:4:error "urk") does crash.

In your case, produce id 1 is not evaluated by $. Instead, it is evaluated according to lengthGT4, and only as much as needed to match or refute the patterns. Hence, it never gets fully evaluated to an infinite list (which would make the program run forever).

2. Why following not jump doesn't match lengthGT4 (_ :. _) = False and turns out False? While here jump out matchs lengthGT4 (_ :. _ :. _ :. _ :. _ :. _) = True and turns out True?

Patterns are tried in-order, from top to bottom. Effectively, a definition like

f pat1 = exp1
f pat2 = exp2
...

Means, in pseudo-code:

Take the input argument of f.
Evaluate the input as much as needed to match or refute pat1.
if it's a match then
   Bind variables of pat1 to the corresponding values.
   Evaluate exp1 and return the result.
else
   Evaluate the input as much as needed to match or refute pat2.
   if it's a match then
      Bind variables of pat2 to the corresponding values.
      Evaluate exp2 and return the result.
   else
      ...

In your specific case, the pattern in lengthGT4 (_ :. _) = False is not considered until the pattern in lengthGT4 (_ :. _ :. _ :. _ :. _ :. _) = True is refuted. But that is not refuted for that input produce id 1, since it can evaluate to a list with at least 5 elements.