Re: [Haskell-cafe] Re: Is "take" behaving correctly?

Hi
The same should apply to head and tail. head or tail of [] should be [].
What does the list think?
Disagree, strongly. Its not even possible for head, since [a] -> a. Wadler's theorems for free states that if head is given an empty list the _only_ thing it can do is crash.
What's the logic behind this? Thanks, Paul

On 9/12/07, PR Stanley
The same should apply to head and tail. head or tail of [] should be Disagree, strongly. Its not even possible for head, What's the logic behind this?
You don't need anything sophisticated for this. What possible total function could have signature [a] -> a? If you provide an argument of [] it has to conjure up a value of type a from somewhere. Where could it possibly get such a value for every single type a? For example, define
data Void -- the type with no elements (using -fglasgow-exts)
x = [] :: [Void] is a perfectly good list but head x has to be of type Void which has no elements. -- Dan

PR Stanley wrote:
Hi
The same should apply to head and tail. head or tail of [] should be [].
What does the list think?
Disagree, strongly. Its not even possible for head, since [a] -> a. Wadler's theorems for free states that if head is given an empty list the _only_ thing it can do is crash.
What's the logic behind this?
It's easy enough to define tail [] = [], but you can't write head [] = [] since [] is a *list* and head doesn't return a list. It returns a list element. And [] has no elements, so... what are you going to return? Notice that tail [] = error, yet drop 1 [] = [], which is interesting...
participants (3)
-
Andrew Coppin
-
Dan Piponi
-
PR Stanley