[Haskell-cafe] Re: Laws and partial values
daniel.is.fischer at web.de
Sun Jan 25 17:36:19 EST 2009
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?
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
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
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
I see the flaw in the argument you presented, but fortunately it's not even
close to mine.
> - Conal
More information about the Haskell-Cafe