Imrpovements to the logic system

[endgame]

I think I can improve the logic system (Logic.Propositional) from its current form. The main complaint I have is that I don't think the rules accurately capture natural deduction. Consider:

and_intro :: p -> q -> Proof (p && q)

This reads to me like "if I have a p and I have a q, then I have a Proof of p && q". What I think is better, is to stay within the world of proofs, with this alternate version:

and_intro :: Proof p -> Proof q -> Proof (p && q)

This reads more accurately as "if I have a Proof of p and a Proof of q, then I can construct a Proof of p && q. The fact that it's a premise is communicated because it's on the LHS of the (->) rather than by being an unadorned type.

This has several implications:

• I can't construct nonsense like and_intro 3 "hello" :: Proof (Int && String)
• There are nicer correspondences between the implication/elimination rules, and native haskell types. I can write these functions, and their inverses, linking conjunction with (,), disjunction with Either and implication with (->):
  • and_elim :: Proof (p && q) -> (Proof p, Proof q) (you do this one already)
  • or_elim :: Proof (p || q) -> Either (Proof p) (Proof q)
  • impl_elim :: Proof (p --> q) -> Proof p -> Proof q
• In fact, you may not need to dance in and out of the ESDL constructors And, Or and Implies, and just stick with the more native embeddings using (,)/Either/(->).
• The Bifunctor/Profunctor instances become a convenient way to map over one side of these operators.
• The exotic operators in Logic.Proof cease to be necessary, because you can do pretty much everything with straight function application/composition.
• I'm not sure what happens to the Functor/Applicative/Monad instances for Proof. because I don't think a value of Proof (a -> b) makes much sense (invalidating Applicative). join :: Proof (Proof a) -> Proof a doesn't look so crash-hot either. Does the Functor instance make sense? (What's the a -> b in fmap :: (a -> b) -> Proof a -> Proof b, when all your logical arguments have type Proof a -> Proof b anyway?)
• Because assumptions (i.e., function arguments) are now Proofs, lambdas become a convenient way to name introduced assumptions mid-proof. See this alternative modus_tollens as an example:

  modus_tollens :: Proof (p `Implies` q) -> Proof (Not q) -> Proof (Not p)
  modus_tollens impl q' = not_intro $ \p -> contradicts' q' (impl_elim p impl)

If this sounds interesting to you, I'm happy to have a crack at putting together a PR.

[matt-noonan]

This all sounds totally reasonable to me! I've been trying to decide if the Monad instance really makes sense or not, and I think I agree that the benefit is marginal and the instance itself is slightly weird.