我在安全关键行业工作,我们的软件项目通常都有安全要求; 我们必须证明该软件具有高度确定性.通常这些都是消极的,例如"不应该比1更频繁地腐败".(我应补充一点,这些要求来自统计系统安全要求).
腐败的一个来源显然是编码错误,我想使用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"键入check,但"badConvert"键入失败类型检查.
显然,我可以小心地不将Critical构造函数导入到进行转换的模块中.但是如果我能在类型中表达这个属性会好得多,因为那时我可以编写保证保留这个属性的函数.
我尝试在各个地方添加幻像类型和"forall",但这没有用.
可行的一件事是不导出Critical构造函数,然后具有
mkCritical :: String -> IO Critical
由于创建这些关键数据项的唯一位置是在输入函数中,这是有道理的.但我更喜欢更优雅和通用的解决方案.
编辑
在评论中,FUZxxl建议看一下Safe Haskell.这看起来是最好的解决方案.而不是像我原来想要的那样在类型级别添加"无损坏"修饰符,看起来你可以在模块级别执行它,如下所示:
1:创建一个模块"Critical",导出Critical数据类型的所有功能,包括其构造函数.通过在标题中添加"{ - #LANGUAGE Unsafe# - }"将此模块标记为"不安全".
2:创建一个"SafeCritical"模块,重新导出除构造函数和可能用于破坏临界值的任何其他函数之外的所有内容.将此模块标记为"值得信赖".
3:将处理临界值所需的任何模块标记为"安全"而不会损坏.然后使用它来演示导入为"safe"的任何函数都不会导致损坏到Critical值.
这将留下较少的代码,例如解析关键值的输入代码,需要进一步验证.我们无法消除此代码,但减少需要详细验证的数量仍然是一个重大的胜利.
该方法基于以下事实:除非函数返回,否则函数不能创建新值.如果一个函数只获得一个临界值(如上面的"转换"函数),那么它就是唯一可以返回的值. …
haskell ×1