Haskell: pattern matching on undefined values

Question

As I understand it, Haskell's undefined value - of a particular type - is a value that can't be determined, for whatever reason (maybe there is no sensible definition, or the calculation diverges). For instance: undefined :: [Int] is a list, so it must be constructed with either [] or (:), but it doesn't know which one! Hence it makes sense that case splitting on undefined makes the whole expression undefined: I don't know whether null (undefined :: [a]) is True or False, because I don't know whether undefined :: [a] is empty or not.

(By the way - if you disagree with my suggestion that undefined is built with a constructor, then surely null (undefined :: [a]) should evaluate to False? After all undefined isn't equivalent to []!)

However, Haskell pattern matching doesn't follow this way of thinking.

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?

(I know that newtype behaves differently here.)

Also:

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.

I think the rules on pattern matching currently say that if a sub-pattern fails then the pattern should immediately fail; if it diverges, then the whole pattern should also diverge; and if it succeeds, then the next sub-pattern should be tried. If all sub-patterns succeed, then the whole pattern succeeds.

What I am suggesting is that if any of the sub-patterns fail then the whole pattern should fail; if none fail but some diverge then the whole pattern should diverge; and if all succeed then the whole pattern should succeed.

Why is this not how Haskell does things?

---

EDIT:

So to summarise my interpretation of the responses I've read:

undefined should be read as "This would cause your program to run forever" not "This is not well defined", and Exception: Prelude.undefined should be read as "Watch out! Your program would have never terminated if undefined was an infinite loop" rather than "I don't know what to do because I don't know what value undefined is".

Could somebody please verify that this is correct? If so then I will probably accept mb14's answer.

Thanks everyone. Sorry for being so slow on the uptake!

Answer 1

Basically, you are saying that undefined :: Foo and Foo undefined undefined should be the same because (as you said But whatever the value is, it must be constructed with Foo.).

This assumption is not correct. Foo must be constructed with Foo only if it can be constructed. What if I have foo = if x then (Foo 1 "a") else (Foo 2 "b"). If x is undefined then trying to evaluate f diverges. At that point, there is no notion of constructor or not. It just diverges.

It is the same with your example null (undefined :: [a]) should be undefined (diverge) as well because you need to try to evaluate the parameter of null to know if it's a [] or a :.

Undefined in Haskell is not magic, it's just a loop. You could define your own loop = let x = x in x. This will loop each time you try to evaluate it. calling null loop or sill loop will loop and therefore is equal to loop, isn't it ?. Do you still consider that loop :: Foo and Foo loop loop are the same ? I don't. I expect silly loop to loop but not silly (Foo loop loop).

The only difference between this loop and undefined is just that ghc can detect undefined is a loop and so break the look and display an error message instead of looping forever. It's just there for convenience and if it wasn't there, people would define undefined = loop.

Answer 2

(By the way - if you disagree with my suggestion that undefined is built with a constructor, then surely null (undefined :: [a]) should evaluate to False? After all undefined isn't equivalent to []!)

This means it shouldn't evaluate to True, and it doesn't.

What I am suggesting is that if any of the sub-patterns fail then the whole pattern should fail; if none fail but some diverge then the whole pattern should diverge; and if all succeed then the whole pattern should succeed.

How could this be implemented? To find whether the first sub-pattern fails, you need to evaluate that argument; and if it diverges, the evaluation won't finish and the entire pattern match diverges by definition. You could try to evaluate all the patterns "in parallel", but this would greatly complicate the language: the current definition converts multiple equations into one which does case on the first argument, then on the second one, etc., so it doesn't introduce any new concepts; yours would have to.

I wouldn't quite say "undefined is supposed to represent a non-terminating calculation", but you aren't supposed to be able to distinguish them:

Errors in Haskell are semantically equivalent to ⊥ (“bottom”). Technically, they are indistinguishable from nontermination, so the language includes no mechanism for detecting or acting upon errors. However, implementations will probably try to provide useful information about errors. See Section 3.1.

Answer 3

You are starting from a false premise.

For instance: undefined :: [Int] is a list, so it must be constructed with either [] or (:), but it doesn't know which one!

No, it is constructed with neither. undefined :: [Int] is a list in the sense of being a value of type [a] for some a. It is not a list in the sense of being constructed with either [] or (:). This would be circular reasoning: "It is a list because it is constructed with [] or (:). It is constructed with [] or (:) because it is a list."

(By the way - if you disagree with my suggestion that undefined is built with a constructor, then surely null (undefined :: [a]) should evaluate to False? After all undefined isn't equivalent to []!)

By your logic, let loop = loop in null loop must also give False because loop isn't equivalent to [], as must all other forms of non-termination. This would make null a solution to the Halting Problem*!

The mistake you have made is that null does not actually ask if the value is constructed with [] or not. It asks whether the value is constructed with [], constructed with (:), or none of the above. Since undefined is constructed with neither [] nor (:), null undefined is neither True nor False. This is because Haskell's boolean logic is, in fact, a three-value system: Bool is inhabited by True, False, and bottom. It is entirely possible for a predicate to have an answer which is neither True nor False. Indeed, because Haskell is not a total language, it must be possible.

Here's another counterexample:

data Void

is a type with no constructors. If undefined must be constructed then it could not inhabit Void because Void has no constructors. But it does inhabit Void. GHC will happily accept undefined :: Void.

Since it is not true that undefined must be constructed, I won't address the rest of the arguments based on this premise.

Now, let's talk about why the given definition of undefined might be so. I will argue that undefined is a user-friendly alternative to nontermination for representing bottom.

Since Haskell is a non-total language with general recursion, one can always define:

undefined :: a
undefined = undefined

This undefined is a bottom value, an inhabitant of every type. However, it is not a particularly user-friendly bottom value because any scrutinization will cause a program to hang indefinitely. The undefined in the Prelude is a user-friendly alternative: scrutinization does not cause a program to hang but rather terminates the program immediately. However, in all other respects, Prelude.undefined must act like a bottom value if it is to be of use.

Consider the alternative, where Prelude.undefined was somehow observably different under evaluation from a "true" bottom value. This would mean that we have two extra inhabitants of every type: the "true" bottom value and an extra non-bottom value with subtly different semantics. This would not be useful, for what I hope are obvious reasons.

Thus, in order for Prelude.undefined to be useful, it must have equivalent behavior under evaluation to undefined = undefined. The fact that the behavior is not identical is a matter of convenience, but we can and should treat the result of its evaluation as equivalent. Consider the error that it throws to mean "GHC managed to detect this nonterminating program for you. You are welcome, but you might not be so lucky next time." In fact, by this logic you should also consider any values built using error to be similarly equivalent bottom values. It is the only useful, consistent interpretation.

---

* Or rather, null and a notNull that similarly checks for (:) and gives False for bottoms would form a solution to the halting problem: halts x = null x || notNull x.

Answer 4

You might want to take a look at The 2010 Haskell Language Report, specifically, section 3.1 on Errors.

Short answer: Your example fails because of WHNF -> NF evaluation, which has to do with Haskell's laziness, which makes it possible that some values will never be used or "looked at"; if Haskell's laziness rules allow undefined to be skipped over, you won't get a crash and error code. Otherwise, you will. In that case, you did. Changing that behavior wouldn't involve changing undefined so much as it would involve changing Haskell's evaluation strategies.

Observations:

[] is just syntactic sugar for repeated application of (:) + a Nil, so it's not true that "it can be constructed with either", or it is true, but misleading, because they are actually the same thing.

The way you've phrased undefined make it seem as if it's a sensible value for cases where types (or pattern matches) aren't fully determinable, however, as far as I understand it, this is not the purpose of undefined. Rather, given that it has a type of undefined :: t, it allows you to place it inside of a function and have that function typecheck in most scenarios.

Let me phrase that another way: undefined ought to be used to leave a function in some real sense of the word, undefined, while allowing you to compile because undefined's type will make it typecheck (otherwise you'd have to remove that function from scope). undefined, I do not believe, has any other purpose (and ideally, you should use error for this instead). If you call a function with undefined in it, and Haskell ever evaluates undefined (I think this would be taking it from a WHNF representation to NF), then you'll get a crash + error message.

The fact that people use undefined for other reasons like examining laziness properties of Haskell does not to me mean that undefined itself is supposed to have any behavior or properties other than throwing an error every time the compiler sees it. The fact that it does that is why it's a useful function for looking at those properties of Haskell. The key observation is that this shows how Haskell evaluates anything, not just undefined.

Answer 5

Complementary to all the other answers, there is a way to catch an exception. The downside is that you will have to perform your operation in the IO monad. I will explain. The things to look at are evaluate, try and ErrorCall. It works like this:

import Control.Exception

test :: a -> IO (Either ErrorCall a)
test val = try (evaluate val)

main = do
    result <- test (undefined :: String)
    print result

This will print

Left Prelude.undefined
CallStack (from HasCallStack):
 error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err
 undefined, called at main.hs:7:21 in main:Main

While using anything other than undefined will the string, e.g.

Right "foo"