Re: [Haskell-cafe] Re: Laws and partial values

25 Jan 2009


      On Sun, 2009-01-25 at 10:09 -0800, Conal Elliott wrote:
...
On Sun, Jan 25, 2009 at 9:17 AM, Jonathan Cast
 wrote:
On Sun, 2009-01-25 at 09:04 -0800, Conal Elliott wrote:
        >
        > On Sun, Jan 25, 2009 at 7:11 AM, Jonathan Cast
        >  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