问题标签 [typed-lambda-calculus]

System F是在编写原型时简单地推理类型的好方法。除了自己实现之外，我还想使用现有的实现。

在寻找实现时，似乎没有任何实现——我不知道为什么。

我的问题是：系统 F 的规范实现是什么？

我需要说明术语的类型

并使用证明树证明它。我相当确定这是将 2 作为 的输入x，然后将 2 与 1 进行比较并返回 a boolean。这意味着术语的类型是int → boolean。我只是不确定如何为其编写证明树。如果有人可以向我指出一些示例或解释如何解决类似的问题，那就太好了。

最近开始了一个关于简单类型 lambda 演算的大学模块，对于任何给定的示例，它只是 (t1->t2) 或类似的，我从未使用过这么长的类型字符串。问题是定义一个术语，使用尽可能短的定义，类型为 (t1→t3)→(t2→t3→t5)→t2→t1→t7。我如何开始这个，我可以把它分解成更小的类型还是我必须把它作为一个长类型来完成。

有没有一种明确的方法可以在 lambda 演算中找到术语？例如假设我们有一个pair构造函数

pair = λa. λb. λf. f a b

我们有fst构造函数

fst = λp. p (λa. λb. a)

返回对的第一个元素，我们现在必须定义snd返回对的第二项的构造函数。我已经到了这样定义它

snd = λp. p (λa. λb. b)与snd (pair a b) = b.

snd 也可以定义为

snd = λp. p (λb. λa. b),

问题是，有没有明确的方法来定义新的构造函数？

当我必须定义构造函数时，人们应该如何思考，当我被要求定义新的构造函数时，我如何测试我的答案是否正确。

谁能解释类型检查和类型推断问题之间的区别？

我试图寻找差异，但我找不到任何令人信服的来源可以清楚地解释差异。如果可能的话，也包括例子。

如何在（纯）构造演算中定义递归函数？我在那里看不到任何定点组合器。

我想使用 Agda 作为我的类型检查器和评估器来测试系统 F 中的一些定义。

我第一次尝试介绍 Church 自然数是通过写作

这将像常规类型别名一样使用：

然而，定义Num不输入（种类？）检查。使其工作并尽可能接近系统 F 表示法的最合适方法是什么？

作为背景，我正在浏览“Flock of Functions”并尽我所能将这些 Javascript 示例转换为类型化的 Typescript。请参阅https://github.com/glebec/lambda-talk/blob/master/src/index.js#L152以供参考。True 函数返回第一个 curried 参数，并忽略第二个。

考虑以下 Typescript 代码：

假设我想保留“显式函数返回类型”规则，我如何摆脱 ESLint 禁用注释？换句话说，我想正确键入 True 函数。

我的编辑告诉我问题(_els) => thn出在代码部分。它需要以某种方式输入。

]

我可以做些什么来设置返回类型或以其他方式正确输入这个东西，这样我就不需要禁用 ESLint 规则？

我不明白repeat (j l h)下面关于渐进类型lambda演算的论文中的代码片段是什么意思，算法是快速排序，也许知道算法的人可以猜到语法定义：

编辑：根据我目前的理解，算法有错误，应该是：[i: (Ref Int) (box (- l 1))]，即h应该是l。

论文链接：https ://dl.acm.org/doi/10.1145/3314221.3314627#sec-supp

他们的 Grift 编译器的源代码是用编写的，.rkt所以我希望如果有人知道 Racket 可以提供帮助，这里定义了重复语法：https ://github.com/Gradual-Typing/Grift/blob/95c56d94b38e9b33adf7a662c6d7768430d977da/src/language/语法.rkt#L126

我是函数式编程/Racket/GTLC+ 的新手，抱歉，我已尽力描述我的问题...

我正在学习简单类型的 Lambda 微积分，但我对这些方程感到困惑。

我想知道它们叫什么以及它们是如何工作的。

谢谢你的帮助！

（图片取自https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html）