[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Tim Newsham]

> Slightly offtopic - I am curious about the use of forall in some type
> signatures:

If you specify the "forall p q" at the top level then the types
used internally will use the same "p" and "q".  Otherwise the
internal types will be new "p"s and "q"s and wont line up with
the outer type declaration.

>> 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?

Ahh!  "r" is a remnant of earlier iterations where I had carried
around the "r" in every CProp from the classical propositions.
Then I realized I could just pick any "r" (I picked "()") and avoid
having to type "r" everywhere.  So its no longer used, and I'll remove
it from the code and the paper.  Thank you!

> 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
>

Tim Newsham
http://www.thenewsh.com/~newsham/