[Haskell-cafe] Re: Laws and partial values

[Jake McArthur]

Thomas Davie wrote:
>> Oviously, bottom is not ()
> 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 ().

This would be true if the type system distinguished between termination 
and nontermination and I had said

     bottom :: Total ()

, where Total is the type annotation that says the computation must 
terminate, in which case I would have had to say this, or something 
equivalent:

     bottom = ()

But Haskell has no Total type annotation, and it allows for general 
recursion. That is,

     bottom = bottom

is perfectly fine. The Haskell's semantics *require* this to be a 
nonterminating function of type Unit.

>> More generally, _|_ inhabits every Haskell type, even types with 
>> no constructors (which itself requires a GHC extension, of course):
> 
> Does it?  Do you have a document that defines Haskell types that way?

As Daniel has already pointed out, the report does specify this.

>>    data Empty
>>
>>    bottom' :: Empty
>>    bottom' = undefined
>>
> 
> Now that one is interesting, I would argue that this is a potential flaw 
> in the type extension – values in the set defined here do not exist, 
> that's what the data definition says.

Again, the specification mandates that all data types also implicitly 
include _|_. Would you argue that the type system should prevent me from 
saying this?

     foo :: Empty
     foo = foo

The type of foo unifies with itself, and the type system is unaware that 
foo has no data constructors.

- Jake