Refactor logic

[endgame]

Sorry this took so long. It got a bit bigger than I intended. I'm happy to split it into smaller PRs if there are bits you don't want, or want to take in smaller chunks.

Summary of changes:

• Valuable: I stand by these and really want them merged
  • Use Proof a instead of a in premises. This makes proof types phantom everywhere.
  • Remove data constructors for logic constants and connectives. Because they are always phantom in Proof a, we don't need them.
  • Remove default signatures on the typeclasses for algebraic properties (e.g., Reflexive). Because these always take and return proofs, we can make them axiom everywhere.
  • Make the Proof type poly-kinded. So if someone wants to define his or her logic using -XDataKinds, it's possible to use that in a Proof.
  • Remove Functor/Applicative/Monad instance and custom operators for Proof, because they don't make logical sense any more.
  • Made calls to sorry emit warnings.
• Semi-valuable: I'd like these merged but am not going to lose sleep.
  • Renamed mapping functions to mimic the ones defined by Functor/Bifunctor/Profunctor.
• Bikeshedding: Happy to drop these on the floor to get the other things in.
  • Renamed functions in Propositional.hs to camelCase, to make hlint calm down.

Other remarks:

• I couldn't implement an isomorphism between Proof (a || b) and Either (Proof a) (Proof b), because you can't tell which of a or b is true, which is how you select which data constructor to use.
• I couldn't create Functor/Bifunctor/Profunctor instances for the logic types, because to map over a conjunction, say, you need a Proof p -> Proof p', not a p -> p'. There might be a typeclass that allows this, but I don't know of one.

Closes #2.

[matt-noonan]

This looks great, thank you!

My only request is to restore the default signatures for the algebraic property typeclasses, except using your all-Proof types. This lets the library author write empty instance declarations for the symbols they create, while forcing anybody else to write explicit instances. It doesn't make a huge difference, but I do think it is better to make it marginally harder for the library user to declare properties, relative to the library author. Ideally, if the user wants to make an instance for one of these properties, they would provide an actual proof instead of axiom. Does that seem reasonable to you, too?

[endgame]

Do you mean something like this?

class Transitive c where
  transitive :: Proof (c p q) -> Proof (c q r) -> Proof (c p r)
  default transitive :: Defining (c p q) => Proof (c p q) -> Proof (c q r) -> Proof (c p r)
  transitive _ _ = axiom

I'm not a huge fan but if you really want it I'll put it in. Reasoning:

1. If you're not defining a property alongside your connective, you're creating an orphan instance which is already Frowned Upon.
2. It forces the programmer to define constructors that never get used, just to make the default rule fire. This seems a bit subtle.

The best practice against orphan instances already gets you the protection you want: you assert these properties either against known connectives when you define the class, or against known classes when you define new connectives.

[matt-noonan]

Fair enough!