Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad

Un-top-posted. See below.

On 19 June 2012 02:21, Derek Elkins wrote:

...

On Jun 18, 2012 4:54 PM, "George Giorgidze" wrote:

...

Hi Derek,

On 16 June 2012 21:53, Derek Elkins 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 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]