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