Tim, I have also enjoyed the article, it's well written and easy enough to follow (at least for me). Slightly offtopic - I am curious about the use of forall in some type signatures:
subsume :: forall p q r. Prop (p :=> q) -> Prop ((p :/\ q) :== p) subsume pIMPq = equivInj (impInj pq2p) (impInj p2pq) where pq2p :: Prop (p :/\ q) -> Prop p pq2p assumePQ = andElimL assumePQ p2pq :: Prop p -> Prop (p :/\ q) p2pq assumeP = andInj assumeP q where q = impElim assumeP pIMPq
There "r" type variable is mentioned, but it does not occur anywhere else in the signature - what's the purpose of this construct? Regards, -- Krzysztof Kościuszkiewicz Skype: dr.vee, Gadu: 111851, Jabber: kokr@jabberpl.org Mobile IRL: +353851383329, Mobile PL: +48783303040 "Simplicity is the ultimate sophistication" -- Leonardo da Vinci