haskell - 错误和正确代码

Question

我开始严重依赖 haskell 的类型系统来避免错误，并且正在寻找它是否也可以用来确保(弱？)形式的代码正确性。

我想到的代码正确性形式如下:

一个函数f :: a -> b如果 f 是正确的保证产生 b 类型的输出对于 a 类型的任何输入.对于众所周知的函数头(head:: [a] -> a)，这显然失败了。

我知道类型系统无法保证这种形式的正确性的一种方法是代码使用错误(error :: Char -> a)。错误函数几乎覆盖了整个类型系统，所以我想避免使用这个函数，除非明确表示。

我的问题有两个:

除了错误之外，还有哪些其他函数(或 haskell 片段)是 Haskell 类型系统的异常(exception)？

更重要的是，有没有一种方法可以禁止在 Haskell 模块中使用此类功能？

非常感谢!

Answer 1

您可以编写自己的永远不会产生值的函数。考虑以下函数:

never :: a -> b
never a = never a

它终止失败，所以它被认为是值 _|_ (发音为 bottom)。 All types in Haskell are actually the sum of the type and this special value .

您还可以编写仅部分定义的函数，例如

undefinedForFalse :: Bool -> Bool
undefinedForFalse True = True

undefinedForFalse False是 undefined ，这是一个在语义上等同于 _|_ 的特殊值除了运行时系统可以停止执行，因为它知道它永远不会完成。
error也是特殊函数，其结果在语义上总是等价于 _|_ ，它告诉运行时系统它可以停止执行，知道它永远不会完成，以及一条信息性错误消息。

Haskell 无法证明一个类型永远不能取值 _|_因为类型总是可以取值 _|_ .永远不能是 _|_ 的值称为“总”。总是产生 _|_ 以外的值的函数在有限的时间内称为“总函数”。可以证明这一点的语言称为“总语言”或“ total functional programming languages”。如果他们可以为语言中的所有类型证明这一点，那么他们必然是图灵不完备的。