[Haskell-cafe] Re: Laws and partial values
jake at pikewerks.com
Sat Jan 24 16:20:10 EST 2009
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
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
foo :: Empty
foo = foo
The type of foo unifies with itself, and the type system is unaware that
foo has no data constructors.
More information about the Haskell-Cafe