On 24 Jan 2009, at 21:31, Dan Doel wrote:
On Saturday 24 January 2009 3:12:30 pm Thomas Davie wrote:
On 24 Jan 2009, at 20:28, Jake McArthur wrote:
Thomas Davie wrote:
But, as there is only one value in the Unit type, all values we have no information about must surely be that value
The flaw in your logic is your assumption that the Unit type has only one value. Consider
bottom :: () bottom = undefined
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 ().
For integers, is _|_ equal to 0? 1? 2? ... Hypothetically (as it's already been pointed out that this is not the case in Haskell), _|_ in the integers would not be known, until it became more defined. I'm coming at this from the point of view that bottom would contain all the information we could possibly know about a value while still being the least value in the set.
In such a scheme, bottom for Unit would be (), as we always know that the value in that type is (); bottom for pairs would be (_|_, _|_), as all pairs look like that (this incidentally would allow fmap and second to be equal on pairs); bottom for integers would contain no information, etc.
, but its type, nonetheless, is Unit. Unit actually has both () and _|_. 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?
From the report: "Since Haskell is a non-strict language, all Haskell types include _|_."
http://www.haskell.org/onlinereport/exps.html#basic-errors
Although some languages probably have the semantics you're thinking of (Agda, for instance, although you can write non-terminating computations and it will merely flag it in red, currently), Haskell does not.
Yep, indeed. Bob