On Fri, 23 Jan 2009, Derek Elkins wrote:

mempty `mappend` undefined = undefined (left identity monoid law) The above definition doesn't meet this, similarly for the right identity monoid law. That only leaves one definition, () `mappend` () = () which does indeed satisfy the monoid laws.

So the answer to the question is "Yes." Another example of making things as lazy as possible going astray.

I'd like to argue that laws, such as monoid laws, do not apply to partial values. But I haven't thought my position through yet. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

Thanks for letting me reflect on this. I assume that my final program (my final value) is always a total value. Anything else is an error. Therefore, if we required relaxed monoid laws of the form x `mappend` mzero <= x then we could safely substitute (x `mappend` mzero) by x without changing the final value (I think this true). But the reverse substituion ,replacing x with (x `mappend` mzero), might not be sound. Now, I can see why you would prefer that the laws hold for partial values. On Fri, 23 Jan 2009, Luke Palmer wrote:

On Fri, Jan 23, 2009 at 6:10 PM, wrote: On Fri, 23 Jan 2009, Derek Elkins wrote:

mempty `mappend` undefined = undefined (left identity monoid law) The above definition doesn't meet this, similarly for the right identity monoid law.  That only leaves one definition, () `mappend` () = () which does indeed satisfy the monoid laws.

So the answer to the question is "Yes."  Another example of making things as lazy as possible going astray.

I'd like to argue that laws, such as monoid laws, do not apply to partial values.  But I haven't thought my position through yet.

Please try to change your mind.  

You know how annoying it is when you are doing math, and you want to divide, but first you have to add the provision that the denominator isn't zero.  Saying that monoid laws do not apply to partial values, while easing the implementation a bit, add similar provisions to reasoning. 

For example, it is possible to prove that foldr mappend mempty (x:xs) = foldr1 mappend (x:xs).  Which means that anywhere in the source where we see the former, we can "clean it up" to the latter.  However, if monad laws don't apply to partial values, then we first have to prove that none of the (x:xs) are _|_, perhaps even that no substrings are _|_.  This is a much more involved transformation, so much so that you probably just wouldn't do it if you want to be correct.

Bottoms are part of Haskell's semantics; theorems and laws have to apply to them to.  You can pretend they don't exist, but then you have to be okay with never using an infinite data structure.  I.e. if your programs would run just as well in Haskell as they would in a call-by-value language, then you don't have to worry about bottoms.

Luke

-- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie 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 (). 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 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. -- ryan

On Sat, Jan 24, 2009 at 2:40 AM, Ryan Ingram wrote:

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

On Sun, Jan 25, 2009 at 8:00 AM, Jonathan Cast wrote:

On Sat, 2009-01-24 at 03:08 -0700, Luke Palmer wrote:

...

On Sat, Jan 24, 2009 at 2:40 AM, Ryan Ingram wrote: But _|_ is not ().

Correction: _|_ is not always ().

For example: in Haskell.

Prelude> () `seq` True True Prelude> (undefined `asTypeOf` ()) `seq` True *** Exception: Prelude.undefined

Gee, I'm sure glad that I wrote that detailed analysis of what I meant. It's nice to see people responding to arguments rather than opinions for once. Luke

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 ().

, but its type, nonetheless, is Unit. Unit actually has both () and _|_. More generally, _|_ inhabits every Haskell type, even types with no constructors (which itself requires a GHC extension, of course):

Does it? Do you have a document that defines Haskell types that way?

data Empty

bottom' :: Empty bottom' = undefined

If you only ever use total functions then you can get away with not accounting for _|_. Perhaps ironically a function that doesn't account for _|_ may be viewed philosophically as a partial function since its contract doesn't accommodate all possible values.

Now that one is interesting, I would argue that this is a potential flaw in the type extension – values in the set defined here do not exist, that's what the data definition says. Bob

On 24 Jan 2009, at 21:31, Dan Doel wrote:

On Saturday 24 January 2009 3:12:30 pm Thomas Davie wrote:

...

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 ().

