[Haskell-cafe] Re: Laws and partial values

[Jonathan Cast]

On Sun, 2009-01-25 at 10:09 -0800, Conal Elliott wrote:
> 
> On Sun, Jan 25, 2009 at 9:17 AM, Jonathan Cast
> <jonathanccast at fastmail.fm> wrote:
>         
>         On Sun, 2009-01-25 at 09:04 -0800, Conal Elliott wrote:
>         >
>         > On Sun, Jan 25, 2009 at 7:11 AM, Jonathan Cast
>         > <jonathanccast at fastmail.fm> wrote:
>         >
>         >         On Sun, 2009-01-25 at 10:46 +0100, Thomas Davie
>         wrote:
>         >         > On 25 Jan 2009, at 10:08, Daniel Fischer wrote:
>         >         >
>         >         > > Am Sonntag, 25. Januar 2009 00:55 schrieb Conal
>         Elliott:
>         >         > >>> It's obvious because () is a defined value,
>         while bottom
>         >         is not -
>         >         > >>> per
>         >         > >>> definitionem.
>         >         > >>
>         >         > >> I wonder if this argument is circular.
>         >         > >>
>         >         > >> I'm not aware of "defined" and "not defined" as
>         more than
>         >         informal
>         >         > >> terms.
>         >         > >
>         >         > > They are informal. I could've written one is a
>         terminating
>         >         > > computation while
>         >         > > the other is not.
>         >         >
>         >         > Is that a problem when trying to find the least
>         defined
>         >         element of a
>         >         > set of terminating computations?
>         >
>         >
>         >         Yes.  If you've got a set of terminating
>         computations, and it
>         >         has
>         >         multiple distinct elements, it generally doesn't
>         *have* a
>         >         least element.
>         >         The P in CPO stands for Partial.
>         >
>         >         jcc
>         >
>         > and this concern does not apply to ()  .
>         
>         
>         And?  () behaves in exactly the same fashion as every other
>         Haskell data
>         type in existence, and in consequence we're having an
>         extended, not
>         entirely coherent, discussion of how wonderful it would be if
>         it was a
>         quite inconsistent special case instead?  Why?
>         
>         jcc
> 
> Hi Jonathan,
> 
> The discussion so far had mostly been about whether *necessarily*
> () /= _|_, i.e., whether a choice of () == _|_ contradicts domain
> theory.

We started, I think, with the claim that () as implemented by GHC did in
fact satisfy the monoid laws, because () = _|_.  This is false ---
Haskell as it exists does not satisfy that equation.  The claim for this
was somewhat over-stated (it's not a law of domain theory that a domain
have two elements --- Haskell 98 even has a bottom-only type!)  So we
got the question of whether it is such a law or not.  But we started
with the question of whether () in the standard library is a monoid or
not --- with the claim that it is made on the basis of the idea that ()
`should' equal undefined :: ().  Apparently on the basis of a belief
that that was the way Haskell works.

> I think you're now switching to a different question (contributing to
> the "not entirely coherent" aspect of the discussion): which semantics
> is *preferable* for what reasons (merits).  On that question, I'm
> inclined to agree with you, because I like consistency.

Fun.

jcc