17

在阅读马特梅写的文章时，我看到了以下句子。

有经验的程序员擅长将正确性约束直接编码到 Haskell 类型系统中

有人可以解释这句话的含义或提供一个简短的例子吗？

4

2 回答 2

18

这可以涵盖非常广泛的不同技术。最简单的基本上是不可避免的：如果你想要一个可以为 null 的值，它可以依赖于可变状态或用户输入，你必须用类型系统标记它。这就是分别做Maybe的ST和IO做的。因此，如果您有不属于上述三种类型之一的东西，您就知道它必须是一个不能为空的引用透明值。

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

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

newtype Raw a = Raw a

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

sanitize :: Raw String -> String

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

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

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

data Z
data S n

（我们在这里在类型级别使用Peano Arithmetic。）这个想法很简单：0是后继函数，1也是，2 等等。ZSS ZS (S Z)

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

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

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

类型安全的矩阵乘法有更多细节。

于 2013-04-25T05:47:24.937 回答
7

好吧，在我看来，像您所看到的那样的说明经常无法传达的一件事是，这种按类型正确性的东西通常不是“自然地”发生的东西，而是来自使用设计类型的技术对于来自其他语言的程序员来说并不明显。我最喜欢的例子之一来自关于幻象类型的 Haskell Wiki 页面；如果您查看该页面上的第 1 节，他们有这个示例（IMO 应该是newtype声明而不是data）：

data FormData a = FormData String

在a做什么？好吧，它的作用是人为地使FormData "foo" :: FormData Validated和FormData "foo" :: FormData Unvalidated，尽管它们的“真正”是相同的，但现在具有不兼容的类型，因此您可以强制您的代码不要混合使用其中的一种。好吧，让我不要重复页面所说的内容，它相对容易阅读（至少第 1 节）。

我在一个断断续续的项目中使用了一个更复杂的示例：OLAP超立方体可以看作是一种数组，它不是由整数索引索引，而是由数据模型对象（如人、天、产品线）索引， ETC。：

-- | The type of Hypercubes.
data Hypercube point value = ...

-- | Access a data point in a hypercube.
get :: Eq point => Hypercube point value -> point -> value

-- | This is totally pseudocode...
data Salesperson = Mary | Joe | Irma deriving Eq
data Month = January | February | ... | December deriving Eq
data ProductLine = Widget | Gagdet | Thingamabob

-- Pseudo-example: compute sales numbers grouped by Salesperson, Month and
-- ProductLine for the combinations specified as the "frame"
salesResult :: HyperCube (Salesperson, Month, ProductLine) Dollars 
salesResult = execute salesQuery frame
    where frame = [Joe, Mary] `by` [March, April] `by` [Widgets, Gadgets]
          salesQuery = ...

-- Read from salesResult how much Mary sold in Widgets on April.
example :: Dollars
example = get salesResult (Mary, April, Widgets)

我希望这比我担心的更有意义。无论如何，该示例的要点是以下问题： 的类型get，如此处所述，允许您要求 aHypercube告诉您它没有的点的值：

badExample :: Dollar
badExample = get salesResult (Irma, January, Thingamabob)

一种可能的解决方案是让get操作返回Maybe value而不是仅仅返回value. 但我们实际上可以做得更好；我们可以设计一个 API，其中 aHypercube只能被询问它包含的值。关键与FormData示例相似，但更复杂的变体。首先我们介绍一下这个幻像类型：

data Cell tag point = Cell { getPoint :: point } deriving Eq

现在我们重新制定Hypercube并get成为标签敏感的。在这个重新制定的示例中，我实际上将使其更加具体。我们从这个开始：

{-# LANGUAGE ExistentialTypes #-}

data AuxCube tag point value = 
    AuxCube { getFrame :: [Cell tag point]
            , get :: Cell tag point -> value }

-- This is using a type system extension called ExistentialTypes:
data Hypercube point value = forall tag. Hypercube (AuxCube tag point value)

-- How to use one of these cubes.  Suppose we have:
salesResult :: Hypercube (Salesperson, Month, ProductLine) Dollars 
salesResult = execute salesQuery points
    where points = [Joe, Mary] `by` [March, April] `by` [Widgets, Gadgets]
          salesQuery = ...

-- Now to read values, we have to do something like this:
example = case salesResult of
              Hypercube (AuxCube frame getter) -> getter (head frame)

如果在这里的使用使您感到困惑，我深表歉意ExistentialTypes，但长话短说，它在此示例中的作用基本上是每个都Hypercube包含一个AuxCube具有唯一匿名标记类型参数的，因此现在没有两个Hypercubes 可以具有Cell相同的 s类型。出于这个原因，如果我们使用模块系统来阻止调用者构造Cells，调用者就不可能向 a 请求Hypercube它Cell没有值的 a。

致谢：我是通过在 Stack Overflow 中提问来学习这项技术的。

于 2013-04-25T07:18:19.767 回答