Richard, Thanks for your excellent feedback! Very helpful!
Signed multisets are unfamiliar to most of us, and I for one found the paper a little fast-paced. Can you put a bit more into the documentation?
Definitely. That's what weekends are for... :) I'll add some sections to the documentation that explain the main concepts and intuitions.
Just for starters, I found it confusing when the documentation talks about "an element with multiplicity zero", because in the _paper_ a value that has multiplicity zero in an mzset is NOT an element of it.
I see... It seems that with multisets every value of the appropriate type is an element of the set, but some values (i.e., those with multiplicities > 0) are more of an element than others (i.e., those with multiplicity 0). In the paper this is reflected by having the "element-of" relation a ternary relation between elements, sets, and multiplicities (with a "functional dependency" from elements and sets to multiplicities). Confusingly, "not-an-element-of" notation is used as an abbreviation for "element-of with multiplicity zero". The library labels elements with multiplicities > 0 as "members".
For a specific example, I haven't the faintest intuition about what 'map' should do. Suppose we have {(k1)x1, (k2)x2} and f x1 == f x2 = y. Should the value of map f {...} be {(k1+k2)y} or {(k1`max`k2)y} or what?
"Should" is a tricky term here. It depends on what you consider to be the structure of a multiset. Currently, map applies its function argument copywise: {x1_1, x1_2, ..., x1_k1, x2_1, x2_2, ..., x2_k2 } | | | | | | | f | f | f | f | f | f v v v v v v {y_1, y_2, ..., y_k1, y_k1+1, y_k1+2, ..., y_k1+k2}∑ That is, we preserve the additive structure. But perhaps this is inconsistent: the Monoid instance for SignedMultiset operates on the extremal structure rather than the additive structure. A wrapper type Additive, newtype Additive a = Additive (SignedMultiset a) supplies a monoid instance that operates on the additive structure. So, perhaps, it's better to have map as it is implemented now, operate on Additive rather than SignedMultiset and have a map for SignedMultiset that uses max rather than (+). A rationale for this would be that, this way, map would be a proper generalisation of ordinary sets. (The same rationale has been applied to union.) Pondering over this, I realise that the difference operator also doesn't property generalise the concept for ordinary sets. However, that concept indeed seems a bit more tricky to generalise.
Are you _sure_ that the definitions of isSubmultisetOf and isProperSubmultisetOf are correct? Proper sub<thing> is normally taken as requiring that only *one* member of the larger collection occur strictly fewer times in the smaller; here you require that for *all*.
You are right: isProperSubmultisetOf is too restrictive. I'll fix it. Thanks, Stefan