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

[Derek Elkins]

Un-top-posted.  See below.

> On 19 June 2012 02:21, Derek Elkins <derek.a.elkins at gmail.com> wrote:
>>
>> On Jun 18, 2012 4:54 PM, "George Giorgidze" <giorgidze at gmail.com> wrote:
>>>
>>> Hi Derek,
>>>
>>> On 16 June 2012 21:53, Derek Elkins <derek.a.elkins at 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 <giorgidze at 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]