search

ekmett / ersatz

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

Add queries for relation cardinality #79

Closed emeinhardt closed 9 months ago

emeinhardt commented 10 months ago

Per the title.

jwaldmann commented 10 months ago

Yes, these looks plausible (for the user). Looking at the code, point-free style ((r !) .: (swap .: (,))) feels quite cryptic (I had to look up (.:)). On the other hand, pointed style (what we mostly use) perhaps is too pedestrian.

General thoughts (I should break this out into separate issues)

  1. The name card_dom suggests that this really should be card . dom (where card = sumBits) but then we would need dom : Relation a b -> Set a, for some type Set a that represents unknown sets, which we don't have right now. We could make Set a = Relation a (), then dom r = product r (the-full-relation-from-a-to -()) or similar.

  2. cardinality via sumBits: I am currently experimenting with alternate implementations of at-most-1, at-most-k (improving on Ersatz.Counting). Then (or even before) we could apply at-most-1 for: relation being a function, injectivity of function, and similar.

RyanGlScott commented 10 months ago

I'm leery about adding a new dependency solely for the sake of bringing in the (.:) function. I'd prefer either redefining (.:) in ersatz (its definition is quite small) or writing out the composition explicitly.

emeinhardt commented 9 months ago

@jwaldmann

card_dom / Ersatz.Set?

I see your point about card_dom/card_img and compositionality ± namespace hygiene.

  1. I'll remove those two definitions from this PR.
  2. I am also happy to follow your suggestion about symbolic sets — newtype Set a = Set { unSet :: Relation a () }? — in a new branch to see what that representation looks like with Boolean operations and some functionality for Ersatz.Relation like domain_of_definition/image. Would you like me to open an issue for discussion when that's ready or submit a PR with it?

Functional relations

You allude to functional relations, injectivity, etc.: I have a branch extending Ersatz.Relation that's intended for working with functional relations. Should I wait for your PR with improvements on Ersatz.Counting before submitting my branch as a PR?

Tacit style

The "blackbird" combinator can be useful quite often (more than anything else in composition or similar packages), but yeah I understand tacit style is a matter of taste.

Per above, I've removed card_dom/card_img for now, but I have other PRs currently drafted or in-progress that are written in tacit style in some places (few as point-free as card_dom/card_img!): perhaps after reviewing some of that code it might be clearer what (if any) amount of tacit style is desirable for Ersatz?

@RyanGlScott

composition

I understand wanting to limit additional dependencies, but on the other hand composition itself has no dependencies and is quite stable. Nevertheless, unless you and @jwaldmann would prefer to avoid tacit style entirely, I can make (.:) an Ersatz-local redefinition in the other branches that use it.