[Haskell-cafe] Slightly Offtopic in Part
Dan Licata
drl at cs.cmu.edu
Fri Feb 8 21:59:21 EST 2008
Out of context (am I missing some earlier part of this thread?) I'm not
entirely sure what you mean.
Are you're talking about the disjunction elim rule in intuitionistic
natural deduction:
Gamma |- A + B Gamma, A |- C Gamma, B |- C
----------------------------------------------
Gamma |- C
If so, this is just 'case'. If you annotate the rule with proof terms
(programs in the simply-typed lambda-calculus), you get the typing rule
for case:
Gamma |- e : A + B
Gamma, x1 : A |- e1 : C
Gamma, x2 : B |- e2 : C
------------------------------------------------------
Gamma |- case e of { Inl x1 -> e1 ; Inr x2 -> e2 } : C
I.e., when pattern matching on the following type
data Or a b =
Inl a
| Inr b
(this type is isomorphic to Either in the Prelude)
you have two cases to consider, one where you have an 'a' and the other
where you have a 'b'.
E.g., let's prove a simple theorem:
comm :: Or a b -> Or b a
comm x = case x of
Inl x1 -> Inr x1
Inr x2 -> Inl x2
Does that help?
-Dan
On Feb09, PR Stanley wrote:
> Hi folks
> The disjunction elimination rule:
> I've been trying to make sense of it and I think I have had some
> success; however, it's far from adequate. I wonder, is there a way of
> demonstrating it in Haskell? A code frag with a jargon-free
> explanation would be mucho appreciated.
> Cheers, Paul
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
More information about the Haskell-Cafe
mailing list