haskell - 将正确性约束直接编码到 Haskell 类型系统中？

Question

在阅读article时Matt might 写的，我看到下面这句话。

experienced programmers become adept at encoding correctness constraints directly into the Haskell type system

谁能解释一下这句话的意思或者提供一个简短的例子吗？

Answer 1

这可以涵盖非常各种不同的技术。最简单的基本上是不可避免的:如果你想要一个可以为 null 的值，它可以依赖于可变状态或用户输入，你必须使用类型系统来标记它。这就是 Maybe、ST 和 IO 分别所做的事情。因此，如果您的某些内容不属于上述三种类型之一，您就知道它必须是一个不能为 null 的引用透明值。

上述技术对于该语言来说是非常基础的，基本上是不可避免的。然而，还有其他更有趣的方法可以使用类型系统来提高安全性和正确性。

一个有用的例子是防止 SQL 注入(inject)。 SQL注入(inject)是Web应用程序中的一个常见问题——有关基本思想，请查看this XKCD cartoon 。我们实际上可以使用类型系统来确保传递到数据库的任何字符串都已被清理。基本思想是为“原始”字符串创建一个新类型:

newtype Raw a = Raw a

然后，确保从用户获取输入的所有函数都返回原始值而不是普通字符串。最后，您只需要一个清理功能:

sanitize :: Raw String -> String

由于普通函数接受 String 而不是 Raw，因此您将无法意外传入未经处理的字符串。由于我们使用 newtype 定义了 Raw，因此它根本没有运行时开销。

Yesod主要的 Haskell Web 框架之一，使用类似这样的技术来防止 SQL 注入(inject)。它还具有其他一些很酷的方法，例如使用类型系统来防止数据库中的链接损坏；你应该检查一下。

在真正极端的情况下，您甚至可以使用类型系统来确保矩阵具有正确的大小。这是一个非常简单的方法来做到这一点。首先，我们需要类型级别的数字:

data Z
data S n

(我们在 Peano Arithmetic 处使用 type level。)这个想法很简单:Z 是 0，S 是后继函数，所以 S Z 为 1，S (S Z) 为 2，依此类推。

我们现在可以编写一个安全的矩阵乘法函数:

matMul :: Mat a b -> Mat b c -> Mat a c

此函数仅允许您在内部维度匹配的情况下将矩阵相乘，并确保生成的矩阵在其类型中具有正确的维度。

Type-safe matrix multiplication有更多详细信息。