强大的haskell没有错误

Question

我正在学习Haskell.我选择这种语言的动机之一是编写具有高度鲁棒性的软件,即完全定义的函数,数学上确定的函数,永不崩溃或产生错误.我并不是指由系统的谓词("系统内存不足","计算机着火"等)引起的故障,这些都不是很有趣,并且可能只是使整个过程崩溃.我也不是指由无效声明(pi = 4)引起的错误行为.

相反,我指的是错误状态导致的错误,我希望通过严格的静态类型使这些状态不可表示和不可编译(在某些函数中)来删除.在我看来,我把这些功能称为"纯粹",并认为强类型系统可以让我实现这一目标.但是,Haskell并没有以这种方式定义"纯",并允许程序error在任何上下文中崩溃.

为什么捕获异常非纯,但抛出异常是纯粹的？

这是完全可以接受的,并不奇怪.然而,令人失望的是,Haskell似乎没有提供某些功能来禁止可能导致分支使用的函数定义error.

这是一个人为的例子,为什么我觉得这令人失望:

module Main where
import Data.Maybe

data Fruit = Apple | Banana | Orange Int | Peach
    deriving(Show)

readFruit :: String -> Maybe Fruit
readFruit x =
    case x of
         "apple" -> Just Apple
         "banana" -> Just Banana
         "orange" -> Just (Orange 4)
         "peach" -> Just Peach
         _ -> Nothing

showFruit :: Fruit -> String
showFruit Apple = "An apple"
showFruit Banana = "A Banana"
showFruit (Orange x) = show x ++ " oranges"

printFruit :: Maybe Fruit -> String
printFruit x = showFruit $ fromJust x

main :: IO ()
main = do
    line <- getLine
    let fruit = readFruit line
    putStrLn $ printFruit fruit
    main

让我们说,我是偏执的纯粹的功能,readFruit并且printFruit真的不会因为无人状态而失败.你可以想象这个代码是用于发射满载宇航员的火箭,在绝对关键的例程中需要序列化和反序列化果实值.

第一个危险自然是我们在模式匹配中犯了一个错误,因为这给了我们无法处理的可怕的错误状态.值得庆幸的是,Haskell提供了内置的方法来防止这些,我们只需编译 -Wall包含-fwarn-incomplete-patternsAHA的程序:

src/Main.hs:17:1: Warning:
    Pattern match(es) are non-exhaustive
    In an equation for ‘showFruit’: Patterns not matched: Peach

我们忘了序列化Peach水果并且showFruit会抛出错误.这是一个简单的修复,我们只需添加:

showFruit Peach = "A peach"

该程序现在编译没有警告,避免危险!我们发射火箭但突然程序崩溃了:

Maybe.fromJust: Nothing

由于下面的错误线路导致火箭注定并击中海洋:

printFruit x = showFruit $ fromJust x

基本上fromJust有一个分支,它提出了一个Error所以我们甚至不希望程序编译,如果我们试图使用它,因为printFruit绝对必须是"超级"纯.我们可以修复它,例如通过用以下代码替换:

printFruit x = maybe "Unknown fruit!" (\y -> showFruit y) x

我觉得奇怪的是哈斯克尔决定实施严格的分型和不完全型检测,都在诺贝尔追求防止被表示的无效状态,但不给程序员的方式来检测分支正好落在在终点线前error,当他们不允许.从某种意义上说,这使得Haskell不如Java强大,它迫使您声明允许函数引发的异常.

实现这一点的最简单的方法是简单地error以某种方式未定义,本地为函数和其等式通过某种形式的相关声明使用的任何函数.然而,这似乎不可能.

关于错误与异常的维基页面通过合同提到了一个名为"扩展静态检查"的扩展,但它只会导致链接断开.

它基本归结为:如何使上面的程序不能编译,因为它使用fromJust？欢迎提出所有想法,建议和解决方案.

Answer 1

答案是我想要的是一定程度的完整性检查，不幸的是 Haskell 还没有提供（还？）。

或者，我想要依赖类型（例如Idris），或静态验证器（例如Liquid Haskell）或语法 lint 检测（例如hlint）。

我现在正在认真研究 Idris，它似乎是一门神奇的语言。这是Idris 创始人的演讲，我推荐观看。

这些答案归功于@duplode、@chi、@user3237465 和@luqui。