headers
Roman Cheplyaka | 20 Feb 19:42
Gravatar

Monad laws in presence of bottoms

I just realised that many common monads do not obey the monad laws when
it comes to bottoms.

E.g. for the Reader monad:

  undefined >>= return /= undefined
  return () >>= undefined /= undefined
  return () >>= const undefined /= undefined
  return undefined >>= \x -> case x of () -> return () /= undefined

Not a long time ago David Barbour argued on this list that bottoms
should be ignored when checking the monad laws.

Is that the commonly accepted interpretation of the laws?
Is there any other interpretation in which the Reader monad obeys the
laws?

--

-- 
Roman I. Cheplyaka :: http://ro-che.info/
Permalink | Reply |
headers
Sebastian Fischer | 21 Feb 00:28
Picon
Favicon

Re: Monad laws in presence of bottoms

On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka <roma <at> ro-che.info> 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..

Sebastian

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
Roman Cheplyaka | 21 Feb 08:17
Gravatar

Re: Monad laws in presence of bottoms

* Sebastian Fischer <fischer <at> nii.ac.jp> [2012-02-21 00:28:13+0100]
> On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka <roma <at> ro-che.info> 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/
Permalink | Reply |
headers
wren ng thornton | 21 Feb 16:44

Re: Monad laws in presence of bottoms

On 2/21/12 2:17 AM, Roman Cheplyaka wrote:
> * Sebastian Fischer<fischer <at> nii.ac.jp>  [2012-02-21 00:28:13+0100]
>> On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka<roma <at> ro-che.info>  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
Permalink | Reply |
headers
MigMit | 21 Feb 17:27
Picon
Favicon

Re: Monad laws in presence of bottoms

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<fischer <at> nii.ac.jp>  [2012-02-21 00:28:13+0100]
>>> On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka<roma <at> ro-che.info>  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 <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
wren ng thornton | 22 Feb 06:30

Re: Monad laws in presence of bottoms

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 }

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.

--

-- 
Live well,
~wren
Permalink | Reply |
headers
Miguel Mitrofanov | 22 Feb 07:45
Picon
Favicon

Re: Monad laws in presence of bottoms


22.02.2012, 09:30, "wren ng thornton" <wren <at> freegeek.org>:
> 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?

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
wren ng thornton | 22 Feb 08:20

Re: Monad laws in presence of bottoms

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

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

Sure, domain theory is a part of mathematics, but the term "domain" is 
used to mean a bunch of different and largely unrelated things. For example:

* in type theory and set theory the "domain" of a function is the set of 
inputs on which it's defined

* in domain theory a "domain" is a partial order with a least element 
and the property that every non-empty countable chain has a least upper 
bound

* in ring theory a "domain" is is a ring which has no left nor right 
zero-divisors

* in analysis a "domain" is any connected open subset of a 
finite-dimensional vector space

etc.

--

-- 
Live well,
~wren
Permalink | Reply |
headers
Miguel Mitrofanov | 22 Feb 08:58
Picon
Favicon

Re: Monad laws in presence of bottoms


22.02.2012, 11:20, "wren ng thornton" <wren <at> freegeek.org>:
> 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?

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
wren ng thornton | 22 Feb 09:36

Re: Monad laws in presence of bottoms

On 2/22/12 2:20 AM, wren ng thornton wrote:
> 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

Sorry, I misread what you wrote. Yes, of course you're correct. I can't 
recall off-hand why it is that domain products break things; I'll have 
to look it up.

--

-- 
Live well,
~wren
Permalink | Reply |
headers
Dan Doel | 21 Feb 17:54
Picon

Re: Monad laws in presence of bottoms

On Tue, Feb 21, 2012 at 10:44 AM, wren ng thornton <wren <at> freegeek.org> 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
Permalink | Reply |
headers
wren ng thornton | 22 Feb 07:40

Re: Monad laws in presence of bottoms

On 2/21/12 11:54 AM, Dan Doel wrote:
> On Tue, Feb 21, 2012 at 10:44 AM, wren ng thornton<wren <at> freegeek.org>  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?

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 category-theoretic product of A and B is just some triple (C, pi_A : 
C -> A, pi_B : C -> B) such that forall D, forall f : D -> A, and forall 
g : D -> B, there exists a unique h : D -> C such that f = pi_A . h and 
g = pi_B . h  ---in other words, it's the limit of a functor from the 
category with two objects and no morphisms which maps one object to A 
and the other object to B.

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.

However, the domain product is not a category-theoretic product in 
pDCPO. First off, the objects in pDCPO are domains, but since the domain 
product of A and B has no bottom it can't be a domain, so it can't be an 
object in pDCPO. Moreover, the morphisms in pDCPO will preserve the 
domain structure--- but there's no way to do that for a map from some 
domain C to the domain product of A and B, because there's no way to map 
the bottom of C to the bottom of the domain product (because there isn't 
one!).

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

For more on the category-theoretic study of domain theory, see 
<http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf>. You can search 
the pdf for "pointed dcpo" to jump to the relevant sections. Of course 
there are many different category-theoretic formalizations of domain 
theory, pDCPO is just one of them. To get a survey of the terrain, you 
may want to take a look at 
<http://seclab.web.cs.illinois.edu/wp-content/uploads/2011/04/Gunter85.pdf>.

For a more direct introduction to domain theory and its application to 
lazy languages, see Geoffrey Burn's _Lazy Functional Languages: Abstract 
Interpretation and Compilation_.

--

-- 
Live well,
~wren
Permalink | Reply |
headers
Dan Doel | 22 Feb 08:37
Picon

Re: Monad laws in presence of bottoms

On Wed, Feb 22, 2012 at 1:40 AM, wren ng thornton <wren <at> freegeek.org> 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 .
<f,g> maps everything to b0, regardless of what g is.

-- Dan
Permalink | Reply |
headers
wren ng thornton | 22 Feb 09:49

Re: Monad laws in presence of bottoms

On 2/22/12 2:37 AM, Dan Doel wrote:
> unless I'm still sketchy on what you mean by domain. I don't think it
> matters that we're only considering strict homomorphisms.

I think part of the problem is that there are many different ideas of 
what exact properties a domain has. The one I'm most familiar with are 
consistently-complete \omega-algebraic cpos, but they're far from the 
only option.

Also, I may be misremembering my facts about how the domain theory and 
the category theory fit together. I do recall that domain products break 
some sorts of desirable properties, but that may be due to something 
else about them.

--

-- 
Live well,
~wren
Permalink | Reply |
headers
wren ng thornton | 22 Feb 07:53

Re: Monad laws in presence of bottoms

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
Permalink | Reply |
headers
wren ng thornton | 22 Feb 20:40

Re: Monad laws in presence of bottoms

On 2/21/12 10:44 AM, wren ng thornton wrote:
> 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

Bah, I don't know why my wires were crossed yesterday. It's *coproducts* 
where the category-theoretic and domain-theoretic definitions are at 
odds. For *products*, the issues are just about whether the category is 
cartesian closed and the like (i.e., divergence between products and 
tensors). Up too late with too little coffee, no doubt. My apologies for 
causing confusion.

--

-- 
Live well,
~wren
Permalink | Reply |

Gmane