[Haskell-cafe] Re: Laws and partial values

[Thomas Davie]

On 25 Jan 2009, at 23:36, Daniel Fischer wrote:
>>
>> Why is this obvious - I would argue that it's "obvious" that bottom
>> *is* () - the data type definition says there's only one value in the
>> type.  Any value that I haven't defined yet must be in the set, and
>> it's a single element set, so it *must* be ().
>
> It's obvious because () is a defined value, while bottom is not - per
> definitionem.
> The matter is that besides the elements declared in the datatype  
> definition,
> every Haskell type also contains bottom.
> -----
>
> I thought that under discussion were the actual Haskell semantics -  
> I'm not so
> sure about that anymore. If Thomas Davie (Bob) was here discussing an
> alternative theory in which () is unlifted, the sorry, I completely
> misunderstood.
>
> My "argument" is that in Haskell as it is, as far as I know, _|_  
> *is* defined
> to denote a nonterminating computation, while on the other hand ()  
> is an
> expression in normal form, hence denotes a terminating computation,  
> therefore
> it is obvious that the two are not the same, as stated by Jake.
> Of course I may be wrong in my premise, then, if one really cared  
> about
> obviousness, one would have to put forward a different argument.

If you go look through the message history some more, you'll see a  
couple of emails which convinced me that that indeed was the semantics  
in haskell, and a follow up saying "okay, lets discuss a hypothetical  
now, because this looks fun and interesting."

Bob