Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
Hi Alexander, Thanks for commenting on this issue. On 21 June 2012 16:34, Alexander Solla alex.so...@gmail.com wrote: These nits don't need to be picked. The theory of equivalence relations is extremely well understood. This is a topic covered by the sophomore mathematics level. I did not say that the theory of equivalence relations is not well understood. All I have said is that [1] demonstrates that people have different ideas as to what an Eq instance should satisfy. And, yes, it is all about picking a suitable notion for Eq and designating other (possibly related and useful) notions for other type classes. Being an equivalence relation is just one of them. But, to be honest, I find this rather confusing. I thought, and I suspect I am not the only one, Eq was about equality and not about equivalence. I have just had a look at the Haskell 2010 and Prelude. When it comes to the Eq type class, precise definition of what its instances should satisfy is missing. But crucially, both texts talk about equality and not about equivalence. The word equivalence is not even mentioned in the context of the Eq class. This may sound to much of a technical/terminological point, but I believe the terminology we use is important, especially, in the context of Haskell where formal reasoning about programs is not unusual. Also, I find the use of the == symbol to denote equivalence rather than equality rather questionable. The way lhs2tex typesets the == symbol, makes this even more questionable. Again this may sound to much of a symbolical point, but I believe the symbols we use are important, especially, in the context of Haskell where formal reasoning about programs is not unusual. I would like to kindly ask you to provide a reference designating Eq for equivalence and not for equality and stating that only being an equivalence relation is required. Thanks in advance. Why not use the Eq type class (as the current Haskell 2010 and Prelude texts suggest) for a stronger notion of equality (observational equality with a suitable notion of observation is one candidate), and designate weaker notions such as being just an equivalence relation to different type classes? But, my opinion is that if you can write a pure function f that can tell them apart (i.e., f x /= f y), I find it a very strange notion of equality. There's your problem. Unfortunately, this is not only my problem. In addition to mailing list discussions I referred to in the earlier email sent to Derek [2,3] (these discussions are about functor and monad instances for sets), a paper by John Hughes about Restricted Data Types in Haskell [4] and a draft by Oleg Kiselyov about Restricted Monads [5] are also relevant. Both, John and Oleg, use monad instances for sets as primary examples. However, their properties can be easily violated by Eq instances provided by Derek and Dan. John's and Oleg's constructions, for the monad laws to hold, rely on Eq to be equality and not just an equivalence relation. It is straight-forward to generate an equivalence relation that can tell things apart with respect to a different equivalence relation. Equivalence relations do not need to agree! See above, I thought Eq was about equality and not about equivalence. If you really want to keep distinct equivalence relations apart semantically, just use a newtype wrapper to explicitly name the relation. This is certainly possible. Can you point to a library or a document that exemplifies this approach for dealing with different notions of equality and/or equivalence. Maybe there are already conventions in place that I am not aware of. Thanks in advance. I am not saying that this is a trivial undertaking, but would be a more principled approach. It would require the Haskell community and, especially, standard library and language specification developers to agree on a suitable notion of equality that Eq instances should satisfy. That has already happened. A relation merely has to satisfy the equivalence relation axioms. Can you provide a reference? When this was agreed and where is this specified? Thanks in advance, George [1] http://www.haskell.org/pipermail/haskell-cafe/2008-March/thread.html [2] http://www.haskell.org/pipermail/haskell-cafe/2010-July/080977.html [3] http://haskell.1045720.n5.nabble.com/Functor-instance-for-Set-td5525789.html [4] http://www.cs.utexas.edu/users/ham/richards/FP%20papers/restricted-datatypes.pdf [5] http://okmij.org/ftp/Haskell/types.html#restricted-datatypes ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
Hi Derek, Thanks for providing the executable example that demonstrates your point. It is an interesting one. See my response below. I think it takes us into the discussion as to what constitutes reasonable/law abiding instances of Eq and Ord and what client code that uses Eq and Ord instances can assume. To give out my point in advance, Eq and Ord instances similar to yours (i.e., those that proclaim two values as equal but at the same time export or allow for function definitions that can observe that they are not equal; that is, to tell them apart) not only break useful properties of the Data.Set.Monad wrapper but they also break many useful properties of the underlaying Data.Set, and many other standard libraries and functions. On 20 June 2012 04:03, Derek Elkins derek.a.elk...@gmail.com wrote: This is impressive because it's false. The whole point of my original response was to justify Dan's intuition but explain why it was misled in this case. No, In my opinion, it is not false. The fact that you need to wrap the expression between fmap f and fmap g suggests that the problem is with mapping the functions f and g and not with toList and fromList as you suggest. See below for clarifications. Let us concentrate on the ex4 and ex6 expressions in your code. These two most clearly demonstrate the issue. import Data.Set.Monad data X = X Int Int deriving (Show) instance Eq X where X a _ == X b _ = a == b instance Ord X where compare (X a _) (X b _) = compare a b f (X _ b) = X b b g (X _ b) = X 1 b xs = Prelude.map (\x - X x x) [1..5] ex4 = toList $ fmap f . fmap g $ fromList xs ex6 = toList $ fmap f . fromList . toList . fmap g $ fromList xs print ex4 gives us [X 1 1,X 2 2,X 3 3,X 4 4,X 5 5] and print ex6 gives us [X 5 5] From the first look, it looks like that (fromList . toList) is not identity. But if tested and checked separately it is. Maybe something weird is going on with (fmap f) and (fmap g) and/or their composition. Before we dive into that let us try one more example: ex7 = toList $ fmap f . (empty `union`) . fmap g $ fromList xs print ex7 just like ex6 gives us [X 5 5] should we assume that (empty `union`) is not identity either? This hints that, probably something is wrong with (fmap f), (fmap g), or their composition. Let us check. If one symbolically evaluates ex4 and ex6 (I did it with pen and paper and I am too lazy to type it here), one can notice that: ex4 boils down to evaluating Data.Set.map (f . g) (Data.Set.fromList xs) while ex6 boils down to evaluating Data.Set.map f (Data.Set.map g (Data.Set.fromList xs)) (BTW, is not it great that Data.Set.Monad managed to fuse f and g for ex4) So for your Eq and Ord instances and f and g functions the following does not hold for the underlaying Data.Set library: map f . map g = map (f . g) So putting identity functions like (fromList . toList) or (empty `union`) prevents the fusion and allows one to observe that (map f . map g) is not the same as (map (f . g)) for the underlaying Data.Set and for your particular choice of f and g. This violates the second functor law. So does this mean that I (and few other people [1, 2]) should not have attempted to turn Set into a functor? I do not think so. (BTW, what distinguishes the approach used in Data.Set.Monad from other efforts is that it does not require changes in the definitions of standard Functor and Monad type classes). In my opinion, the problem here lies with the Eq and Ord instances of the X data type AND with the function f that can tell apart two values that are proclaimed to be equal by the Eq instance. As I said, such instances and accompanied functions not only break useful properties of Data.Set.Monad, but also useful properties of the library that underlies it (i.e., the original Data.Set), and possibly many other standard libraries and functions (see [4]). Putting the functor laws aside, there are even more fundamental set-oriented properties that can be broken by Ord instances that are not law abiding. See the following GHCi session taken from [3]: Prelude import Data.Set Prelude Data.Set let x = fromList [0, -1, 0/0, -5, -6, -3] :: Set Float Prelude Data.Set member 0 x True Prelude Data.Set let x' = insert (0/0) x Prelude Data.Set member 0 x' False Is this because Data.Set is broken? No, in my opinion, this is because the Ord instance of Float does not satisfy the Ord laws (about total order). To summarise, in my opinion the problem here lies with the fact that the Eq and Ord instances for the X data type proclaim two values as equal when it can be easily observed that they are not equal (in this case with the function f). Note, that the functions of Data.Set.Monad and Data.Set rely on your Eq and Ord instances. Of course, there would be nothing wrong with the Eq and Ord instances for X as long as you would export it as abstract data type and you would not export functions that can observe two values to be different when
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
Hi Dan,
On 21 June 2012 04:21, Dan Burton danburton.em...@gmail.com wrote:
Hi George,
I didn't have access to my computer over the weekend, so I apologize for not
actually running the examples I provided. I was simply projecting what I
thought could reasonably be assumed about the behavior of a Set.
Derek attempted to clarify your points and also provided executable examples.
I think his code is closely related and raises similar issues to what
you have just provided.
Data.Set.Monad's departure from those assumptions is a double-edged sword,
and so I'd just like to clarify a couple things.
I disagree on this. I think these particular Eq and Ord instances are
double-edged swords (and rather dangerous ones) especially in the
set-oriented code where almost every set-oriented function relies on
correct behaviour of functions related to equality and ordering.
As I have pointed out in my previous email (in response to Derek's
email) these particular instances not only break useful properties of
Data.Set.Monad, but they also break useful properties of the
underlaying Data.Set library (and useful properties of many other
standard libraries and functions too, see [1]).
Regarding antisymmetry, if I also define
instance Ord Foo where
(==) = (==) `on` a
then would that count as satisfying the law?
Probably, you mean here Eq instead of Ord.
If a = b and b = a then a = b (antisymmetry)
It all depends on what one means by =. Opinions differ on this, see
[1]. If we mean ==, which is a function to Bool, from the Eq class,
then it does satisfy the antisymmetry law.
But in this case, the question arises what are the laws that Eq
instances should satisfy.
Should it be that x == y implies x = y? But once again what does =
mean here. It depends on who you ask (once again see [1]).
But, my opinion is that if you can write a pure function f that can
tell them apart (i.e., f x /= f y), I find it a very strange notion of
equality. And this is actually what breaks many useful properties of
Data.Set.Monad, as well as, Data.Set.
In any event, I find it an amusing coincidence that Data.Set.Monoid does
essentially the same thing as Foo: it retains some extra information, and
provides an Eq instance that asserts equality modulo dropping the extra
information.
No, it does not. Data.Set.Monad hides the internal representation of
the Set data type and does not export functions that can inspect its
internal representation. (There are a few functions like showTree that
allow inspection of the structure, but such functions are clearly
marked).
In other words, the Set data type is exported as an abstract data type.
In contrast, the structure of the Foo data type is exposed and
functions are explicitly provided that tell apart two values that are
proclaimed to be equal by the Eq instance.
As it turns out (demonstrated by Derek and yourself) such questionable
Eq instances can be used to confuse the Data.Set.Monad and Data.Set
libraries.
So I have a question and a concern. Loading this file into ghci:
hpaste.org/70245
ghci foo1 == foosTransform1
True
ghci foo2 == foosTransform2
False
given x == y, where x and y are Sets, we cannot guarantee that fmap f x ==
fmap f y, due to the extra information retained for the sake of obeying
functor laws.
My question is this: how does the library manage to obey functor laws?
It simply assumes that (map f) . (map g) = map (f . g) for the
underlaying primitive set type and evaluates ((fmap f) . (fmap g)) as
(fmap (f . g)). You cannot directly see the aforementioned evaluation
steps in the run function. Instead, please expand the definition of
fmap in terms of Bind and Return and follow the evaluation rules using
Bind's associativity and Return's left identity.
My concern is this: the aforementioned behavior should be clearly documented
in the haddocks. Presumably, people will not know about the extra
information being retained. The following, out of context (where most
debugging happens), could be quite confusing:
ghci foosTransform1
fromList [Foo {a = 1, b = 4}]
ghci fmap restoreA foosTransform1
fromList [Foo {a = 1, b = 1},Foo {a = 2, b = 2},Foo {a = 3, b = 3},Foo {a =
4, b = 4}]
The data seems to pop out of nowhere. Even if Ord instances like the one for
Foo shouldn't exist, they almost certainly will anyways, because the Haskell
type system doesn't prevent them. Users of the library should be informed
accordingly.
I agree, it should be documented that the library relies on (map f) .
(map g) = map (f . g) to hold for Data.Set, for those (I would still
call them questionable) Eq and Ord instances where the above property
does not hold things break in the Data.Set.Monad library as well.
Having said that, questionable Eq instances break so many other
functions in other standard libraries [1], that documenting every such
case would be a significant undertaking. My opinion is to informally
impose restrictions on Eq and Ord instances instead,
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
On Thu, Jun 21, 2012 at 7:00 AM, George Giorgidze giorgi...@gmail.comwrote: Regarding antisymmetry, if I also define instance Ord Foo where (==) = (==) `on` a then would that count as satisfying the law? Probably, you mean here Eq instead of Ord. If a = b and b = a then a = b (antisymmetry) It all depends on what one means by =. Opinions differ on this, see [1]. If we mean ==, which is a function to Bool, from the Eq class, then it does satisfy the antisymmetry law. But in this case, the question arises what are the laws that Eq instances should satisfy. Should it be that x == y implies x = y? But once again what does = mean here. It depends on who you ask (once again see [1]). These nits don't need to be picked. The theory of equivalence relations is extremely well understood. This is a topic covered by the sophomore mathematics level. But, my opinion is that if you can write a pure function f that can tell them apart (i.e., f x /= f y), I find it a very strange notion of equality. There's your problem. It is straight-forward to generate an equivalence relation that can tell things apart with respect to a different equivalence relation. Equivalence relations do not need to agree! If you really want to keep distinct equivalence relations apart semantically, just use a newtype wrapper to explicitly name the relation. I am not saying that this is a trivial undertaking, but would be a more principled approach. It would require the Haskell community and, especially, standard library and language specification developers to agree on a suitable notion of equality that Eq instances should satisfy. That has already happened. A relation merely has to satisfy the equivalence relation axioms. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
On Thu, Jun 21, 2012 at 8:30 AM, George Giorgidze giorgi...@gmail.com wrote: Hi Derek, Thanks for providing the executable example that demonstrates your point. It is an interesting one. See my response below. I think it takes us into the discussion as to what constitutes reasonable/law abiding instances of Eq and Ord and what client code that uses Eq and Ord instances can assume. To give out my point in advance, Eq and Ord instances similar to yours (i.e., those that proclaim two values as equal but at the same time export or allow for function definitions that can observe that they are not equal; that is, to tell them apart) not only break useful properties of the Data.Set.Monad wrapper but they also break many useful properties of the underlaying Data.Set, and many other standard libraries and functions. I will readily admit that the Ord instance arguably does not satisfy the laws one would want (though it is consistent with the Eq instance). It arguably is supposed to produce a total order which it does not. However, Eq is only required to be an equivalence relation (and even that is stretching the definition of required), and the Eq instance is certainly an equivalence relation. Furthermore, the only reason your library requires an Ord instance is due to the underlying Data.Set requiring it. You could just as well use a set implementation that didn't require Ord and the same issue would occur. I mention this to remove the bad Ord instance from consideration. For me saying two Haskell expressions are equal means observation equality. I.e. I can -always- substitute one for the other in any context. I tolerate equal meaning equal modulo bottom, because unless you are catching asynchronous exceptions, which Haskell 2010 does not support, the only difference is between whether you get an answer or not, not what that answer is if you get it which is only so harmful. For Data.Set.Monad, fmap f . fmap g = fmap (f . g) holds (at least modulo bottom) for all f and g as required by the Functor laws. I have no problem if you want to say fromList . toList = id -given- (==) is the identity relation on defined values, but omitting the qualification is misleading and potentially dangerous. The Haskell Report neither requires nor enforces that those relations hold, which is particularly underscored by the fact, as you yourself demonstrated that even -standard- types fail to satisfy even the laws that you perhaps can interpret the Haskell Report as requiring. There have been violations of type safety due to assuming instances satisfied laws that they didn't. On 20 June 2012 04:03, Derek Elkins derek.a.elk...@gmail.com wrote: This is impressive because it's false. The whole point of my original response was to justify Dan's intuition but explain why it was misled in this case. No, In my opinion, it is not false. The fact that you need to wrap the expression between fmap f and fmap g suggests that the problem is with mapping the functions f and g and not with toList and fromList as you suggest. See below for clarifications. Let us concentrate on the ex4 and ex6 expressions in your code. These two most clearly demonstrate the issue. import Data.Set.Monad data X = X Int Int deriving (Show) instance Eq X where X a _ == X b _ = a == b instance Ord X where compare (X a _) (X b _) = compare a b f (X _ b) = X b b g (X _ b) = X 1 b xs = Prelude.map (\x - X x x) [1..5] ex4 = toList $ fmap f . fmap g $ fromList xs ex6 = toList $ fmap f . fromList . toList . fmap g $ fromList xs print ex4 gives us [X 1 1,X 2 2,X 3 3,X 4 4,X 5 5] and print ex6 gives us [X 5 5] From the first look, it looks like that (fromList . toList) is not identity. But if tested and checked separately it is. Maybe something weird is going on with (fmap f) and (fmap g) and/or their composition. Before we dive into that let us try one more example: ex7 = toList $ fmap f . (empty `union`) . fmap g $ fromList xs print ex7 just like ex6 gives us [X 5 5] should we assume that (empty `union`) is not identity either? Correct. It is not. This hints that, probably something is wrong with (fmap f), (fmap g), or their composition. Let us check. If one symbolically evaluates ex4 and ex6 (I did it with pen and paper and I am too lazy to type it here), one can notice that: ex4 boils down to evaluating Data.Set.map (f . g) (Data.Set.fromList xs) while ex6 boils down to evaluating Data.Set.map f (Data.Set.map g (Data.Set.fromList xs)) (BTW, is not it great that Data.Set.Monad managed to fuse f and g for ex4) So for your Eq and Ord instances and f and g functions the following does not hold for the underlaying Data.Set library: map f . map g = map (f . g) So putting identity functions like (fromList . toList) or (empty `union`) prevents the fusion and allows one to observe that (map f . map g) is not the same as (map (f . g)) for the underlaying Data.Set and for
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
Hi George,
I didn't have access to my computer over the weekend, so I apologize for
not actually running the examples I provided. I was simply projecting what
I thought could reasonably be assumed about the behavior of a Set.
Data.Set.Monad's departure from those assumptions is a double-edged sword,
and so I'd just like to clarify a couple things.
Regarding antisymmetry, if I also define
instance Ord Foo where
(==) = (==) `on` a
then would that count as satisfying the law?
In any event, I find it an amusing coincidence that Data.Set.Monoid does
essentially the same thing as Foo: it retains some extra information, and
provides an Eq instance that asserts equality modulo dropping the extra
information.
So I have a question and a concern. Loading this file into ghci:
hpaste.org/70245
ghci foo1 == foosTransform1
True
ghci foo2 == foosTransform2
False
given x == y, where x and y are Sets, we cannot guarantee that fmap f x ==
fmap f y, due to the extra information retained for the sake of obeying
functor laws.
My question is this: how *does* the library manage to obey functor laws?
My concern is this: the aforementioned behavior should be clearly
documented in the haddocks. Presumably, people will not know about the
extra information being retained. The following, out of context (where most
debugging happens), could be quite confusing:
ghci foosTransform1
fromList [Foo {a = 1, b = 4}]
ghci fmap restoreA foosTransform1
fromList [Foo {a = 1, b = 1},Foo {a = 2, b = 2},Foo {a = 3, b = 3},Foo {a =
4, b = 4}]
The data seems to pop out of nowhere. Even if Ord instances like the one
for Foo shouldn't exist, they almost certainly will anyways, because the
Haskell type system doesn't prevent them. Users of the library should be
informed accordingly.
Dan Burton
801-513-1596
On Mon, Jun 18, 2012 at 2:40 PM, George Giorgidze giorgi...@gmail.comwrote:
Hi Dan,
Thanks for your feedback and your question regarding the functor laws.
Please try your example in GHCi and/or evaluate it by hand. The
library does not violate the functor laws.
I committed quick check properties for functor laws, as well as, laws
for other type classes to the repo. You can give it a try. It is also
possible, with a little bit of effort, to prove those properties by
hand.
Speaking of laws, BTW, your contrived Ord instance violates one of the
Ord laws. The documentation for Ord says that: The Ord class is used
for totally ordered datatypes. Your definition violates the
antisymmetry law [1]:
If a = b and b = a then a == b
by reporting two elements that are not equal as equal.
Cheers, George
[1] http://en.wikipedia.org/wiki/Totally_ordered
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
Hi Derek, Thanks for clarifying your point. You are right that (fromList . toList) = id is a desirable and it holds for Data.Set. But your suggestions that this property does not hold for Data.Set.Monad is not correct. Please check out the repo, I have just pushed a quickcheck definition for this property. With a little bit of effort, one can also prove this by hand. Let me also clarify that Data.Set.Monad exports Set as an abstract data type (i.e., the user cannot inspect its internal structure). Also the run function is only used internally and is not exposed to the users. Cheers, George On 19 June 2012 02:21, Derek Elkins derek.a.elk...@gmail.com wrote: On Jun 18, 2012 4:54 PM, George Giorgidze giorgi...@gmail.com wrote: Hi Derek, On 16 June 2012 21:53, Derek Elkins derek.a.elk...@gmail.com wrote: The law that ends up failing is toList . fromList /= id, i.e. fmap g . toList . fromList . fmap h /= fmap g . fmap h This is not related to functor laws. The property that you desire is about toList and fromList. Sorry, I typoed. I meant to write fromList . toList though that should've been clear from context. This is a law that I'm pretty sure does hold for Data.Set, potentially modulo bottom. It is a quite desirable law but, as you correctly state, not required. If you add this (non)conversion, you will get the behavior to which Dan alludes. The real upshot is that Prim . run is not id. This is not immediately obvious, but this is actually the key to why this technique works. A Data.Set.Monad Set is not a set, as I mentioned in my previous email. To drive the point home, you can easily implement fromSet and toSet. In fact, they're just Prim and run. Thus, you will fail to have fromSet . toSet = I'd, though you will have toSet . fromSet = I'd, i.e. run . Prim = id. This shows that Data.Set.Set embeds into but is not isomorphic to Data.Set.Monad.Set. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
Un-top-posted. See below. On 19 June 2012 02:21, Derek Elkins derek.a.elk...@gmail.com wrote: On Jun 18, 2012 4:54 PM, George Giorgidze giorgi...@gmail.com wrote: Hi Derek, On 16 June 2012 21:53, Derek Elkins derek.a.elk...@gmail.com wrote: The law that ends up failing is toList . fromList /= id, i.e. fmap g . toList . fromList . fmap h /= fmap g . fmap h This is not related to functor laws. The property that you desire is about toList and fromList. Sorry, I typoed. I meant to write fromList . toList though that should've been clear from context. This is a law that I'm pretty sure does hold for Data.Set, potentially modulo bottom. It is a quite desirable law but, as you correctly state, not required. If you add this (non)conversion, you will get the behavior to which Dan alludes. The real upshot is that Prim . run is not id. This is not immediately obvious, but this is actually the key to why this technique works. A Data.Set.Monad Set is not a set, as I mentioned in my previous email. To drive the point home, you can easily implement fromSet and toSet. In fact, they're just Prim and run. Thus, you will fail to have fromSet . toSet = I'd, though you will have toSet . fromSet = I'd, i.e. run . Prim = id. This shows that Data.Set.Set embeds into but is not isomorphic to Data.Set.Monad.Set. On Tue, Jun 19, 2012 at 4:02 AM, George Giorgidze giorgi...@gmail.com wrote: Hi Derek, Thanks for clarifying your point. You are right that (fromList . toList) = id is a desirable and it holds for Data.Set. But your suggestions that this property does not hold for Data.Set.Monad is not correct. Please check out the repo, I have just pushed a quickcheck definition for this property. With a little bit of effort, one can also prove this by hand. This is impressive because it's false. The whole point of my original response was to justify Dan's intuition but explain why it was misled in this case. Let me also clarify that Data.Set.Monad exports Set as an abstract data type (i.e., the user cannot inspect its internal structure). Also the run function is only used internally and is not exposed to the users. If fromList . toList = id is true for Data.Set.Set, then fromList . toList for Data.Set.Monad.Set reduces to Prim . run. I only spoke of the internal functions to get rid of the noise, but Data.Set.fromList . Data.Set.Monad.toList = run, and Data.Set.Monad.fromList . Data.Set.toList = Prim, so it doesn't matter that these are internal functions. As I said to Dan I will say to you, between Dan and myself the counter-example has already been provided, all you need to do is execute it. Here's the code, if fromList . toList = id, then ex4 should produce the same result as ex5 (and ex6). import Data.Set.Monad data X = X Int Int deriving (Show) instance Eq X where X a _ == X b _ = a == b instance Ord X where compare (X a _) (X b _) = compare a b f (X _ b) = X b b g (X _ b) = X 1 b xs = Prelude.map (\x - X x x) [1..10] -- should be a singleton ex1 = toList . fromList $ Prelude.map g xs -- should have 10 elements ex2 = toList $ fmap (f . g) $ fromList xs -- should have 1 element ex3 = toList $ fmap g $ fromList xs -- should have 10 element, fmap f . fmap g = fmap (f . g) ex4 = toList $ fmap f . fmap g $ fromList xs -- should have 1 element, we don't generate elements out of nowhere ex5 = toList $ fmap f $ fromList ex3 -- i.e. ex6 = toList $ fmap f . fromList . toList . fmap g $ fromList xs main = mapM_ print [ex1, ex2, ex3, ex4, ex5, ex6] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
Hi Dan,
Thanks for your feedback and your question regarding the functor laws.
Please try your example in GHCi and/or evaluate it by hand. The
library does not violate the functor laws.
I committed quick check properties for functor laws, as well as, laws
for other type classes to the repo. You can give it a try. It is also
possible, with a little bit of effort, to prove those properties by
hand.
Speaking of laws, BTW, your contrived Ord instance violates one of the
Ord laws. The documentation for Ord says that: The Ord class is used
for totally ordered datatypes. Your definition violates the
antisymmetry law [1]:
If a = b and b = a then a == b
by reporting two elements that are not equal as equal.
Cheers, George
[1] http://en.wikipedia.org/wiki/Totally_ordered
On 16 June 2012 09:47, Dan Burton danburton.em...@gmail.com wrote:
Convenience aside, doesn't the functor instance conceptually violate some
sort of law?
fmap (const 1) someSet
The entire shape of the set changes.
fmap (g . h) = fmap g . fmap h
This law wouldn't hold given the following contrived ord instance
data Foo = Foo { a, b :: Int }
instance Ord Foo where
compare = compare `on` a
Given functions
h foo = foo { a = 1 }
g foo = foo { a = b foo }
Does this library address this? If so, how? If not, then you'd best note it
in the docs.
On Jun 15, 2012 6:42 PM, George Giorgidze giorgi...@gmail.com wrote:
I would like to announce the first release of the set-monad library.
On Hackage: http://hackage.haskell.org/package/set-monad
The set-monad library exports the Set abstract data type and
set-manipulating functions. These functions behave exactly as their
namesakes from the Data.Set module of the containers library. In
addition, the set-monad library extends Data.Set by providing Functor,
Applicative, Alternative, Monad, and MonadPlus instances for sets.
In other words, you can use the set-monad library as a drop-in
replacement for the Data.Set module of the containers library and, in
addition, you will also get the aforementioned instances which are not
available in the containers package.
It is not possible to directly implement instances for the
aforementioned standard Haskell type classes for the Set data type
from the containers library. This is because the key operations map
and union, are constrained with Ord as follows.
map :: (Ord a, Ord b) = (a - b) - Set a - Set b
union :: (Ord a) = Set a - Set a - Set a
The set-monad library provides the type class instances by wrapping
the constrained Set type into a data type that has unconstrained
constructors corresponding to monadic combinators. The data type
constructors that represent monadic combinators are evaluated with a
constrained run function. This elevates the need to use the
constraints in the instance definitions (this is what prevents a
direct definition). The wrapping and unwrapping happens internally in
the library and does not affect its interface.
For details, see the rather compact definitions of the run function
and type class instances. The left identity and associativity monad
laws play a crucial role in the definition of the run function. The
rest of the code should be self explanatory.
The technique is not new. This library was inspired by [1]. To my
knowledge, the original, systematic presentation of the idea to
represent monadic combinators as data is given in [2]. There is also a
Haskell library that provides a generic infrastructure for the
aforementioned wrapping and unwrapping [3].
The set-monad library is particularly useful for writing set-oriented
code using the do and/or monad comprehension notations. For example,
the following definitions now type check.
s1 :: Set (Int,Int)
s1 = do a - fromList [1 .. 4]
b - fromList [1 .. 4]
return (a,b)
-- with -XMonadComprehensions
s2 :: Set (Int,Int)
s2 = [ (a,b) | (a,b) - s1, even a, even b ]
s3 :: Set Int
s3 = fmap (+1) (fromList [1 .. 4])
As noted in [1], the implementation technique can be used for monadic
libraries and EDSLs with restricted types (compiled EDSLs often
restrict the types that they can handle). Haskell's standard monad
type class can be used for restricted monad instances. There is no
need to resort to GHC extensions that rebind the standard monadic
combinators with the library or EDSL specific ones.
[1] CSDL Blog: The home of applied functional programming at KU. Monad
Reification in Haskell and the Sunroof Javascript compiler.
http://www.ittc.ku.edu/csdlblog/?p=88
[2] Chuan-kai Lin. 2006. Programming monads operationally with Unimo.
In Proceedings of the eleventh ACM SIGPLAN International Conference on
Functional Programming (ICFP '06). ACM.
[3] Heinrich Apfelmus. The operational package.
http://hackage.haskell.org/package/operational
___
Haskell mailing list
hask...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad
Hi Derek, On 16 June 2012 21:53, Derek Elkins derek.a.elk...@gmail.com wrote: The law that ends up failing is toList . fromList /= id, i.e. fmap g . toList . fromList . fmap h /= fmap g . fmap h This is not related to functor laws. The property that you desire is about toList and fromList. The toList and fromList functions are not required to satisfy toList . fromList /= id. This does not hold for Data.Set and it does not hold for the Data.Set.Monad wrapper either. Duplicates are lost when lists are converted into sets. Other instances of fromList and toList also fail to satisfy the property that you desire (e.g., Map). Cheers, George ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
