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

Solution

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

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