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

Question

在阅读由matt的书写的article的同时，我看到了下面的感觉。

有经验的程序员能熟练地直接编码正确性约束到Haskell的类型系统

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

Answer 1

这可以涵盖真的各种不同的技术。最简单的基本上是不可避免的：如果你想要一个可以为null的值，这可以取决于可变状态或用户输入，你必须用类型系统标记。这分别是Maybe,ST和IO。因此，如果您有上述三种类型中的某一种不具备，则您必须知道该参数必须是透明的值，不能为空。

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

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

newtype Raw a = Raw a 

然后，请确保您的所有功能，从用户获得的回报输入Raw值而不是正常的字符串。最后，你只需要一个净化功能：

sanitize :: Raw String -> String 

由于正常功能接受String而非Raw，你将无法在unsanitized串意外通过。由于我们使用newtype定义了Raw，因此它根本没有运行时间开销。

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

在真正极端的情况下，您甚至可以使用类型系统来确保矩阵的大小合适。这是一个非常简单的方法来做到这一点。首先，我们需要的类型级号：（我们在type level使用Peano Arithmetic这里）

data Z 
data S n 

的想法很简单：Z为0，S是后继功能，所以S Z是1，S (S Z)是2等等。

现在，我们可以写一个安全的矩阵乘法功能：

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

该功能只会让你乘矩阵如果内部尺寸相匹配，并确保所产生的基质在其类型正确的尺寸。

Type-safe matrix multiplication有更多细节。

Answer 2

嗯，在我看来，像你所见过的那些展览往往无法表达的东西之一就是这种类型的正确性往往是不会“自然地”发生的东西，而是来自使用技术来设计您的类型，这对于来自其他语言的程序员来说并不明显。我最喜欢的例子之一来自the Haskell Wiki page on phantom types;如果你看一下第1部分在该网页上，他们有这样的例子（IMO应该是一个newtype声明，而不是data）：

data FormData a = FormData String 

有什么a在做什么？那么，它的作用就是人为地让FormData "foo" :: FormData Validated和FormData "foo" :: FormData Unvalidated，尽管它们“真的”是相同的，现在有不兼容的类型，因此你可以强制你的代码不混合一个和另一个。那么，让我不要重复页面所说的内容，阅读起来相对容易（至少在第1部分）。

，我一直在用我的和小康的一个项目一个更复杂的例子：OLAP立方体可以看作是一种阵列由整数索引没有编号，而是由类似人的数据模型对象，天，产品系列等：

-- | 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的类型，都在这了，让你问一个Hypercube告诉你一个点的价值也没有：

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

一种可能对此的解决方案是使get操作返回Maybe value而不仅仅是value。但我们其实可以做得更好;我们可以设计一个API，其中Hypercube只能被问及它包含的值。关键是类似于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了一个独特的匿名标签type参数，所以现在没有两个Hypercube可以具有相同类型的Cell。由于这个原因，如果我们使用模块系统来阻止呼叫者构建Cell s，呼叫者不可能要求Hypercube找到Cell它没有值。

Credits：I learned this technique by asking here in Stack Overflow。