我需要实现Haskell的map函数，使其能够与Church列表一起使用。Church列表定义如下： type Churchlist t u = (t->u->u)->u->u 在λ演算中，列表被编码如下： [] := λc. λn. n [1,2,3] := ...

我正在尝试在Haskell中实现Church数，但遇到了一个小问题。当我尝试进行减法时，Haskell会抱怨出现无限类型的错误： 出现检查：无法构造无限类型：t = (t -> t1) -> (t1 -> t2) -> t2 我有99%的把握我的λ演算是正确的（如果...

我正在学习SICP，问题2.6让我陷入困境。在处理Church数字时，将0和1编码为满足某些公理的任意函数的概念似乎是有道理的。此外，使用零的定义和add-1函数导出单个数字的直接公式也是有道理的。但我不明白如何形成加法运算符。 到目前为止，我有这个。 (define zero (lamb...

我正在学习《软件基础》，目前在做关于“Church数”的练习。这里是自然数的类型签名：Definition nat := forall X : Type, (X -> X) -> X -> X. 我已经定义了一个类型为 nat -> nat 的函数 succ。现在我想这...

我正在使用Haskell玩一些lambda演算的东西，具体来说是关于Church数。 我定义了以下内容： let zero = (\f z -> z) let one = (\f z -> f z) let two = (\f z -> f (f z)) let iszer...

具体而言，为什么我们使用foldr来编码列表，使用迭代来编码数字？ 抱歉我的介绍有些冗长，但我不知道如何命名我想要询问的东西，所以我需要先进行一些阐述。这主要参考了C.A.McCann的这篇文章，但它并没有完全满足我的好奇心，同时我也会略显地讲解rank-n-types和无限懒加载的问题。 ...

教堂编码（也称访问者模式）是一种将数据表示为函数的方法：不再使用常规的数据结构，而是使用函数表达数据。 data T = C1 F1 F2 | C2 F3 F4 您可以定义 data T = T (forall r. (F1 -> F2 -> r) -> (F3 -&...

请注意这个程序： {-# LANGUAGE RankNTypes #-} import Prelude hiding (sum) type List h = forall t . (h -> t -> t) -> t -> t sum_ :: (Num a) =...

这是一篇关于Haskell的文章。只需将其保存为“ChurchList.lhs”即可运行。 > {-# LANGUAGE Rank2Types #-} 一个 Church 编码列表是一种通过函数表示列表的方式。它类似于折叠和续传风格。 > newtype ChurchLis...

我一直在尝试在Scala中实现教会编码数据类型。似乎需要使用rank-n类型，因为你需要一个一等的const函数，其类型为forAll a. a -> (forAll b. b -> b)。 然而，我已经成功地这样编码了对： import scalaz._ trait Com...