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: [EMAIL PROTECTED]
Mobile IRL: +353851383329,  Mobile PL: +48783303040
"Simplicity is the ultimate sophistication" -- Leonardo da Vinci


Tim Newsham
http://www.thenewsh.com/~newsham/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to