键入强制执行的“严格/命令”子集/Haskell 版本答案

【问题标题】：Type enforced "strict/imperitive" subset/version of Haskell键入强制执行的“严格/命令”子集/Haskell 版本
【发布时间】：2013-04-19 03:59:40
【问题描述】：

我非常喜欢 Haskell，但我担心 Haskell 的主要问题之一是难以推理空间使用情况。基本上，thunk 和递归的可能性似乎会造成一些棘手的情况，似乎必须通过添加正确的严格性来非常小心，以免程序在特定输入上耗尽内存。

我喜欢 C/C++ 的一点是，我可以很快确定程序空间使用的上限，尤其是在避免递归的情况下。变量一目了然。

我想知道是否有一种方法可以创建 Haskell 的类型安全“命令式”子集，它没有 thunk，并且是严格的。

我了解Data.STRef 提供了可变单元格，但据我了解，这些单元格本身仍然很懒惰并且可以包含 thunk。我正在考虑强制此类单元格中的数据严格，但我不确定如何以类型系统强制执行的方式执行此操作。

我在想类似“Strict Monad”的东西，但也许这不是这样做的正确形式。

【问题讨论】：

你见过Disciple language吗？
谢谢。我一直在寻找一种方法将其压缩到当前的 Haskell（嗯，就是 GHC）中，但这也很有趣。
在具有手动内存管理的程序中内存泄漏的普遍性反驳了您的论点，即很容易确定 C/C++ 程序的空间使用上限。也就是说，很好的问题！
@Clinton，哦，作为一名 C++ 开发人员，我深深地不同意内存管理“非常简单”。一般来说，这很困难，而且有很多抽象是因为它你根本无法做到的。
@Clinton 这有点像说“在 Haskell 中空间泄漏很容易避免，只需对数据进行管道化并使用严格注释（如有必要）”。当然有办法通过仔细编程来避免空间问题，但保证偶尔会出错，因为所有代码都有错误。

标签： haskell lazy-evaluation strictness

【解决方案1】：

我相当肯定在 Haskell 中实现这一点几乎是不可能的，它默认假设是惰性的。例如，标准库中的某些函数在严格的语言中是无用的，因为如果您请求它们的全部输出，它们实际上保证不会终止。因此，如果你有一个 Haskell 的“严格子集”，就很难与任何其他 Haskell 代码互操作，而且你实际上是在用另一种语言进行编程。

另外，我认为你在考虑单子时找错地方了。 Data.STRef 确实与避免笨拙和懒惰无关。实际上，您想要的（严格性）与命令式无关，您不需要可变性或单子来获得它。有些编程语言和 Haskell 一样纯粹，但到处都是严格的。例如，我使用过的一个是Mercury。

【讨论】：

我认为 Mercury 并不严格。之所以严格要求它应该检查目标的每个先决条件（由连词 , 组成）而它可以选择析取（;）。而且据我所知，它可以在保持di/uo 的同时重新排序任何东西（被破坏的输入/用于表示类似 IO 的东西的唯一输出）。附言很高兴知道还有另一个人看到了 Mercury 并传播了存在这种语言的事实。
@ony 析取是非严格的，就像 if/then/else 在每种语言中都是非严格的一样；如果在选择一个分支之前对所有分支进行了全面评估，那么您就不能真正进行分支！该语言通常是严格的，因为调用 predicate(Input, Output) 将返回 Output 绑定到一个完全评估的值（没有 thunk），如果 Output 是无限的，那么即使你不需要调用也不会终止使用Output 做任何事情。
@ony 但是，由于回溯/不确定性，它有点复杂，所以从这个意义上说你是对的。如果在更高级别发生故障，predicate 可能能够恢复生成另一个Output，因此它所引用的数据可能会保存在内存中以防万一。由于 Haskell 的非严格性，它与失控的 thunk-generation 并不是一回事，而且通常可以从谓词的确定性类更直观地预测。

【解决方案2】：

