[Haskell-cafe] Re: Laws and partial values

[Daniel Fischer]

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