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.