Haskell:未定义值的模式匹配

Question

据我了解，Haskell 的 undefined值 - 特定类型的值 - 是无法确定的值，无论出于何种原因(可能没有合理的定义，或者计算出现分歧)。例如:undefined :: [Int]是一个列表，所以它必须用 [] 或 (:) 构造，但它不知道是哪一个!因此，在 undefined 上拆分大小写会使整个表达式未定义是有道理的:我不知道 null (undefined :: [a])是对还是错，因为不知道是不是undefined :: [a]是否为空。

(顺便说一句 - 如果你不同意我的建议，即 undefined 是用构造函数构建的，那么肯定 null (undefined :: [a]) 应该评估为 False？毕竟 undefined 不等同于 []!)

然而，Haskell 模式匹配并不遵循这种思维方式。

data Foo = Foo Int String  -- Only one data constructor

silly :: Foo -> Bool
silly (Foo _ _) = True

ghci> silly (undefined :: Foo)
*** Exception: Prelude.undefined    -- But whatever the value is, it must 
                                    -- be constructed with Foo.
                                    -- So why fail to match?

(我知道 newtype 在这里表现不同。)

还:

foo :: Int -> String -> Bool
foo 8 "Hello" = True
foo _ _       = False

ghci> foo undefined undefined
*** Exception: Prelude.undefined     -- GOOD - can't tell which case to choose.

ghci> foo undefined "Hello"
*** Exception: Prelude.undefined     -- GOOD - still can't tell.

ghci> foo undefined "Goodbye"
*** Exception: Prelude.undefined     -- BAD  - should return false!
                                     -- Pattern match on first line should fail,
                                     -- because whatever the int is, the
                                     -- string can't match the given pattern.

我认为目前模式匹配的规则是，如果一个子模式失败，那么该模式应该立即失败；如果它发散，那么整个模式也应该发散；如果成功，则应尝试下一个子模式。如果所有子模式都成功，则整个模式都成功。

我的建议是，如果任何子模式失败，那么整个模式都应该失败；如果没有失败但有些分歧，那么整个模式应该分歧；如果一切都成功，那么整个模式应该会成功。

为什么这不是 Haskell 做事的方式？

编辑:

所以总结一下我对我读过的回应的解释:
undefined应该读作“这会导致你的程序永远运行”而不是“这没有很好的定义”，和 Exception: Prelude.undefined应该读作“小心!如果 undefined 是一个无限循环，你的程序永远不会终止”而不是“我不知道该怎么做，因为我不知道 undefined 是什么值”。

有人可以验证这是正确的吗？如果是这样，那么我可能会接受 mb14 的回答。

谢谢大家。很抱歉吸收这么慢!

Answer 1

基本上，您是说 undefined :: Foo和 Foo undefined undefined应该是一样的，因为(正如你所说的 But whatever the value is, it must be constructed with Foo.) 。

这个假设是不正确的。 Foo 必须用 Foo 构建只有当它可以 build 时。如果我有 foo = if x then (Foo 1 "a") else (Foo 2 "b") 怎么办.如 x未定义然后尝试评估 f发散。那时，没有构造函数与否的概念。它只是发散。

与您的示例相同 null (undefined :: [a])应该是 undefined (发散)也是因为您需要尝试评估 null 的参数知道它是否是 []或 : .

Haskell 中的 undefined 不是魔法，它只是一个循环。您可以定义自己的 loop = let x = x in x .每次您尝试对其进行评估时，这都会循环。
调用 null loop或 sill loop将循环，因此等于 loop ，不是吗？你还认为loop :: Foo和 Foo loop loop是相同的 ？我不。我期待 silly loop循环但不循环 silly (Foo loop loop) .

这个唯一的区别loop和 undefined就是ghc可以检测到undefined是一个循环，因此打破外观并显示错误消息而不是永远循环。它只是为了方便而存在，如果不存在，人们会定义 undefined = loop .