[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Krzysztof Kościuszkiewicz]

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 at jabberpl.org
Mobile IRL: +353851383329,  Mobile PL: +48783303040
"Simplicity is the ultimate sophistication" -- Leonardo da Vinci