在OCaml中使用GADTs构建简单的lambda演算DSL
如何使用GADTs在OCaml中定义类似于简单lambda演算的DSL？具体而言，我无法弄清楚如何正确地定义类型检查器，以将未打标签的AST转换为已打标签的AST，也无法弄清楚上下文和环境的正确类型。 以下是使用传统方法在OCaml中实现简单lambda演算语言的一些代码。 (* Here...
只使用增量、循环、赋值和零实现减法操作
我正在尝试仅使用以下函数构建减法、加法、除法、乘法和其他操作： incr(x) - 一旦调用此函数，它将把 x + 1 赋值给 x assign(x, y) - 此函数将 y 的值分配给 x（x = y） zero(x) - 此函数将 0 分配给 x（x = 0） loop X { } -...
Hindley-Milner类型系统中letrec的正确形式是什么？
我有困难理解维基百科上提供的HM系统的letrec定义，链接在这里：https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions 对我来说，该规则大致转化为以下算法: 对let...
底部类型是什么？
在维基百科中，底部类型被简单地定义为“没有值的类型”。然而，如果 b 是这种空类型，那么乘积类型 (b,b) 也没有值，但似乎与 b 不同。我认为底部是不可居住的，但我认为这个属性不足以定义它。 通过Curry-Howard对应，底部与数学谬误相关联。现在有一个逻辑原则，即从 False 推...
Lambda演算如何实现加法？
我一直在阅读关于λ演算的内容，并且喜欢其中提出的思想，但有些问题我无法解释； λ演算怎样处理加法？ 我知道(\x . + x x) 3 这与3 + 3相同，即6，但是加法函数最初是如何实现的呢？ 这是编译器/语言必须内置的内容吗，还是仅可以由λ演算定义？
如何在JavaScript中正确地柯里化函数？
我在JavaScript中编写了一个简单的curry函数，它对大多数情况都能正确地工作： const curry = (f, ...a) => a.length < f.length ? (...b) => curry(f, ...a, ...b) : ...
寻找一个使用 Church 编码（λ演算）来定义 <、> 和 != 的方法。
我需要创建一些Lambda函数来处理 >, < 和 !=，但我不知道该如何操作，是否有人能帮助我？PS：我们刚开始学习Lambda演算，请不要假设任何先前的知识。谢谢提前！ 编辑 - 我的意思是使用lambda演算实现Lambda演算中的算术运算 编辑2 - 更准确地说：寻找一个C...
Haskell去糖化的策略
我正在开发一款纯函数编程的虚拟机，希望能够测试和使用已经存在的各种Haskell模块。该虚拟机的输入基本上是未类型化的 lambda 演算表达式。我想知道从现代 Haskell 模块（例如，使用 MPTC、模式守卫等）中提取这种表达式的好方法。我做了一些研究，似乎没有现成的工具可以做到这一点（...
任何函数都可以转化为无点形式吗？
许多函数可以简化为无参数形式，但是否所有函数都可以这样做呢？ 例如，我不知道如何对以下函数进行简化：apply2 f x = f x x
什么是在System-F中无法用Hindley Milner表达的类型和/或术语？
我记得在某个地方读到过，Hindley Milner 是对 system-f 的限制。如果是这样，请问能否提供一些可以在 system-f 中输入但无法在 HM 中输入的术语。