3

In automated theorem proving (proof search), I compose transformers of type

t :: Claim -> IO (Maybe (Claim, Proof -> Proof))

such that: when t c returns Just (c', f), then c' implies c and a proof for c is obtained from a proof p' for c' by computing f p'.

Is this a lens, somehow? (If yes, what would it help?)

There's also a more general case (for several, or zero, subgoals)

ts :: Claim -> IO (Maybe ([Claim], [Proof] -> Proof))

The IO part is important because these transformers do substantial work (calling external processes), and I might want to impose timeouts.

1 Answer 1

3

I can't readily see how lenses could help with that. However, reordering your monadic stack and using monad transformers should make composition much easier, and also open up the possibility of abstracting from IO in the cases you don't need impurity:

t' :: Claim -> MaybeT IO (Claim, Proof -> Proof)

If you want or need to keep using an existing implementation of t in spite of the more cumbersome type, you can lift its result to MaybeT with:

(MaybeT . return =<<) . lift :: m (Maybe b) -> MaybeT m b

It is worth noting that Claim -> (Claim, Proof -> Proof) is equivalent to State Claim (Proof -> Proof), so it might be possible to go even further:

t'' :: StateT Claim (MaybeT IO) (Proof -> Proof)

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.