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