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! > mean not every function with a _|_ input will issue a _|_ output, True --- but we can say a couple of things: * For all Haskell functions f, if f _|_ is an application of a constructor C, then f x is an application of C (to some value), for all x. [1] * For all Haskell functions f, if f _|_ is a lambda expression, then f x is a lambda expression, for all x. The only other possibility for f _|_ is _|_. (Do you see why bad above is impossible?) > so we have to say what result will be issued by a _|_ input in the > definitions of the functions if we want to prove the equvalence > between them? You have to deduce what the value at _|_ will be. > However, in the case of map f _|_ , I do believe the result will be > _|_ since it can not be anything else, but how I could prove this? any > clue? Appeal to the semantics of Haskell pattern matching. If you like, you can de-sugar the definition of map a little, to get map = \ f xn -> case xn of [] -> [] x:xn0 -> f x : map f xn0 And then you know that case _|_ of [] -> ... ... = _|_ whatever you fill in for the ellipses. (Do you see why this *must* be part of the language definition?) > ps, the definition of map does not mention anything about _|_ . The behavior of map f _|_ is fixed by the definition of Haskell pattern matching. jcc _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe