search

ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
62 stars 15 forks source link

Add module for unary representation of sets based on Ersatz.Relation #83

Open emeinhardt opened 6 months ago

emeinhardt commented 6 months ago

Per @jwaldmann 's comment in #79 , this adds a unary ("bitmap") representation for finite sets and does so by extending existing functionality in Ersatz.Relation:

newtype Set a = Set { unSet :: Relation a () }

Below are some comments based on previous discussion:

I. Tacit style/dependency footprint Given the definition of Set, it's not surprising that almost all definitions are just calls to the relevant Relation functions with some mild wrapping/unwrapping as preprocessing, postprocessing, or a combination of both.

For the same reasons, most definitions are also in tacit style. Per previous discussion, on #79, composition hasn't changed much, ever, and doesn't have any dependencies itself beyond base. Nevertheless, I am happy to add .: as a local definition in an internal module if the additional dependency is still a concern.

As far as alternatives go, much of the functionality in the Set module could also have been written at least as succinctly using lens, an existing dependency. I think function composition, Control.Arrow, and a handful of extra definitions are more accessible and not much less succinct.

Another alternative abstraction would be profunctors: "take an existing function and make a new one by slapping a preprocessor and/or a postprocessor on it" is one description of what profunctors can do in the context of (->). I think they are a great fit for most of the current contents of Ersatz.Relation.Set and might be a clearer substitute for succinctly expressing intent. Since profunctors is already a dependency of lens and the Profunctor class is re-exported by lens, this option avoids introducing a new dependency. You can decide for yourself if this is clearer by examining this branch.

II. Module name/organization

A. I don't have strong feelings about Ersatz.Relation.Set as the module name/path per se, but given the unavoidable overlap in interfaces between Ersatz.Relation and the module provided here, putting the new set-related functionality in its own namespace strikes me as a better option than putting what's currently in Ersatz.Relation.Set in Ersatz.Relation but adding disambiguating affixes.

I am open to suggestions on alternatives.

B. Other representations of sets and related constructions are possible (e.g. @glguy's Select), so I'm not sure prematurely crowding out those representations by renaming Ersatz.Relation.Set to just Ersatz.Set is a great idea either.

RyanGlScott commented 3 months ago

Hi @emeinhardt,

I haven't really chimed in much on this PR (and related PRs) and it involves a significant amount of changes in parts of ersatz that I'm not familiar with. I think @jwaldmann is most familiar with this part of the code. @jwaldmann, perhaps you could chime in here?

jwaldmann commented 3 months ago

We will look into it.

@emeinhardt , if you haven't done so, could you add examples (to ersatz/examples) or test cases that show applications of the proposed modules. (Not just for judging correctness but also ergonomics.)

Perhaps https://www.mathekalender.de/wp/calendar/challenges/2023-01-en/

Or, Erdos-Ko-Rado

For cardinality constraints, just use Ersatz.Counting as-is, we can improve implementation of counting predicates later, in fact, I have a student assigned to that.