Product

A product is a pair. It contains two parts which are independent of each other. This means values within it can be accessed.

• (a,b) - read a and b like a conjunction
• Projection functions take (a,b)->a and (a,b)->b
• Type is A*B

Sum

A sum is one or the other. Often thought of as a variant.

• match x with (left a) -> s | (right b) -> t read a or b like two options.
• Injection functions take a->left a and b->right b
• Type is A+B

An algebraic type is a sum of products (we call these constructed types)
A record is a product
A case statement operates on a sum

Product

Concrete Syntax

(t1, t2) - build a pair
fst (t1, t2) - return the first element
snd (t1, t2 - return the second element

bind p = (1, 2) in 
  fst p; => 1
  snd p; => 2
  bind p = (p, 3) in
    fst p; => (1, 2)
    snd p; => 3
    bind p = (4, p) in
      fst p; => 4
      snd p; => ((1, 2), 3)
      fst snd p; => 1

t ::= (t, t) | fst t | snd t
v ::= (v, v)
T ::= T*T

Abstract Syntax

• Three new operations
• One new value

Pair :: FBAE -> FBAE -> FBAE
Fst :: FBAE -> FBAE
Snd :: FBAE -> FBAE

PairV :: FBAEVal -> FBAEVal -> FBAEVal

eval

eval e (PairV l r) = return (PairV l r)
eval e (Pair l r) = do { l' <- eval e l;
                         r' <- eval e r;
                         return (PairV l' r')
                        }
eval e (Fst v) = do { (PairV l _) <- eval e v;
                      return l
                     }
eval e (Fst v) = do { (PairV _ r) <- eval e v;
                      return r
                     }

Inference Rules

Sum

Concrete Syntax

(left 1)
(right "!")

match t with (left x) -> (f x) | (right x) -> print x

Abstract Syntax

Left :: FBAE -> (LeftV FBAEVal)
Right :: FBAE -> (RightV FBAEVal)
Match :: FBAE -> FBAE -> FBAE -> FBAE

eval e (Match t l r) = do { t' <- eval e t;
                            match t' with
                              (left x) = eval e l
                              (right x) = eval e r
                           }