小编Yos*_*aka的帖子

我正在阅读Richard Bird撰写的名为"与Haskell一起思考功能"的书,并且遇到了关于无限列表上的归纳的完整链概念.它说:

如果xs0,xs1,...是具有极限xs的部分列表序列,并且P(xsn)对于所有n成立,则P(xs)也成立,则属性P被称为链完成.

作为连锁完整财产的一个例子,它说:

所有方程式e1 = e2,其中e1和e2是涉及普遍量化的自由变量的Haskell表达式,是链完整的.

我很难理解这个例子如何适合链完成的属性.并且它还表明不等式e1 =/= e2不一定是链完整的.我如何从这个链完整性的角度理解这些属性？

顺便说一句,这可能不一定是关于Haskell的问题,而是数学方面的问题.

我尝试了以下代码,但它会生成类型错误.

sa f = f f

• Occurs check: cannot construct the infinite type: t ~ t -> t1
• In the first argument of ‘f’, namely ‘f’
  In the expression: f f
  In an equation for ‘sa’: sa f = f f
• Relevant bindings include
    f :: t -> t1
      (bound at fp-through-lambda-calculus-michaelson.hs:9:4)
    sa :: (t -> t1) -> t1
      (bound at fp-through-lambda-calculus-michaelson.hs:9:1)

Run Code Online (Sandbox Code Playgroud)