我已经开始严重依赖haskell的类型系统来避免bug，并且正在寻找是否也可以使用它来确保(弱?)形式的代码正确性。
我心目中的代码正确性的形式如下:
对于任意a类型的输入，如果f保证产生b类型的输出，则函数f :: a -> b是正确的。对于众所周知的函数头(head:: [a] -> a)，这显然是失败的。
当代码使用error (error :: Char -> a)时，我意识到类型系统无法保证这种形式的正确性。error函数几乎覆盖了整个类型系统，所以除非有明确的目的，否则我希望避免使用这个函数。
我的问题有两个:
-
除了error之外，还有哪些函数(或haskell片段)是haskell类型系统的异常?
-
更重要的是，是否有一种方法可以禁止在Haskell模块中使用这些函数?
多谢!
您可以编写自己的不产生值的函数。考虑以下函数:
never :: a -> b
never a = never a
它没有终止，所以它被认为是值_|_(发音为bottom)。Haskell中的所有类型实际上都是类型和这个特殊值的总和。
您也可以编写仅部分定义的函数，如
undefinedForFalse :: Bool -> Bool
undefinedForFalse True = True
undefinedForFalse False是undefined，这是一个特殊的值，在语义上等同于_|_，除了运行时系统可以停止执行，因为它知道它永远不会完成。
error也是一个特殊的函数，它的结果总是在语义上等同于_|_，它告诉运行时系统它可以停止执行，知道它永远不会完成，并伴随着一个信息错误消息。
Haskell不能证明一个类型永远不能取值_|_，因为一个类型总是可以取值_|_。永远不能为_|_的值称为"total"。在有限时间内总是产生_|_以外的值的函数称为"总函数"。能够证明这一点的语言被称为"总语言"或"总函数式编程语言"。如果他们能证明语言中的所有类型都是图灵不完备的
不可能证明任意函数在图灵完全语言中会产生一个值。当然，对于某些特定的函数可以这样做。Cirdec已经很好地涵盖了这一点，但是我想指出一些关于使用类型系统来保证(某种程度上)正确性的事情。
相关主题是参数性:给定多态类型签名的事实，通常只有一组有限的可能实现(如果我们排除error, undefined和其他类似的东西)。
(a -> b) -> a -> b就是一个例子。这个函数实际上只有一种可能的实现。
另一个例子是给定一个从A类型到B类型的f和一个函数r :: [a] -> [a]，可以表明r . map f = map f . r。这被称为map的"自由定理"。许多其他多态类型也有自由定理。
一个(有时更有用)的结果是，如果你能证明一个函数mapper :: (a -> b) -> F a -> F b服从mapper id = id定律，它可以证明mapper f . mapper g = mapper (f . g)。此外，这将是F类型的fmap实现，因为这两个定律是Functor定律。这种特殊的"融合"定律可以用于优化目的。
来源:定理免费!http://ttic.uchicago.edu/德雷尔/课程/论文/wadler.pdf