Closed ekmett closed 11 years ago
The basic design is that we have a basic type-branded bit type
newtype Bit b = Bit (Circuit (Bit b))
That uses StableNames to rederive sharing information when attaching the Bit b to the current SAT b Monad via
StableName
Bit b
SAT b
Monad
assert :: Bit b -> SAT b ()
Running the SAT b monad, yields a Solution b, which can be used by decode and decode from Encoding to decode the bits into values.
Solution b
decode
Encoding
However, the existentials seem to make writing any combinators that both run and extract solutions very difficult.
Is there a cleaner way to encode the API? Should we ditch the safety of existential branding?
Existential branding dropped.
ekmett
commented
11 years ago ekmett
commented
11 years ago
The basic design is that we have a basic type-branded bit type
That uses
StableNames to rederive sharing information when attaching theBit bto the currentSAT bMonadviaRunning the
SAT bmonad, yields aSolution b, which can be used bydecodeanddecodefromEncodingto decode the bits into values.However, the existentials seem to make writing any combinators that both run and extract solutions very difficult.
Is there a cleaner way to encode the API? Should we ditch the safety of existential branding?