For integers, is _|_ equal to 0? 1? 2? ... Hypothetically (as it's already been pointed out that this is not the case in Haskell), _|_ in the integers would not be known, until it became more defined. I'm coming at this from the point of view that bottom would contain all the information we could possibly know about a value while still being the least value in the set.

In such a scheme, bottom for Unit would be (), as we always know that the value in that type is (); bottom for pairs would be (_|_, _|_), as all pairs look like that (this incidentally would allow fmap and second to be equal on pairs); bottom for integers would contain no information, etc.

...

...

, but its type, nonetheless, is Unit. Unit actually has both () and _|_. More generally, _|_ inhabits every Haskell type, even types with no constructors (which itself requires a GHC extension, of course):

Does it? Do you have a document that defines Haskell types that way?

From the report: "Since Haskell is a non-strict language, all Haskell types include _|_."

http://www.haskell.org/onlinereport/exps.html#basic-errors

Although some languages probably have the semantics you're thinking of (Agda, for instance, although you can write non-terminating computations and it will merely flag it in red, currently), Haskell does not.

Yep, indeed. Bob

On 24 Jan 2009, at 22:19, Henning Thielemann wrote:

On Sat, 24 Jan 2009, Thomas Davie wrote:

...

On 24 Jan 2009, at 21:31, Dan Doel wrote:

...

For integers, is _|_ equal to 0? 1? 2? ... Hypothetically (as it's already been pointed out that this is not the case in Haskell), _|_ in the integers would not be known, until it became more defined. I'm coming at this from the point of view that bottom would contain all the information we could possibly know about a value while still being the least value in the set.

In such a scheme, bottom for Unit would be (), as we always know that the value in that type is (); bottom for pairs would be (_|_, _|_), as all pairs look like that (this incidentally would allow fmap and second to be equal on pairs); bottom for integers would contain no information, etc.

Zero- and one-constructor data types would then significantly differ from two- and more-constructor data types, wouldn't they?

Yes, they would, but not in any way that's defined, or written in, the fact that they have a nice property of being able to tell something about what bottom looks like is rather nice actually. Bob

On 24 Jan 2009, at 22:47, Lennart Augustsson wrote:

You can dream up any semantics you like about bottom, like it has to be () for the unit type. But it's simply not true. I suggest you do some cursory study of denotational semantics and domain theory. Ordinary programming languages include non-termination, so that has to be captured somehow in the semantics. And that's what bottom does.

I'm not sure why you're saying that this semantics does not capture non-termination – the only change is that computations resulting in the unit type *can't* non terminate, because we can always optimize them down to (). Of course, if you want to be able to deal with non- termination, one could use the Maybe () type! Some chatting with Conal about the semantics I'm talking about revealed some nice properties, so I'm gonna run away and think about this, and then blog about it. Bob

Incorrect *if* the semantics distinguishes between () and _|_ (as apparently is the choice in Haskell). On Sat, Jan 24, 2009 at 2:40 PM, Jake McArthur wrote:

Thomas Davie wrote:

...

the only change is that computations resulting in the unit type *can't* non terminate, because we can always optimize them down to ().

No. "Optimizing them down to ()" changes the semantics of the computation. This is incorrect behavior.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Sat, 24 Jan 2009, Thomas Davie wrote:

I'm not sure why you're saying that this semantics does not capture non-termination – the only change is that computations resulting in the unit type *can't* non terminate, because we can always optimize them down to (). Of course, if you want to be able to deal with non-termination, one could use the Maybe () type!

I find the current semantics better: All types are handled the same way by default and whenever you want to "optimize" (undefined::()) to () you can use optimizeNull :: () -> () optimizeNull _ = ()

I can't argue with your position, because I don't understand it. :) -- Lennart On Sat, Jan 24, 2009 at 10:52 PM, wrote:

On Sat, 24 Jan 2009, Lennart Augustsson wrote:

...

You can dream up any semantics you like about bottom, like it has to be () for the unit type. But it's simply not true. I suggest you do some cursory study of denotational semantics and domain theory. Ordinary programming languages include non-termination, so that has to be captured somehow in the semantics. And that's what bottom does.

I'd like to argue (but am not certain) that all the sub-expressions of all *correct* programs are total, or rather that the values that the sub-expressions represent are total.

One needs to distinguish between the value of the representatives of data, and the data being represented. For example (constructive) real numbers are represented by Cauchy sequences, but real numbers are themselves a quotient of this type. We cannot create a data type that directly represents a real numbers and are forced to use representatives to compute with them. Similarly we want the reciprocal function only to be defined on real numbers that are apart from zero (the reciprocal total on this domain), but there is no such function type available in Haskell to do this. Therefore we represent it by a partial function.

Therefore we can safely reason about such programs by substitutions using laws (such as monoid laws) that are correct with respect to the *what the values are representing*. For example, real numbers form a monoid under addition only when the equivalence relation for the data that the values represent is used. Would anyone here argue that (Sum CReal) should *not* be a Monoid instance?

Sorry if this sounds a bit muddled. I need to find a clear way of conveying what I'm thinking. In short, my position is that partial values are only used to define the values of fixpoints and are sometimes used in the represenatives of data, but the data being represented is always total. Monoid laws etc. only apply to the data being represented, not to the underlying represenations.

If my position is untenable, please explain. :)

-- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

On Sat, 24 Jan 2009, Jake McArthur wrote:

What you said makes little sense to me either. ;) But I will try to fit the pieces together as best I can.

It appears to me that you may be talking about isomorphisms between the concepts we try to map to data types and the data representations themselves, and that you are postulating that these concepts are necessarily total, therefore the representations should be as well, or something like that.

I'm saying that the concepts are necessarily total. Acutally, now that I think about it, the concepts might not even have a CPO, so perhaps it is not meaningful to talk about if the concepts are total or not. So I'll refine my position to saying that the concepts just are. Their represenatives may not be total. For example we represent the concept of the reciprocal over Rational (whose domain excludes 0) by a represenative, recip :: Rational -> Rational, which is a partial function. In this case we could imagine an alternative implemenation of recip' :: NonZeroRational -> Rational, which also represents the concept of the reciprocal and is a total function. But in other cases such an alternative represenatitive cannot exist (e.g. recip for CReal). I belive it is the case that the concepts are isomorphic to the represenatives under a specific PER. I cannot imagine it any other way. Anyhow, the big point is that monoid laws apply to the concepts, not to the representatives.

If my understanding of your point is correct, then I disagree with it. What you describe sounds like abstraction, and what you describe as a partial function sounds like a *leaky* abstraction. If we truly want to restrict the domain of a function to nonzero real numbers, then the "total" way to go about it would be to create a new type that represents this domain, say by wrapping your real number type with a newtype and only exporting smart constructors to build values of that type.

Ah, but it is impossible to create such smart constructors because it is undecidable if a particular CReal represents 0 or not.

Deep inside, the function will definitely require a partial expression, but this is abstracted away. Then you can define a Monoid instance for this domain without fear.

But you *still* have to account for nontermination. You can still arrive at a situation where you have

_|_ `mappend` nonzeroRealNum

Since _|_ is a represenative that has no corresponding concept, the above program is simply an error.

. I hope I have understood correctly. I feel that I have not and that this email will just contribute to the confusion of other readers. :\

I hope I can work out my underdeveloped viewpoint through conversation. Hopefully I'll either see that I'm wrong, or convince people that I'm right. :) I'm sort of refining it as I go along here. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

Hi Lennart, On Sat, Jan 24, 2009 at 10:47 PM, Lennart Augustsson wrote:

You can dream up any semantics you like about bottom, like it has to be () for the unit type. But it's simply not true. I suggest you do some cursory study of denotational semantics and domain theory.

