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

Question

在阅读matt写的文章时,我看到了以下的意见.

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

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

Answer 1

这可以覆盖一个真正多种不同的技术.最简单的基本上是不可避免的:如果你想要一个可以为null的值,这可能依赖于可变状态或用户输入,你必须用类型系统标记它.这是什么Maybe,ST并IO分别做.因此,如果您的某些内容不属于上述三种类型之一,则您必须知道它必须是一个不能为空的引用透明值.

上述技术对语言非常重要,基本上是不可避免的.但是,还有其他方法可以使用类型系统来提高安全性和正确性,这些方法更有趣.

一个有用的例子是阻止SQL注入.SQL注入是Web应用程序中的常见问题 - 对于基本概念,请查看此XKCD漫画.我们实际上可以使用类型系统来确保传递给数据库的任何字符串都已经过清理.基本思想是为"原始"字符串创建一个新类型:

newtype Raw a = Raw a

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

sanitize :: Raw String -> String

由于普通函数接受String而不是Raw,因此您将无法意外地传入未经过类型化的字符串.而且由于我们定义了Raw使用newtype,它根本没有运行时开销.

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

在最极端的情况下,您甚至可以使用类型系统来确保矩阵的大小合适.这是一个非常简单的方法.首先,我们需要类型级别的数字:

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

此函数仅允许您在内部维度匹配时将矩阵相乘,并确保结果矩阵在其类型中具有正确的维度.

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

Answer 2

嗯,在我看来,像你所看到的那些博览会经常无法传达的事情之一就是这种正确的类型通常是"自然地"不会发生的东西,而是来自使用设计类型的技巧对于来自其他语言的程序员来说并不明显.我最喜欢的一个例子来自关于幻像类型的Haskell Wiki页面 ; 如果您查看该页面上的第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这里列出的类型允许你让a 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带有唯一的匿名标签类型参数,所以现在没有两个Hypercube可以有Cell相同的s类型.基于这个原因,如果我们使用的模块系统,以防止用户构建CellS,呼叫者不可能问Hypercube的Cell,它不具备一个值.

致谢:我通过在Stack Overflow中询问这个技术.