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