On Wed, 2008-12-31 at 22:08 -0600, Jonathan Cast wrote: > On Thu, 2009-01-01 at 03:50 +0000, ra...@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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe