Sum Type Has multiple constructors but only one way to use it. But the eliminator is more complicated than say, the product type, because we don't know if A+B will be decomposed into type A or type B. 
Notation
In type theory the sum of A and B is denoted A+B. In logic the product is 'or' often denoted \/ .
An element of A+B is denoted <a,b> where 'a' is an element of 'A' and 'b' is an element of 'B'.
Rules
On the page about propositional logic here we had the introduction and elimination rules for 'or' :
Types are defined by their formation, term introduction, term eliminator and computation rules:
Introduction Constructor 
Elimination Deconstructor 




So the introduction rules show,
 If we have a proof of A we have a proof of A \/ B
 If we have a proof of B we have a proof of A \/ B
However we can't go in the reverse direction, for instance, if we have a proof of A \/ B we can't get to a proof of A. A proof of A \/ B does give us some information that is if:
 We have a proof of A \/ B
 A implies C
 B implies C
Then we have a proof of C.
When we translate from propositional logic to type theory we get the corresponding example of a constructors and deconstructor for a sum type (Taken from Idris prelude here):
Constructors  Deconstructor 

data Either : (a, b : Type) > Type where  One possibility of the sum  conventionally used to  represent errors Left : (l : a) > Either a b  The other possibility,  conventionally used to  represent success Right : (r : b) > Either a b 
 Simplytyped eliminator for Either  @ f the action to take on Left  @ g the action to take on Right  @ e the sum to analyze either : (f : Lazy (a > c)) > (g : Lazy (b > c)) > (e : Either a b) > c either l r (Left x) = (Force l) x either l r (Right x) = (Force r) x 
So, like with the introduction rules, the constructors are easy:
 Left to create from type a
 Right to create from type b
As with the elimination rule, the Deconstructor is more complicated.
If we have a function (a > c) and a function (b > c) then we can generate a function: Either a b > c
Another way to think about the deconstructor is as a matching operation, posibly implemented by a 'case' construct.
Rather than use the 'either' function above, it might be easier to use a 'case' construct:  case x:(Either A B) of a => c b => c 
So we can reformulate term eliminator rule as a matching operation. The above formulation told us that we can produce an element of C but here we make it explicit that this happens by matching on whether the element of A+B is an A or a B:
term eliminator rule assume: a implies c 

βreduction and ηreduction
βreduction
construction followed by deconstruction:
 (a > c) > (b > c) > <a,b> = c
ηreduction
deconstruction followed by construction:
 left ( (a > c) > (b > c) > S) = a
 right ( (a > c) > (b > c) > S) = b
Implementation in Idris for Sum
We can't constuct terms as easily because its more difficult to infer the type.  Idris> :let M = Either Integer String Idris> M Either Integer String : Type Idris> the M (Left 4) Left 4 : Either Integer String Idris> :let m = the M (Left 4) Idris> m Left 4 : Either Integer String 
'case' as deconstructor  lookup_default : Nat > List a > a > a lookup_default i xs def = case list_lookup i xs of Nothing => def Just x => x 
Sum Type
I think the + in A+B is thought of as an infix operator , we could write it as a prefix +(A,B) which makes it clearer that it is a type that depends on other types.
The usual axioms of products don't necessarily hold exactly, however they may hold upto isomorphism (or upto beta equality), that is, both sides of the equation contain the same information.
Type  Term  notes 

A+B ≠ B+A  inl(a) =? inr(a)  
(A+B)+C ≠A+(B+C)  
A+0 ≠A  0 can't be constructed so we are left with A=A 
Sum Type 


formation rule 


term introduction rule 


term eliminator rule assume: a implies c 


computation rule beta reduction 
match(inl(a), x.c_{A} y.c_{B}) =>_{β} c_{A}[a/x] 

Local completeness rule 
Implemetations of Sum
Idris 
we could define a sum type like this: data Or : Type > Type > Type where OrIntroLeft : a > A a b OrIntroRight : b > A a b also there is a built in type 'Either': 
from : Idrisdev/libs/prelude/Prelude/Either.idr 
 A sum type data Either : (a, b : Type) > Type where  One possibility of the sum,  conventionally used to represent errors Left : (l : a) > Either a b  The other possibility, conventionally  used to represent success Right : (r : b) > Either a b  Usage hints for erasure analysis %used Left l %used Right r   Syntactic tests   True if the argument is Left, False otherwise isLeft : Either a b > Bool isLeft (Left l) = True isLeft (Right r) = False  True if the argument is Right, False otherwise isRight : Either a b > Bool isRight (Left l) = False isRight (Right r) = True   Misc.   Simplytyped eliminator for Either  @ f the action to take on Left  @ g the action to take on Right  @ e the sum to analyze either : (f : Lazy (a > c)) > (g : Lazy (b > c)) > (e : Either a b) > c either l r (Left x) = (Force l) x either l r (Right x) = (Force r) x 
from : coq/theories/Init/Datatypes.v 
(** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) #[universes(template)] Inductive sum (A B:Type) : Type :=  inl : A > sum A B  inr : B > sum A B. Notation "x + y" := (sum x y) : type_scope. Arguments inl {A B} _ , [A] B _. Arguments inr {A B} _ , A [B] _. 
Next Steps
Other types are discussed on the following pages: