[Haskell-cafe] Slightly Offtopic in Part
Dan Weston
westondan at imageworks.com
Fri Feb 8 22:32:41 EST 2008
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
>
>
More information about the Haskell-Cafe
mailing list