It should be emphasized that a type needs to be inhabited by (at least one) *total* function to prove a theorem. Otherwise, you could have the following partial function purporting to prove the phony theorem that "A or B implies A":

phony :: Either a b -> a
phony (Left a) = a

Dan

Dan Weston wrote:
For more details, look for a function called "orElim" in the write-up

http://www.thenewsh.com/~newsham/formal/curryhoward/

Dan

Ryan Ingram wrote:
I'm assuming you mean the rule described in
http://en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/Inference_Rules

type Disj a b = Either a b

disj_elim :: Disj a b -> (a -> c) -> (b -> c) -> c
disj_elim (Left a) a2c b2c = a2c a
disj_elim (Right b) a2c b2c = b2c b




_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to