Umh. It's certainly not Haskell, but as far as I can tell, the semantics Bob likes are perfectly fine domain theory. (_|_, _|_) = _|_ is the *simpler* definition of domain-theoretical product (and inl(_|_) = inr(_|_) = _|_ is the simpler definition of domain-theoretical sum), and the unit of this product (and sum) is indeed the type containing only bottom. Lifting everything, as Haskell does, is extra. I suppose it's unusual that Bob wants to lift sums but not products, but there's nothing theoretically fishy about it that I can see. All the best, - Benja P.S. For anybody wanting to brush up: http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf -- Section 3.2. -B

Hm. Isn't _|_ simply, by definition, the bottom (least) element in an ordering? I see merit in Haskell's choice that () /= _|_, but so far I'm not persuaded that it's the only possible choice. On Sat, Jan 24, 2009 at 1:47 PM, Lennart Augustsson wrote:

You can dream up any semantics you like about bottom, like it has to be () for the unit type. But it's simply not true. I suggest you do some cursory study of denotational semantics and domain theory. Ordinary programming languages include non-termination, so that has to be captured somehow in the semantics. And that's what bottom does.

-- Lennart

On Sat, Jan 24, 2009 at 9:31 PM, Thomas Davie wrote:

...

On 24 Jan 2009, at 22:19, Henning Thielemann wrote:

...

On Sat, 24 Jan 2009, Thomas Davie wrote:

...

On 24 Jan 2009, at 21:31, Dan Doel wrote:

...

For integers, is _|_ equal to 0? 1? 2? ...

