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