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 ().
, 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?
data Empty
bottom' :: Empty bottom' = undefined
If you only ever use total functions then you can get away with not accounting for _|_. Perhaps ironically a function that doesn't account for _|_ may be viewed philosophically as a partial function since its contract doesn't accommodate all possible values.
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. Bob