我在安全至关重要的行业中工作，并且我们的软件项目通常会提出安全要求；我们必须证明该软件具有高度确定性的事情。这些通常是负面的，例如“损坏频率不应超过1中的1”。 (我应该补充一点，这些要求来自统计系统安全要求)。
损坏的一个根源显然是编码错误，我想使用Haskell类型系统至少排除这些错误的某些类别。像这样:
首先，这是我们必不可少的关键数据项。
newtype Critical = Critical String
现在，我想将此项目存储在其他结构中。
data Foo = Foo Integer Critical
data Bar = Bar String Critical
现在，我想编写一个从Foo到Bar的转换函数，可以确保不会与Critical数据发生冲突。
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”，但这无济于事。
起作用的一件事是不导出Critical构造函数，然后执行
mkCritical :: String -> IO Critical
由于创建这些关键数据项的唯一位置是在输入函数中，因此这很有意义。但我希望有一个更优雅，更通用的解决方案。
编辑
在评论中FUZxxl建议看看Safe Haskell。这看起来是最好的解决方案。与其像我本来想要的那样在类型级别添加“不损坏”修饰符，不如说可以在模块级别执行此操作，如下所示:
1:创建一个模块“Critical”，该模块导出Critical数据类型的所有功能，包括其构造函数。通过在标题中放置“{-＃LANGUAGE Unsafe＃-}”，将此模块标记为“unsafe”。
2:创建一个模块“SafeCritical”，该模块重新导出除构造函数和可能用于破坏临界值的任何其他函数以外的所有内容。将此模块标记为“可信任”。
3:将处理关键值而不会损坏的所有模块标记为“安全”。然后使用它来证明任何导入为“安全”功能的功能都不会导致损坏到临界值。
这将剩下较少的代码，例如解析关键值的输入代码，需要进一步验证。我们无法消除此代码，但是减少需要详细验证的数量仍然是一个重大胜利。
该方法基于以下事实，即函数无法发明新值，除非函数返回它。如果一个函数仅获得一个关键值(如上述“转换”函数中所述)，则该函数只能返回一个关键值。
当一个函数具有两个或更多个相同类型的Critical值时，问题的变化就会更大。它必须保证不会混淆它们。例如，
swapFooBar :: (Foo, Bar) -> (Bar, Foo)
swapFooBar (Foo n c1, Bar s c2) = (Bar s c1, Foo n c2)
但是，可以通过对包含的数据结构进行相同的处理来解决此问题。
最佳答案
您可以使用参数化来达到目标
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
关于haskell - 在Haskell中证明 “no corruption”，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/7435363/