您可能有兴趣了解BangPatterns language extension 和Unboxed types/operations。但你也应该知道任何函数总是具有盒装类型的含义。这是优化的责任，通过根据“bangs”和其他内容将代码编译到函数中来消除任何 ref-kind 值。

【讨论】：

【解决方案3】：

我想了很多。其他人也是如此：

现在是我自己的猜测。

在上述讨论中，大多数情况下的基本想法是，您可以在 any 类型上粘贴!，以获得该类型的严格、明确评估的 WHNF 版本。所以Int 可能是一个重击，而!Int 绝对不是一个。这为类型检查器提出了有趣的问题。 !Int ~ Int 是否成立？如果不是——这两者是完全独立的、不兼容的类型——那么使用它们将是非常痛苦的。另一方面，如果它确实成立，则没有什么可以阻止传递一个未评估的Int，而!Int 是预期的——毕竟，它们是同一类型。您理想情况下想要的是能够提供 !Int ，其中预期 Int ，但反之亦然。这听起来像是一种子类型关系：!a <: a、!a 是 a 的子类型、a 包含已评估值和未评估值（thunk），而 !a 仅包含已评估值。 GHC 的类型系统没有子类型，可能也没有，因为类型系统的其他部分不能很好地与之交互。这是一个高度受限的特定子类型实例：程序员无法声明任意子类型关系，而是存在一个单一的硬编码关系：forall a. !a <: a。我不知道这是否使它更合理地实施。

假设它可以完成。你会得到更多的问题。如果您确实尝试提供Int，而预期!Int 会怎样？类型错误？理想情况下，我认为不会，而是编译器会插入代码来评估它，然后继续。好的。在一般情况下提供[Int] 或[!Int] 或f a 和f !a 怎么样？编译器怎么可能知道如何遍历任何给定的结构来找到它包含a 的那些点，来评估那些，并且只评估那些？那么 that 会是类型错误吗？让我们说它是。程序员如何手动进行转换——从f a 获得f !a？也许通过映射函数eval :: a -> !a？但这是荒谬的。 Haskell 非常懒惰。如果将它应用于参数eval x，那么在需要它的值之前，它将是一个 thunk。所以eval x 不可能有类型!a。返回类型位置中的严格性注释没有任何意义。那么：data Wrap a = Wrap { unwrap :: a }、eval' :: a -> Wrap !a 的语义是 Wrap !a 可能是一个 thunk，但编译器会插入代码，这样当你评估它时，里面的 !a 肯定也会被评估？实际上，这里有一个更简单的公式：data Wrap' a = Wrap' { unwrap' :: !a } (eval' = Wrap')。这是现有的合法 Haskell，被我们新的严格类型所包含。这很好，我猜。但是一旦你尝试使用它，你就会再次遇到问题。你将如何从f a 到f !a，再次--fmap unwrap . fmap Wrap？但是unwrap 的问题与eval 完全相同。所以这一切似乎都不是那么微不足道。那么看似无害的反向案例呢：提供f !a 而f a 是预期的？那样有用吗？（换句话说，f !a <: f a？）这取决于在f 内部如何使用a。编译器必须了解协变、逆变和不变类型参数的位置——子类型化带来的另一件事。

这是我想通的。这似乎比看起来更难。

还有一件有趣的事。您可能听说过也可能没有听说过未提升类型的概念：没有底部居住的类型。这就是，据我所知，与此相同。保证被评估为 WHNF 的类型；保证不是底部的类型。没有区别，对吧？ GHC 实际上已经有一堆未提升的类型作为基元（Int# 等），但它们是有线的（你不能添加新的）并且除了未提升之外还没有装箱，所以它们有不同的类型（# 而不是*）并且不能与普通类型混合。而!a 将是一种未提升但盒装的类型，类似于*。未提升类型是我在类型理论上下文中多次提到的东西，所以也许有一些研究以更一般的方式实现它们。我还没看呢。

【讨论】：