我一直在尝试在 F# 中实现教堂数字。他们在大学的一门课程中被简要介绍过，从那以后我可能已经陷入了困境。我有工作的前任、继任者、添加和操作，但我不能让减法工作。我正在尝试执行多次应用前任的减法 b。我发现奇怪的是，我的代码中的倒数第二行有效，但我认为等效的最后一行无效。存在类型不匹配。

我对 F# 很陌生，因此我们将不胜感激。谢谢你。

这是给出的类型不匹配错误（Intellisense 说这是代码最后一行的 cPred 错误）。我可以看到输出类型被推断错误。有没有办法修复它，或者我编写这个实现的方式有什么根本错误？

我试图了解在正常订单减少之后执行以下减少的正确步骤。我不明白在这个表达式中我应该执行减少的正确顺序是什么，以及为什么：

你能帮帮我吗？

注意：这个减少也可以看作是函数的后继

应用于教会数字 1

知道数字零表示为：

各种优化问题，例如这个问题，导致 Church 编码列表作为一种启用流融合的方式，即编译器消除中间结果（例如列表）。这是在优化问题中成功使用的定义：

以下是我对 Church-somethings 的看法：与其问“某事”是什么，不如问它能为你做什么。对于列表，答案是：列表可以折叠。为了折叠，我需要一个 type 的“更新”函数b->a->b和一个 type 的起始值b。然后我会把折叠的结果返回给你，它的类型是b. 因此定义ListL。以下是对 的一些基本操作ListL：

这里还有更多：

iterUntil迭代一个函数a->a，从某个类型的值开始a，直到a->bool满足谓词。像 Prelude 这样的函数iterate是不可能的——至少我不知道如何定义它，它必须是某种递归。

继续举例，length只是sum在 a 中选择正确的“更新”函数和起始值的练习foldl：

现在，让我们试试headL：

无论提供什么开始，都应该返回b第一个。需要 a ，但我们没有。这是一个奇怪的问题：基本上我们想告诉编译器：你不需要，相信我...另一方面， A 很容易构造。一个in place of the hole不起作用，因为它总是被调用 - 懒惰似乎并没有解决这个问题。所以，我被困住了。因此这里是abuild lbbheadL' :: ListL a -> ListL aerror "empty list!"_headL

问题一：如何headL实施？

第二个问题出现在尝试实现repeatM :: Monad m => m a -> m [a]. 与 一样iterUntil，需要谓词a->Bool来停止迭代：

目的很明确：重复一个单子动作m a，直到a->Bool满足为止。想法当然是ListL a马上把它折叠起来，实现流融合（list fusion）。例如：

这个例子是相当做作的，它打印出在找到第一个数字 >42 之前所花费的抽奖次数。m例如，在更现实的环境中，monad是ST s包装了一些 FFI 的 monad。关键是：这应该有效地运行。我完全被这个卡住了。我如何纠缠(>>=) :: m a -> (a->m b) -> m b与build得到一个m (ListL a)？即这是

问题2：如何iterUntilM实施？

除了作为一个很好的学习练习之外，这真的是一个好主意吗？

这是之后的顺序问题

Monoidal List的功能链如何存储数据？

和

从没有数组的函数链中提取数据

在这里，我想对我的问题的贡献者表示尊重和感谢，特别是@Aadit M Shah 和@user633183

现在，这个问题被打开以澄清差异列表和教会列表之间的异同或关系

.

差异列表

https://stackoverflow.com/a/51320041/6440264

差异列表是一个函数，它接受一个列表并将另一个列表添加到它前面。例如：

差异列表很酷的一点是它们形成了一个幺半群，因为它们只是内函数：

更好的是，您可以将它们打包成一个简洁的小类，其中函数组合是点运算符：

您可以使用该apply方法检索DList如下的值：

与常规列表（功能列表，而不是 JavaScript 数组）相比，使用差异列表的一个优点是串联效率更高，因为列表是从右到左串联的。因此，如果您连接多个列表，它不会一遍又一遍地复制相同的值。

教会编码列表

作为使用 Church 对进行编码的替代方案，可以通过使用右折叠函数对其进行识别来对列表进行编码。例如，一个包含三个元素 x、y 和 z 的列表可以由一个高阶函数编码，该函数在应用于组合子 c 和值 n 时返回 cx (cy (czn))。

