search

ekmett / ersatz

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

sum types: encoding, pattern matching #51

Open jwaldmann opened 4 years ago

jwaldmann commented 4 years ago

SAT encoding of product types is easy: just concatenate encodings of components. Ersatz already has this. For sum types like Either a b, Maybe a, we can encode the discriminant (the number of the constructor) and can overlay the encodings of the components. For programs on such data, we want to encode pattern matching.

My student did this via template Haskell (https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa-221884). Perhaps we can have a simple variant in plain Haskell, perhaps similar to https://mail.haskell.org/pipermail/haskell-cafe/2020-September/132650.html .

I am not implying that their implementation is simple, but it certainly looks simple to use in the given example.

jwaldmann commented 2 years ago

encode (Either a b) could be (Bit,encode a, encode b) (no overlay),

or (Bit, [Bit]) if we require HasBits a, HasBits b, and we need some phantom type parameters, so that we don't lose information.