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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