https://stackoverflow.com/a/51420884/6440264

user633183 的解决方案非常出色。它使用Church 编码的列表使用右折叠来减轻对延续的需求，从而使代码更简单且易于理解。这是她的解决方案，修改后foldr看起来像foldl：

这g是迄今为止积累的 Church 编码列表。最初，它是空列表。g跟注从右边弃牌。但是，我们也从右侧构建列表。因此，由于我们编写它的方式，似乎我们正在构建列表并从左侧折叠它。

如果所有这些功能都让您感到困惑，那么 user633183 真正在做的是：

如您所见，她正在向后构建列表，然后使用reduceRight向后折叠向后列表。因此，看起来您正在向前构建和折叠列表。

我喜欢在差异列表中看到的是

1. 这似乎是自然而直接的理解。
2. 通过连接（展平），它形成幺半群
3. 标识元素是标识函数，不需要提供外部初始值。

我不喜欢什么

1. 至少，提供的示例代码依赖于 JavaScript Array

事实上，我喜欢/不喜欢教堂列表的内容与上述内容相反。

我喜欢

1. 它独立于 JavaScript Array 实现，它可以自己定义操作：user633183's solution

我不喜欢

1. 不知道为什么一定不是左折而是右折？

可以通过使用右折叠函数识别列表来对列表进行编码

2. 不清楚与 Monoids 的关系

3. 特别是，Nil 不是标识元素（= 标识函数），示例代码需要提供外部初始值。

所以，我很好奇的是有没有像 Church-list 这样的 Diffrence 列表的形式化。

规格是

• 基本上，这是一个差异列表

• JavaScipt Array 实现的独立性

• 初始值是内置的标识函数。

谢谢你。

在这里，我测试 TypeScript3.0unkown类型。

https://blogs.msdn.microsoft.com/typescript/2018/07/12/announcing-typescript-3-0-rc/#the-unknown-type

TypeScript 3.0 引入了一种新的类型unknown，它就是这样做的。很像any，任何值都可以分配给unknown; 但是，与 不同any的是，您不能访问类型为 的值的任何属性unknown，也不能调用/构造它们。此外， type 的值unknown只能分配给unknownor any。

我玩了一些Church 编码的东西，并测试unknown了函数的每个参数的类型，我有一个错误如下：

错误：

以防万一，这在 vanilla JS 中经过了很好的测试，但我只是想知道如何在不使用 type.js 的情况下解决这个错误any。

谢谢。

使用函数，我们可以从任何类型中抽象出来。下面以Option类型为例：

现在我想对延迟类型进行编码以在 Javascript 中获得惰性效果。但我不知道正确的方法，以及这种努力是否对 Church Encoding 有意义。这是我的第一个镜头：

我在这里完全处于黑暗之中。这种方法会导致任何有意义的事情吗？

函数编码类型（即嵌套柯里化函数）在 Javascript 中有一些缺点：

• 它们在开发控制台中的表示是模糊的（例如[Some(5), None]显示为[f, f]）
• 没有什么能阻止您将组合器应用于错误的类型（例如eitherMap(f) (Some(5))）
• 你不能检查他们的自由变量
• 你甚至不能躲避打字

这些缺点使它们在现实世界的应用中毫无用处。

我想知道是否有办法克服这些缺点并想出了以下草图：

请注意，我对原型继承根本不感兴趣。

这种方法既乏味又可能很慢，因为我应用了Function构造函数，这使得代码更难预测。有没有更好的方法给 curried 函数一个类型（或者更确切地说是 JS 中的标签），以便消除列出的缺点？

我之前提出了一个问题，但我认为这个问题的形式化不好，所以......我在这个特定的定义中遇到了一些问题，以证明它们的属性：

我有一个列表的定义：

这就是定义：

z_next_list_coorres 实际上是一个引理，我需要在另一个理论中证明一个目标（v'_list x = (list_correspodence x)）。

我一直在尝试使用一些有限的范围来证明 list_correspodence 并且效果很好，似乎定义是相等的，但对于 coq 却不是。

以下代码旨在将布尔值的 Church 编码打印为 Haskell's Bool：

这导致了这个错误：

如何让它发挥作用？

在 Coq 中，我可以为长度为 n 的列表定义 Church 编码：

Haskell 的类型系统（包括它的扩展）是否足够强大以适应这样的定义？如果是，如何？