search

ekmett / ersatz

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

TypeApplications? #58

Closed jwaldmann closed 2 years ago

jwaldmann commented 3 years ago

I do want to use TypeApplications, for unary and binary numbers that have the bit width in the type.

The CI matrix includes ghc-7.10.3, which does not know them.

RyanGlScott commented 2 years ago

I've dropped support for GHC 7.10 in #59.

jwaldmann commented 2 years ago

Thanks.

I have this example application in mind https://github.com/jwaldmann/ersatz/blob/master/tests/Z001.hs#L21 , using https://github.com/jwaldmann/ersatz/blob/master/src/Ersatz/NBV.hs

Maybe a good intermediate step is to provide a module that contains such type-sized bitvectors that ignore overflow, so users can switch from current Bits1, Bits2, ...

Any suggestions on names? Bits Nat would conflict with existing Bits (variable length). They could be distinguished by module prefix. And - I don't like "Bits" here - as each encoding consists of bits. The name could express what we are encoding (naturals, modulo something) and possibly how (binary, perhaps with unary as an alternative).

Later, and separately, another type that does handle overflow (treat it as "plus infinity", e.g., it's > than non-overflowed numbers).

jwaldmann commented 2 years ago

closing this. type-applications can be used.