On Wed, 2008-12-31 at 22:08 -0600, Jonathan Cast wrote:
On Thu, 2009-01-01 at 03:50 +0000, raeck@msn.com wrote:
I am afraid I am still confused.
foo [] = ... foo (x:xs) = ... There is an implied: foo _|_ = _|_ The right side cannot be anything but _|_. If it could, then that would imply we could solve the halting problem:
in a proof, how I could say the right side must be _|_ without defining foo _|_ = _|_ ?
This definition is taken care of for you by the definition of Haskell pattern matching. If the first equation for a function has a pattern other than
* a variable or * a lazy pattern (~p)
for a given argument, then supplying _|_ for that argument /must/ (if the application is total) return _|_. By rule. (We say the pattern is strict, in this case).
and in the case of
bad () = _|_ bad _|_ = ()
Note that these equations (which are not in the right form for the Haskell equations that define Hasekll functions) aren't satisfied by any Haskell function!
This isn't just a quirk of Haskell semantics. bad is not computable. Period.