haskell - 在 Haskell 中证明 "no corruption"

Question

我在一个对安全至关重要的行业工作，我们的软件项目通常都有安全要求；我们必须证明该软件在高度确定性方面所做的事情。通常这些都是否定的，例如“不应该比 1 in 更频繁地损坏”。 (我应该补充一点，这些要求来自统计系统安全要求)。

损坏的一个来源显然是编码错误，我想使用 Haskell 类型系统来排除至少某些类别的这些错误。像这样的东西:

首先，这是我们不能损坏的关键数据项。

newtype Critical = Critical String

现在我想将这个项目存储在其他一些结构中。

data Foo = Foo Integer Critical
data Bar = Bar String Critical

现在我想写一个从 Foo 到 Bar 的转换函数，保证不会弄乱关键数据。

goodConvert, badConvert :: Foo -> Bar

goodConvert (Foo n c) = Bar (show n) c

badConvert (Foo n (Critical s)) = Bar (show n) (Critical $ "Bzzt - " ++ s)

我希望“goodConvert”进行类型检查，但“badConvert”无法进行类型检查。

显然，我可以小心地不要将 Critical 构造函数导入到进行转换的模块中。但是如果我可以在类型中表达这个属性会更好，因为这样我就可以组合出保证保留这个属性的函数。

我尝试在不同的地方添加幻像类型和“forall”，但这没有帮助。

可行的一件事是不导出关键构造函数，然后

mkCritical :: String -> IO Critical

由于创建这些关键数据项的唯一位置是在输入函数中，因此这是有道理的。但我更喜欢更优雅和通用的解决方案。

编辑

在评论中 FUZxxl 建议查看 Safe Haskell .这看起来是最好的解决方案。而不是像我最初想要的那样在类型级别添加“无损坏”修饰符，看起来您可以在模块级别执行此操作，如下所示:

1:创建一个模块“Critical”，导出Critical数据类型的所有特征，包括它的构造函数。通过在标题中放置“{-# LANGUAGE Unsafe #-}”将此模块标记为“不安全”。

2:创建一个模块“SafeCritical”，它重新导出除构造函数和任何其他可能用于破坏临界值的函数之外的所有内容。将此模块标记为“可信赖”。

3:将任何需要处理临界值而不损坏的模块标记为“安全”。然后用它来证明任何作为“安全”导入的函数都不会导致损坏到临界值。

这将留下一小部分代码，例如解析关键值的输入代码，需要进一步验证。我们无法消除此代码，但减少需要详细验证的数量仍然是一项重大胜利。

该方法基于这样一个事实，即除非函数返回新值，否则函数无法发明新值。如果一个函数只获得一个临界值(如上面的“转换”函数)，那么它就是唯一可以返回的值。

当一个函数有两个或多个相同类型的临界值时，问题就变得更难了。它必须保证不会混淆它们。例如，

swapFooBar :: (Foo, Bar) -> (Bar, Foo)
swapFooBar (Foo n c1, Bar s c2) = (Bar s c1, Foo n c2)

然而，这可以通过对包含的数据结构进行相同的处理来处理。

Answer 1

您可以使用参数化来实现这一目标

data Foo c = Foo Integer c
data Bar c = Bar String c

goodConvert :: Foo c -> Bar c
goodConvert (Foo n c) = Bar (show n) c

由于 c是一个不受约束的类型变量，你知道函数 goodConvert对 c 一无所知，因此不能构造该类型的不同值。它必须使用输入中提供的那个。

嗯，差不多。底部值允许您打破此保证。但是，您至少知道，如果您尝试使用“损坏”的值，它将导致异常(或非终止)。

badConvert :: Foo c -> Bar c
badConvert (Foo n c) = Bar (show n) undefined