Hypothetically (as it's already been pointed out that this is not the case in Haskell), _|_ in the integers would not be known, until it

...

...

...

more defined. I'm coming at this from the point of view that bottom would contain all the information we could possibly know about a value while still being the least value in the set.

In such a scheme, bottom for Unit would be (), as we always know that

...

...

...

value in that type is (); bottom for pairs would be (_|_, _|_), as all

became the pairs

...

...

...

look like that (this incidentally would allow fmap and second to be equal on pairs); bottom for integers would contain no information, etc.

Zero- and one-constructor data types would then significantly differ from two- and more-constructor data types, wouldn't they?

Yes, they would, but not in any way that's defined, or written in, the fact that they have a nice property of being able to tell something about what bottom looks like is rather nice actually.

Bob _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 25 Jan 2009, at 00:11, Thomas Davie wrote:

I'm coming at this from the point of view that bottom would contain all the information we could possibly know about a value while still being the least value in the set.

Note that we can't possibly know what information can we possibly know about a value being given it's type. For example, you can prove that the only "reasonable" value of type (forall a. a -> a) is (id); so, from you POV, (_|_) :: forall a. a -> a is equal to (id). This means, that ((_|_) :: forall a. a -> a) 1 = 1 instead of (_|_). But there is no way for a compiler to deduce all the equalities of this kind.

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. Which definition(s) are you referring to? - Conal On Sat, Jan 24, 2009 at 12:31 PM, Daniel Fischer wrote:

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.

...

...

, but its type, nonetheless, is Unit. Unit actually has both () and _|_. More generally, _|_ inhabits every Haskell type, even types with no constructors (which itself requires a GHC extension, of course):

Does it? Do you have a document that defines Haskell types that way?

Section 4.2.1 of the report http://haskell.org/onlinereport/decls.html#sect4.2

...

...

data Empty

bottom' :: Empty bottom' = undefined

If you only ever use total functions then you can get away with not accounting for _|_. Perhaps ironically a function that doesn't account for _|_ may be viewed philosophically as a partial function since its contract doesn't accommodate all possible values.

Now that one is interesting, I would argue that this is a potential flaw in the type extension – values in the set defined here do not exist, that's what the data definition says.

Bob

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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? Bob

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 () .

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

On Sun, Jan 25, 2009 at 10:17 AM, Jonathan Cast wrote:

...

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?

I think the discussion is not about adding an inconsistent special case, but about theories in which a bottomless () *is* consistent. The denotational meaning of a program is nothing more than a meaning function applied to its syntax. In this discussion, we are simply toying with the meaning functions which remain faithful to our intuition about what a program "should" do, while giving slightly different answers on the edge cases, to see if it is more or less beautiful/consistent/useful. This discussion is in the same vein as discussions about what Haskell looks like if you remove seq, or if all one-constructor data types are unlifted -- both of those clean up the semantics considerably. What if this does too, and we just don't see how? We're trying to see. Luke

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. 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. - Conal

On Sun, 2009-01-25 at 07:11 -0800, 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.

Yes, "partial" as in "partial order" (v. total order or preorder) not as in partiality. It's actually the "complete" part that indicates the existence of a least element, pretty much by definition. A cpo is a dcpo (directed complete partial order) with a least element, though sometimes "cpo" is used for "dcpo" in which case a least element is not guaranteed.

On Sun, Jan 25, 2009 at 1:08 AM, 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.

Which definition(s) are you referring to?

...

- Conal

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? Does anyone see the flaw in that logic (and hence the purpose of "obviously"). - Conal

On 25 Jan 2009, at 23:36, Daniel Fischer wrote:

...

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.

If you go look through the message history some more, you'll see a couple of emails which convinced me that that indeed was the semantics in haskell, and a follow up saying "okay, lets discuss a hypothetical now, because this looks fun and interesting." Bob

Thomas Davie wrote:

...

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 ().

This would be true if the type system distinguished between termination and nontermination and I had said bottom :: Total () , where Total is the type annotation that says the computation must terminate, in which case I would have had to say this, or something equivalent: bottom = () But Haskell has no Total type annotation, and it allows for general recursion. That is, bottom = bottom is perfectly fine. The Haskell's semantics *require* this to be a nonterminating function of type Unit.

...

More generally, _|_ inhabits every Haskell type, even types with no constructors (which itself requires a GHC extension, of course):

Does it? Do you have a document that defines Haskell types that way?

As Daniel has already pointed out, the report does specify this.

...

data Empty

bottom' :: Empty bottom' = undefined

Now that one is interesting, I would argue that this is a potential flaw in the type extension – values in the set defined here do not exist, that's what the data definition says.

Again, the specification mandates that all data types also implicitly include _|_. Would you argue that the type system should prevent me from saying this? foo :: Empty foo = foo The type of foo unifies with itself, and the type system is unaware that foo has no data constructors. - Jake

On Sat, Jan 24, 2009 at 10:32 AM, wrote:

On Fri, 23 Jan 2009, Luke Palmer wrote:

For example, it is possible to prove that foldr mappend mempty (x:xs) =

...

foldr1 mappend (x:xs). Which means that anywhere in the source where we see the former, we can "clean it up" to the latter. However, if monad laws don't apply to partial values, then we first have to prove that none of the (x:xs) are _|_, perhaps even that no substrings are _|_. This is a much more involved transformation, so much so that you probably just wouldn't do it if you want to be correct.

Bottoms are part of Haskell's semantics; theorems and laws have to apply to them to. You can pretend they don't exist, but then you have to be okay with never using an infinite data structure. I.e. if your programs would run just as well in Haskell as they would in a call-by-value language, then you don't have to worry about bottoms.

BTW, This last statement isn't true. The expression (let x = 1:x in x) won't work in CBV, but it is a well defined value without any bottoms. In fact, every subexpression in that value is a well defined value wihtout any bottoms.

That's not what I said. My statement was a hypothetical: *if* it works call-by-value, then you don't have to worry about bottom. This program does not work in CBV, so my statement is true. I'm just being pedantic, of course. The deeper reason that you have to worry about bottoms in this expression is that its denotation is a limit: { _|_, 1:_|_, 1:1:_|_, 1:1:1:_|_, ... }. Bottom has an essential role in describing infinity, not just programs which don't halt. Luke **

On Sun, 25 Jan 2009, Lauri Alanko wrote:

On Fri, Jan 23, 2009 at 08:10:38PM -0500, roconnor@theorem.ca wrote:

...

I'd like to argue that laws, such as monoid laws, do not apply to partial values. But I haven't thought my position through yet.

Before you do, you may want to read "Fast and Loose Reasoning is Morally Correct":

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.8232

This is very good. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''