问错误和正确代码

EN

您可以编写自己的函数，这些函数永远不会产生值。考虑以下职能：

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“。如果他们能够为语言中的所有类型证明这一点，他们必然是图灵不完整的。

不可能证明任何任意函数都会在图灵完整语言中产生值。当然，你可以做一些特定的功能。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)。而且，这将是类型fmap的F实现，因为这两条规则都是Functor规则。这种特殊的“融合”律可用于优化目的。

资料来源:免费定理！http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf