Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-22 Thread Miguel Mitrofanov
22.02.2012, 11:20, wren ng thornton w...@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,

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-22 Thread wren ng thornton
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

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-22 Thread wren ng thornton
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

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-22 Thread wren ng thornton
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.

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-21 Thread wren ng thornton
On 2/21/12 2:17 AM, Roman Cheplyaka wrote: * Sebastian Fischerfisc...@nii.ac.jp [2012-02-21 00:28:13+0100] On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyakar...@ro-che.info wrote: Is there any other interpretation in which the Reader monad obeys the laws? If selective strictness (the seq

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-21 Thread MigMit
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 Fischerfisc...@nii.ac.jp [2012-02-21 00:28:13+0100] On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyakar...@ro-che.info wrote: Is

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-21 Thread Dan Doel
On Tue, Feb 21, 2012 at 10:44 AM, wren ng thornton w...@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

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-21 Thread 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

Re: [Haskell-cafe] Monad laws in presence of bottoms

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

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-21 Thread Miguel Mitrofanov
22.02.2012, 09:30, wren ng thornton w...@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:    

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-21 Thread wren ng thornton
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

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-21 Thread 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

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-21 Thread Dan Doel
On Wed, Feb 22, 2012 at 1:40 AM, wren ng thornton w...@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

[Haskell-cafe] Monad laws in presence of bottoms

2012-02-20 Thread Roman Cheplyaka
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 () /=

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-20 Thread Sebastian Fischer
On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka r...@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

Re: [Haskell-cafe] Monad laws in presence of bottoms

2012-02-20 Thread Roman Cheplyaka
* Sebastian Fischer fisc...@nii.ac.jp [2012-02-21 00:28:13+0100] On Mon, Feb 20, 2012 at 7:42 PM, Roman Cheplyaka r...@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

[Haskell-cafe] Monad Laws and Do Notation

2011-09-21 Thread diazepan
I've got this expression expression = do w - hello y - to you return w I wanna know how can I reduce it using monad laws -- View this message in context: http://haskell.1045720.n5.nabble.com/Monad-Laws-and-Do-Notation-tp4828598p4828598.html Sent from the Haskell -

Re: [Haskell-cafe] Monad Laws and Do Notation

2011-09-21 Thread Ivan Lazar Miljenovic
On 22 September 2011 11:46, diazepan spanishbizar...@yahoo.com wrote: I've got this expression expression = do        w - hello        y - to you        return w I wanna know how can I reduce it using monad laws I don't think you can: the best you can do is minimise it with other monadic

Re: [Haskell-cafe] Monad laws

2010-03-03 Thread David Sabel
Hi, thanks for all the comments. In ghc 6.12.1 the behavior is strange: If f is defined in the interpreter via let, then the seq-expression converges GHCi, version 6.12.1: http://www.haskell.org/ghc/ :? for help let f = \x - (undefined::IO Bool) seq (f True) True True but if you build a

Re: [Haskell-cafe] Monad laws

2010-03-03 Thread Yitzchak Gale
Hi Luke, I wrote: For this reason, I consider it a bug in GHC that return :: IO a is lazy. Luke Palmer wrote: Wait a minute...   return undefined = const (return 42) = const (return 42) undefined = return 42 But if return undefined = undefined, then that equals;  undefined = const

[Haskell-cafe] Monad laws

2010-03-02 Thread David Sabel
Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad): return a = f ≡ f a I figured out that there is the distinguishing context (seq [] True) which falsifies the law for a and f defined below let a = True let f = \x - (undefined::IO Bool) seq

Re: [Haskell-cafe] Monad laws

2010-03-02 Thread Luke Palmer
On Tue, Mar 2, 2010 at 1:17 PM, David Sabel sa...@ki.informatik.uni-frankfurt.de wrote: Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad): return a = f ≡ f a I figured out that there is the distinguishing context (seq [] True) which falsifies

Re: [Haskell-cafe] Monad laws

2010-03-02 Thread Andrés Sicard-Ramírez
On 2 March 2010 15:44, Luke Palmer lrpal...@gmail.com wrote: On Tue, Mar 2, 2010 at 1:17 PM, David Sabel sa...@ki.informatik.uni-frankfurt.de wrote: Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad): return a = f ≡ f a I figured out

Re: [Haskell-cafe] Monad laws

2010-03-02 Thread Yitzchak Gale
David Sabel wrote: when checking the first monad law (left unit) for the IO-monad (and also for the ST monad): I figured out that there is the distinguishing context (seq [] True) which falsifies the law... It's worse than that - Haskell types and functions do not even form a category under

Re: [Haskell-cafe] Monad laws

2010-03-02 Thread Luke Palmer
On Tue, Mar 2, 2010 at 4:37 PM, Yitzchak Gale g...@sefer.org wrote: For this reason, I consider it a bug in GHC that return :: IO a is lazy. Wait a minute... return undefined = const (return 42) = const (return 42) undefined = return 42 But if return undefined = undefined, then that

Re: [Haskell-cafe] Monad laws

2006-09-08 Thread Duncan Coutts
On Fri, 2006-09-08 at 01:43 -0400, Albert Lai wrote: Deokhwan Kim [EMAIL PROTECTED] writes: What is the practical meaning of monad laws? 1. (return x) = f == f x 2. m = return == m 3. (m = f) = g == m (\x - f x = g) I offer to re-write the laws in do-notation. (Please view

Re: [Haskell-cafe] Monad laws

2006-09-07 Thread Brian Hulley
Deokhwan Kim wrote: What is the practical meaning of monad laws? (M, return, =) is not qualified as a category-theoretical monad, if the following laws are not satisfied: 1. (return x) = f == f x 2. m = return == m 3. (m = f) = g == m (\x - f x = g) But what practical problems can

Re: [Haskell-cafe] Monad laws

2006-09-07 Thread Lennart Augustsson
Brian, Are you really sure Haskell compilers do that optimization? I would regard a compiler that does optimizations that are justified by laws that the compiler cannot check as broken. -- Lennart On Sep 7, 2006, at 08:50 , Brian Hulley wrote: Deokhwan Kim wrote: What is the

Re: [Haskell-cafe] Monad laws

2006-09-07 Thread Robert Dockins
On Sep 7, 2006, at 9:04 AM, Lennart Augustsson wrote: Brian, Are you really sure Haskell compilers do that optimization? I would regard a compiler that does optimizations that are justified by laws that the compiler cannot check as broken. What, like list fusion? ;-) Although, more

Re: [Haskell-cafe] Monad laws

2006-09-07 Thread Brian Hulley
Lennart Augustsson wrote: On Sep 7, 2006, at 08:50 , Brian Hulley wrote: Deokhwan Kim wrote: What is the practical meaning of monad laws? Afaiu the monad laws are needed so the compiler can do various optimizations, especially in regard to the do notation. Consider: g c = do

Re: [Haskell-cafe] Monad laws

2006-09-07 Thread ajb
G'day all. Quoting Deokhwan Kim [EMAIL PROTECTED]: What is the practical meaning of monad laws? Interesting philosophical question. There will be an article on this topic in the next The Monad.Reader, so watch this space. But what practical problems can unsatisfying them cause? Pretty much

[Haskell-cafe] Monad laws

2006-09-06 Thread Deokhwan Kim
What is the practical meaning of monad laws? (M, return, =) is not qualified as a category-theoretical monad, if the following laws are not satisfied: 1. (return x) = f == f x 2. m = return == m 3. (m = f) = g == m (\x - f x = g) But what practical problems can unsatisfying them cause?