Am Sonntag, 25. Januar 2009 19:01 schrieb Conal Elliott:
I think I smell the same sort of circularity in this shifted "per definitionem" argument as well. Here's how I imagine making this implicit argument explicit:
Define "terminating" (or undefined) to mean "/= _|_" and "not terminating" (undefined) to mean "== _|_". Then, since () is obviously terminating (defined), it follows that () /= _|_ .
Is that the argument you had in mind?
No. Okay, let me quote my first post in this thread to have the context: ----- Am Samstag, 24. Januar 2009 21:12 schrieb Thomas Davie:
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 ().
It's obvious because () is a defined value, while bottom is not - per definitionem. The matter is that besides the elements declared in the datatype definition, every Haskell type also contains bottom. ----- I thought that under discussion were the actual Haskell semantics - I'm not so sure about that anymore. If Thomas Davie (Bob) was here discussing an alternative theory in which () is unlifted, the sorry, I completely misunderstood. My "argument" is that in Haskell as it is, as far as I know, _|_ *is* defined to denote a nonterminating computation, while on the other hand () is an expression in normal form, hence denotes a terminating computation, therefore it is obvious that the two are not the same, as stated by Jake. Of course I may be wrong in my premise, then, if one really cared about obviousness, one would have to put forward a different argument.
Does anyone see the flaw in that logic (and hence the purpose of "obviously").
I see the flaw in the argument you presented, but fortunately it's not even close to mine.
- Conal
Cheers, Daniel