Laws and partial values (was: [Haskell-cafe] mapM_ -> Monoid.Monad.map)

[Luke Palmer]

On Sat, Jan 24, 2009 at 2:40 AM, Ryan Ingram <ryani.spam at gmail.com> wrote:

> On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie <tom.davie at gmail.com>
> wrote:
> > Isn't the point of bottom that it's the least defined value.  Someone
> above
> > made the assertion that for left identity to hold, _|_ `mappend` () must
> be
> > _|_.  But, as there is only one value in the Unit type, all values we
> have
> > no information about must surely be that value, so this is akin to saying
> ()
> > `mappend` () must be (), which our definition gives us.
>
> But _|_ is not ().


Correction: _|_ is not always ().

I'm no expert in topology, but I think it goes something like this:

You can interpret partiality in (at least) two ways.  The one you're using
is to treat () as the Sierpinski space, which has one open set (which you
can think of as ()) and one closed set (as _|_).  Bottoms are explicit, and
nontermination is an essential part of the calculus.   The rest of the
topology is generated as follows: each function f : a -> () defines an open
and a closed set of as.  The open set is { x | f(x) = () }, and the closed
set is { x | f(x) = _|_ }.   It is a fatal error to ignore _|_ in this
semantics.

There is another topology.  Here the points are bottom-free values, possibly
infinite.  It is generated by, for each *finite *partial value v, choosing
the set of all fully-defined x such that v is less defined than x.   So, for
example, the open set representing Left _|_ in the space Either Bool Bool is
{ Left True, Left False }, whereas _|_ in this space is { Left True, Left
False, Right True, Right False }.

As far as I know, this is a valid topology as well, in which
scott-continuity corresponds to topological continuity.  However, if you are
using this topology, then () = _|_.

I think the difference is that the latter topology ignores nontermination.
When programs terminate, the two interpretations agree.  But the latter does
not give you any way to prove that something will not terminate.

FWIW, that last paragraph was gross speculation.  :-)


>
> For example:
>
> data Nat = Z | S Finite
>
> proveFinite :: Nat -> ()
> proveFinite Z = ()
> proveFinite (S x) = proveFinite x
>
> infinity :: Nat
> infinity = S infinity
>
> somecode x = case proveFinite x of () ->
> something_that_might_rely_on_x_being_finite


If some code relies on a value being finite, the only way it can go wrong if
you give it something infinite is not to terminate.  This is kind of the
point of continuity.


>
> problem = somecode infinity
>
> If you can pretend that the only value of () is (), and ignore _|_,
> you can break invariants.  This becomes even more tricky when you have
> a single-constructor datatype which holds data relevant to the
> typechecker; ignoring _|_ in this case could lead to unsound code.


Except in those cases (in the absense of unsafeCoerce, I'm talking about
GADTs etc.) the compiler is checking them for you.

Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090124/05fd1bbd/attachment-0001.htm