Haskell中lengthGT4 $ produce id 1归约为True的过程解析

给出代码如下：

lengthGT4 :: List a -> Bool
lengthGT4 (_ :. _ :. _ :. _ :. _ :. _) = True
lengthGT4 (_ :. _) = False    -- 故意这么写的

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

lengthGT4 $ produce id 1

注：$是右结合的语法糖，等价于lengthGT4 (produce id 1)，作用是将右侧表达式作为左侧函数的第一个参数。

问题1解答：归约过程中$何时传参，为什么produce不会无限展开？ #

首先要明确：$只是语法糖，整个表达式等价于lengthGT4 (produce id 1)，不存在“何时传参”的问题——produce id 1从语义上就是lengthGT4的参数。核心在于Haskell的惰性求值+模式匹配驱动求值逻辑：

1. 当lengthGT4要处理参数时，会从上到下尝试自己的模式匹配规则，而模式匹配需要参数足够“具体”才能判断是否匹配。
2. 第一个模式(_ :. _ :. _ :. _ :. _ :. _)要求参数是嵌套了5层:.（Cons构造子）的列表（对应至少5个元素，因为最后一个_可以是任意列表）。因此Haskell会逐步展开produce id 1的结果：
   • 第一次展开：produce id 1 → 1 :. produce id 1，此时只有1层:.，不满足第一个模式；
   • 继续展开尾部的produce id 1，得到1 :. 1 :. produce id 1（2层:.），仍不满足；
   • 重复展开，直到得到5层:.的结构（比如1 :. 1 :. 1 :. 1 :. 1 :. produce id 1），此时参数结构完全匹配第一个模式。
3. 一旦匹配成功，求值立即停止并返回True，不会继续展开produce的剩余部分——这就是produce不会无限展开的原因：惰性求值只计算满足模式匹配所需的最小部分，不需要生成完整的无限列表。

问题2解答：为什么标注“not jump”的表达式不匹配第二个模式，而“here jump out”的表达式匹配第一个模式？ #

核心原因是Haskell的模式匹配是按顺序尝试的，只有当前面的模式完全无法匹配时，才会尝试后面的模式：

1. 对于标注“not jump”的1 :. (produce id 1)：

   • lengthGT4会优先尝试第一个模式，这个模式需要至少5层:.的结构。当前表达式只有1层，但Haskell不会直接判定不匹配——它会尝试展开尾部的produce id 1，看看能不能生成足够的:.结构，而不是直接跳到第二个模式。
   • 只有当展开后发现参数永远无法满足第一个模式（比如传入长度小于5的有限列表），才会触发第二个模式。

2. 对于标注“here jump out”的表达式（实际是展开到5层:.的结构，比如1 :. 1 :. 1 :. 1 :. 1 :. produce id 1）：

   • 此时参数的结构完全匹配第一个模式：最外层是:.，其尾部也是:.，依此类推直到第5层:.，最后一个_可以匹配剩余的produce id 1（不管它是什么）。
   • 匹配成功后立即返回True，不会再尝试第二个模式。

补充：第二个模式(_ :. _)本身能匹配任何非空列表，但因为它排在第一个模式之后，只有当第一个模式完全无法匹配时才会被触发。比如传入长度为3的有限列表，展开后无法满足第一个模式的5层:.要求，才会匹配第二个模式返回False。

内容的提问来源于stack exchange，提问作者zichao liu