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

[George Giorgidze]

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.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.