* Sebastian Fischer [2012-02-21 00:28:13+0100]

On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka wrote:

...

Is there any other interpretation in which the Reader monad obeys the laws?

If "selective strictness" (the seq combinator) would exclude function types, the difference between undefined and \_ -> undefined could not be observed. This reminds me of the different language levels used by the free theorem generator [1] and the discussions whether seq should have a type-class constraint..

It's not just about functions. The same holds for the lazy Writer monad, for instance. -- Roman I. Cheplyaka :: http://ro-che.info/

Ehm... why exactly don't domain products form domains? On 21 Feb 2012, at 19:44, wren ng thornton wrote:

On 2/21/12 2:17 AM, Roman Cheplyaka wrote:

...

* Sebastian Fischer [2012-02-21 00:28:13+0100]

...

On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka wrote:

...

Is there any other interpretation in which the Reader monad obeys the laws?

If "selective strictness" (the seq combinator) would exclude function types, the difference between undefined and \_ -> undefined could not be observed. This reminds me of the different language levels used by the free theorem generator [1] and the discussions whether seq should have a type-class constraint..

It's not just about functions. The same holds for the lazy Writer monad, for instance.

That's a similar sort of issue, just about whether undefined == (undefined,undefined) or not. If the equality holds then tuples would be domain products[1], but domain products do not form domains! In order to get a product which does form a domain, we'd need to use the smash product[2] instead. Unfortunately we can't have our cake and eat it too (unless we get rid of bottom entirely).

Both this issue and the undefined == (\_ -> undefined) issue come down to whether we're allowed to eta expand functions or tuples/records. While this is a well-studies topic, I don't know that anyone's come up with a really pretty answer to the dilemma.

[1] Also a category-theoretic product.

[2] Aka: data SmashProduct a b = SmashProduct !a !b

-- Live well, ~wren

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

22.02.2012, 09:30, "wren ng thornton" :

On 2/21/12 11:27 AM, MigMit wrote:

...

 Ehm... why exactly don't domain products form domains?

One important property of domains[1] is that they have a unique bottom element. Given domains A and B, let us denote the domain product as:

     (A,B) def= { (a,b) | a <- A, b <- B }

Which will inherit an ordering in the obvious/free way from the domain orderings on A and B. Since both A and B are domains, they have bottom elements:

     exists a0:A. forall a:A. (a0  <=_A  a)      exists b0:B. forall b:B. (b0  <=_B  b)

However, there is no free ordering on:

     { (a0,b) | b <- B } \cup { (a,b0) | a <- A }

What? By definition, since, a0 <= a and b0 <= b, we have (a0, b0) <= (a0, b) and (a0, b0) <= (a0, b0), so, (a0, b0) is clearly the bottom of A\times B.

So all of those are minimal elements of (A,B) but none of them is a unique minimum; hence (A,B) is not a domain.

The smash product gets around this because it takes all those elements and makes them equal, just like a strict tuple would in Haskell.

[1] This is in the sense of domain theory. It has nothing (per se) to do with the many other uses of the term "domain" in mathematics.

Sorry, isn't the domain theory a part of mathematics?

22.02.2012, 11:20, "wren ng thornton" :

On 2/22/12 1:45 AM, Miguel Mitrofanov wrote:

...

...

 However, there is no free ordering on:

       { (a0,b) | b<- B } \cup { (a,b0) | a<- A }  What? By definition, since, a0<= a and b0<= b, we have (a0, b0)<= (a0, b) and (a0, b0)<= (a0, b0), so, (a0, b0) is clearly the bottom of A\times B.

Sorry, the ordering relation on domain products is defined by:

     (a1,b1) <=_(A,B) (a2,b2) if and only if a1 <=_A a2 and b1 <=_B b2

So, you're agreeing with me? a0 <=_A a, b0 <=_B b0, so (a0, b0) <=_(A,B) (a, b0). Right?

On Tue, Feb 21, 2012 at 10:44 AM, wren ng thornton wrote:

That's a similar sort of issue, just about whether undefined == (undefined,undefined) or not. If the equality holds then tuples would be domain products[1], but domain products do not form domains! ... [1] Also a category-theoretic product.

This doesn't make much sense to me, either. If it's a category theoretic product in a category of domains, then the product must be a domain, no?

In order to get a product which does form a domain, we'd need to use the smash product[2] instead. Unfortunately we can't have our cake and eat it too (unless we get rid of bottom entirely).

You don't have to get rid of bottom entirely (I think). If you make matches against products irrefutable, then you're again in the situation of seq being the only thing able to distinguish between _|_ and (_|_, _|_), so we could keep the current implementation (which is efficient) without it being possible to observe within the language. You just have to make seq not be magic on products. Miranda did this, except it still had a seq which exposed the lie. The problem with this is that you can easily build up a product that is a bunch of thunks and cause a stack overflow; I _think_ that's more of a concern than doing the same with a function. So in practice it might be harder to do without seq on tuples. -- Dan

On Wed, Feb 22, 2012 at 1:40 AM, wren ng thornton wrote:

It's a category-theoretic product, but not for the category of domains. Let Set be the category of sets and set-theoretic functions. And let pDCPO be the category of (pointed) domains and their homomorphisms.

The (domain-theoretic) domain product was discussed in my previous message to MigMit. It's a category-theoretic product in Set (among other categories) because the necessary morphisms exist and they satisfy the necessary equations. Moreover, in Set the domain product coincides with the cartesian product (we just forget about the orderings on the input domains and the resulting product). Hence, since the cartesian product is a category-theoretic product for Set, we know that the domain product must be a category-theoretic product in Set.

Well, like Miguel, I don't see the problem with choosing the ordering: (a,b) <= (a', b') iff a <= a' and b <= b' This makes (a0, b0) the bottom element. The only difference with Haskell's tuple types is that it lacks an extra element below (a0, b0); it's unlifted. It also seems to me that this _is_ the correct product for domains, unless I'm still sketchy on what you mean by domain. I don't think it matters that we're only considering strict homomorphisms.

Conversely, the smash product is a category-theoretic product in pDCPO, but not in Set. Since every domain homomorphism must map bottoms to bottoms, it follows that f(d0) = a0 and g(d0) = b0. From this we have the necessary continuity to ensure that C, pi_A, and pi_B all exist in pDCPO. However, since there exist set-theoretic functions f and g which do not have that special property, the smash product is going to lose information about the non-bottom component of the product and so it cannot satisfy the necessary category-theoretic equations (in Set).

The smash product is not a product for domains (in general), either. You are not allowed to throw away the components for such a product, because given a homomorphism f that maps everything to a0, pi_B . maps everything to b0, regardless of what g is. -- Dan

On 2/21/12 11:54 AM, Dan Doel wrote:

You don't have to get rid of bottom entirely (I think). If you make matches against products irrefutable, then you're again in the situation of seq being the only thing able to distinguish between _|_ and (_|_, _|_), so we could keep the current implementation (which is efficient) without it being possible to observe within the language. You just have to make seq not be magic on products. Miranda did this, except it still had a seq which exposed the lie.

I thought Miranda identified _|_ with (_|_,_|_) ...though I admit I never really played around with Miranda. In any case, the point is that the weirdness of Haskell's products and function spaces are related around this issue of eta expansion. Haskell's sums are also weird (they're not category-theoretic coproducts), but that's not clearly an issue with eta. When it comes to practical utility, I think the choices Haskell made are quite nice. I'd love for smash products to have built-in syntax like tuples do, so I could use them cleanly rather than doing (((,) $! a) $! b) or defining my own ADT for them; but I understand entirely about why the Haskell committee decided that having two different versions of products/tuples would lead to API bloat and user confusion. However, while Haskell's choices are quite nice from a practical perspective, when it comes to theoretical rigor they're quite ugly. And that's the issue we're running into here when trying to figure out a theoretically sound way of defining how monads should behave with respect to bottoms. -- Live well, ~wren