On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie <tom.davie@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