什么因素会使一个类型系统一致？
我拿到了András Kovács的DBIndex.hs，这是一个非常简单的依赖类型核心实现。我试图进一步简化它，尽可能地减少代码量，但又不会“破坏”类型系统。经过几次简化后，我得到了一个更小的版本： {-# language LambdaCase, ViewPatterns #-} da...
Lambda演算中布尔值的查询
这是AND运算符的λ演算表示：lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b 有人能帮我理解这个表示吗？
在纯函数式编程语言中，数据（例如字符串、整数、浮点数等）是否也只是函数？
我在思考像 Ruby 这样的纯面向对象语言，其中所有东西，包括数字、整数、浮点数和字符串本身都是对象。纯函数式语言也是这样吗？例如，在 Haskell 中，数字和字符串也是函数吗？ 我知道 Haskell 是基于 λ 演算的，它将所有东西，包括数据和操作，表示为函数。对我来说似乎很合理，一个...
如何找到最佳处理顺序？
我有一个有趣的问题，但我不确定如何准确地表述它... 考虑λ演算。对于给定的λ表达式，存在多种可能的约简顺序。但其中一些不终止，而其他一些则会。 在λ演算中，事实证明有一种特定的约简顺序，如果实际上存在一个不可约解，则此顺序保证始终终止。这被称为正则序。 我写了一个简单的逻辑求解器。但问...
解决函数方程的最先进方法是什么？
假设您想找到一个满足以下方程式的λ演算程序T： (T (λ f x . x)) = (λ a t . a) (T (λ f x . (f x))) = (λ a t . (t a)) (T (λ f x . (f (f x)))) = (λ a b ...
为什么Java Lambda表达式不会引入新的作用域级别？
据我了解，像Haskell这样的语言以及λ演算中，每个λ表达式都有自己的作用域。因此如果我有嵌套的 λ 表达式，例如：\x -> (\x -> x)，那么第一个 \x 参数就不同于第二个 \x。 在Java中，如果这样做会导致编译错误，就像如果在lambda中再次使用x作为参数名...
修改这个简单的reducer，展示不同的评估策略，是否有可能？
我更喜欢通过查看代码来学习，而不是阅读冗长的解释。这可能是我不喜欢长篇学术论文的原因之一。代码明确、简洁、无噪音，如果你不理解某些东西，你可以直接尝试操作它 - 不需要问作者。 这是Lambda演算的完整定义： -- A Lambda Calculus term is a function...
可以证明惰性求值在所有规约策略中具有最小的渐进时间复杂度吗？
当我阅读 Church Rosser II 定理的时候（链接），我想知道是否存在一些加强版的定理，使其不仅表明外最约简会终止，还能告诉我们渐进时间复杂度？或者，是否可以证明按需调用策略在所有约简策略中具有最小的渐进时间复杂度？
SKI演算法和BCKW的实际应用
我能理解如何创建和思考SKI和BCKW演算法，但是我从未能够找到实际的用途。也许我没有深入地去寻找？也就是说，我想知道（请只给一个例子，我并不意味着这是真的）Java Servlets是否广泛使用S而Python生成器是BCW的一个例子，而我只是无法看透森林中的树木？ 我可以理解如何创建和思...
使用PHOAS，是否可以将一个术语评估为正常形式，然后将其转换为字符串？
从this Haskell Cafe的帖子中，借用一些代码示例来自jyp，我们可以在Haskell中构建一个简单的PHOAS评估器，如下所示： {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} import Data.Char data...