diff --git a/README.md b/README.md
index 5cb5f17..fe75879 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,5 @@
 # Lambda Calculus
-This is a simple implementation of the untyped lambda calculus
-with an emphasis on clear, readable Haskell code.
+This is a simple programming language derived from lambda calculus.
 
 ## Usage
 Run the program using `stack run` (or run the tests with `stack test`).
@@ -9,34 +8,24 @@ Type in your expression at the prompt: `>> `.
 The expression will be evaluated to normal form using the call-by-value evaluation strategy and then printed.
 Exit the prompt with `Ctrl-c` (or equivalent).
 
-### Example session
-```
->> let D = \x. x x; F = \f. f (f y) in D (F \x. x)
-y y
->> let T = \f x. f (f x) in (\f x. T (T (T (T T))) f x) (\x. x) y
-y
->> (\x y z. x y) y
-λy' z. y y'
->> let fix = (\x. x x) \fix f x. f (fix fix f) x; S = \n f x. f (n f x); plus = fix \plus x. x S in plus (\f x. f (f (f x))) (\f x. f (f x)) f x
-f (f (f (f (f x))))
->> y (callcc \k. (\x. (\x. x x) (\x. x x)) (k z))
-y z
->> ^C
-```
+## Syntax
+The parser's error messages currently are virtually useless, so be very careful with your syntax.
 
-## Notation
-[Conventional Lambda Calculus notation applies](https://en.wikipedia.org/wiki/Lambda_calculus_definition#Notation),
-with the exception that variable names are multiple characters long,
-`\` is permitted in lieu of `λ` to make it easier to type,
-and spaces are used to separate variables rather than commas.
-
-* Variable names are alphanumeric, beginning with a letter.
-* Outermost parentheses may be dropped: `M N` is equivalent to `(M N)`.
-* Applications are left-associative: `M N P` may be written instead of `((M N) P)`.
-* The body of an abstraction or let expression extends as far right as possible: `\x. M N` means `\x.(M N)` and not `(\x. M) N`.
-* A sequence of abstractions may be contracted: `\foo. \bar. \baz. N` may be abbreviated as `\foo bar baz. N`.
-* Variables may be bound using let expressions: `let x = N in M` is syntactic sugar for `(\x. N) M`.
-* Multiple variables may be defined in one let expression: `let x = N; y = O in M`
+* Variable names: any sequence of letters.
+* Function application: `f x y`
+* Lambda abstraction: `\x y z. E` or `λx y z. E`
+* Let expressions: `let x = E; y = F in G`
+* Parenthetical expressions: `(E)`
+* Constructors: `()`, `(x, y)` (or `(,) x y`), `Left x`, `Right y`, `Z`, `S`, `[]`, `(x : xs)` (or `(:) x xs`), `Char n`.
+  * The parentheses around the cons constructor are not optional.
+  * `Char` takes a natural number and turns it into a character.
+* Pattern matchers: `{ Left x -> e ; Right y -> f }`
+  * Pattern matchers can be applied like functions, e.g. `{ Z -> x, S -> y } 10` reduces to `y`.
+  * Patterns must use the regular form of the constructor, e.g. `(x : xs)` and not `((:) x xs)`.
+  * There are no nested patterns or default patterns.
+  * Incomplete pattern matches will crash the interpreter.
+* Literals: `1234`, `[e, f, g, h]`, `'a`, `"abc"`
+  * Strings are represented as lists of characters.
 
 ## Call/CC
 This interpreter has preliminary support for
@@ -50,3 +39,65 @@ with an argument named `!` which is used exactly once;
 however, continuations are *not* the same as lambda abstractions
 because they perform the side effect of modifying the current continuation,
 and this is *not* valid syntax you can input into the REPL.
+
+## Example code
+The fixpoint function:
+```
+(\x. x x) \fix f x. f (fix fix f) x
+```
+
+Create a list by iterating `f` `n` times:
+```
+fix \iterate f x. { Z -> x ; S n -> iterate f (f x) n }
+```
+
+Create a list whose first element is `n - 1`, counting down to a last element of `0`:
+```
+\n. { (n, x) -> x } (iterate { (n, x) -> (S n, (n : x)) } (0, []) n)
+```
+
+Putting it all together to count down from 10:
+```
+>> let fix = (\x. x x) \fix f x. f (fix fix f) x; iterate = fix \iterate f x. { Z -> x ; S n -> iterate f (f x) n }; countDownFrom = \n. { (n, x) -> x } (iterate { (n, x) -> (S n, (n : x)) } (0, []) n) in countDownFrom 10
+[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
+```
+
+Append two lists together:
+```
+fix \append xs ys. { [] -> ys ; (x : xs) -> (x : append xs ys) } xs
+```
+
+Reverse a list:
+```
+fix \reverse. { [] -> [] ; (x : xs) -> append (reverse xs) [x] }
+```
+
+Putting them together so we can reverse `"reverse"`:
+```
+>> let fix = (\x. x x) \fix f x. f (fix fix f) x; append = fix \append xs ys. { [] -> ys ; (x : xs) -> (x : append xs ys) } xs; reverse = fix \reverse. { [] -> [] ; (x : xs) -> append (reverse xs) [x] } in reverse "reverse"
+"esrever"
+```
+
+Calculating `3 + 2` with the help of Church-encoded numerals:
+```
+>> let Sf = \n f x. f (n f x); plus = \x. x Sf in plus (\f x. f (f (f x))) (\f x. f (f x)) S Z
+5
+```
+
+This expression would loop forever, but `callcc` saves the day!
+```
+>> y (callcc \k. (\x. (\x. x x) (\x. x x)) (k z))
+y z
+```
+
+A few other weird expressions:
+```
+>> let D = \x. x x; F = \f. f (f y) in D (F \x. x)
+y y
+>> let T = \f x. f (f x) in (\f x. T (T (T (T T))) f x) (\x. x) y
+y
+>> (\x y z. x y) y
+λy' z. y y'
+>> { Char c -> Char (S c) } 'a
+'b
+```
diff --git a/src/LambdaCalculus/Evaluator.hs b/src/LambdaCalculus/Evaluator.hs
index 954347c..2382ce6 100644
--- a/src/LambdaCalculus/Evaluator.hs
+++ b/src/LambdaCalculus/Evaluator.hs
@@ -1,16 +1,19 @@
 module LambdaCalculus.Evaluator
-  ( Expr (..), ExprF (..), VoidF, Text
+  ( Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text
   , Eval, EvalExpr, EvalX, EvalXF (..)
-  , pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
+  , pattern AppFE, pattern CtrE, pattern CtrFE
+  , pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
   , eval, traceEval, substitute, alphaConvert
   ) where
 
 import LambdaCalculus.Evaluator.Base
 import LambdaCalculus.Evaluator.Continuation
 
+import Control.Monad (forM)
 import Control.Monad.Except (MonadError, ExceptT, throwError, runExceptT)
 import Control.Monad.State (MonadState, State, evalState,  modify', state, put, gets)
 import Control.Monad.Writer (runWriterT, tell)
+import Data.Foldable (fold)
 import Data.Functor.Foldable (cata, para, embed)
 import Data.HashSet (HashSet)
 import Data.HashSet qualified as HS
@@ -21,17 +24,19 @@ import Data.Void (Void, absurd)
 -- | Free variables are variables which are present in an expression but not bound by any abstraction.
 freeVars :: EvalExpr -> HashSet Text
 freeVars = cata \case
+  VarF n   -> HS.singleton n
   AbsF n e -> HS.delete  n  e
   ContF e  -> HS.delete "!" e
-  VarF n   -> HS.singleton n
-  e -> foldr HS.union HS.empty e
+  CaseF ps -> foldMap (\(Pat _ ns e) -> HS.difference e (HS.fromList ns)) ps
+  e -> fold e
 
 -- | Bound variables are variables which are bound by any form of abstraction in an expression.
 boundVars :: EvalExpr -> HashSet Text
 boundVars = cata \case
   AbsF n e -> HS.insert  n  e
   ContF e  -> HS.insert "!" e
-  e -> foldr HS.union HS.empty e
+  CaseF ps -> foldMap (\(Pat _ ns e) -> HS.union (HS.fromList ns) e) ps
+  e -> fold e
 
 -- | Vars that occur anywhere in an experession, bound or free.
 usedVars :: EvalExpr -> HashSet Text
@@ -57,6 +62,12 @@ alphaConvert ctx e_ = evalState (alphaConverter e_) $ HS.union ctx (usedVars e_)
             n' <- fresh n
             e'' <- e'
             pure $ Abs n' $ replace n n' e''
+        -- | TODO: Only replace the names that *have* to be replaced.
+        | CaseF ps <- e, any (any (`HS.member` ctx) . patNames) ps ->
+            Case <$> forM ps \(Pat ctr ns e') -> do
+              ns' <- mapM fresh ns
+              e'' <- e'
+              pure $ Pat ctr ns' $ foldr (uncurry replace) e'' (zip ns ns')
         | otherwise -> embed <$> sequenceA e
 
     -- | Create a new name which is not used anywhere else.
@@ -74,7 +85,13 @@ replace name name' = cata \case
   e
     | VarF name2    <- e, name == name2 -> Var name'
     | AbsF name2 e' <- e, name == name2 -> Abs name' e'
+    | CaseF ps <- e -> Case $ flip map ps \(Pat ctr ns e') -> Pat ctr (replace' ns) e'
     | otherwise -> embed e
+  where
+    replace' = map \case
+        n
+          | n == name -> name'
+          | otherwise -> n
 
 -- | Substitution which does *not* avoid variable capture;
 -- it only gives the correct result if the bound variables in the body
@@ -85,6 +102,8 @@ unsafeSubstitute var val = para \case
     | VarF  var2   <- e', var == var2 -> val
     | AbsF  var2 _ <- e', var == var2 -> unmodified e'
     | ContF      _ <- e', var == "!"  -> unmodified e'
+    | CaseF ps <- e' -> Case $ flip map ps \(Pat ctr ns (unmod, sub)) ->
+        Pat ctr ns if var `elem` ns then unmod else sub
     | otherwise -> substituted e'
   where
     substituted, unmodified :: EvalExprF (EvalExpr, EvalExpr) -> EvalExpr
@@ -93,18 +112,37 @@ unsafeSubstitute var val = para \case
 
 isReducible :: EvalExpr -> Bool
 isReducible = snd . cata \case
-  AppFE ctr args -> eliminator ctr [args]
-  CallCCF        -> constructor
-  AbsF _ _       -> constructor
-  ContF _        -> constructor
+  AppFE ctr args -> active ctr [args]
+  AbsF _ _       -> passive
+  ContF _        -> passive
+  CaseF _        -> passive
+  CallCCF        -> passive
+  CtrFE _        -> constant
   VarF _         -> constant
   where
     -- | Constants are irreducible in any context.
     constant = (False, False)
-    -- | Constructors are reducible if an eliminator is applied to them.
-    constructor = (True, False)
-    -- | Eliminators are reducible if they are applied to a constructor or their arguments are reducible.
-    eliminator ctr args = (False, fst ctr || snd ctr || any snd args)
+    -- | Passive expressions are reducible only if an active expression is applied to them.
+    passive = (True, False)
+    -- | Active expressions are reducible if they are applied to a constructor or their arguments are reducible.
+    active ctr args = (False, fst ctr || snd ctr || any snd args)
+
+lookupPat :: Ctr -> [Pat phase] -> Pat phase
+lookupPat ctr = foldr lookupCtr' (error "Constructor not found")
+  where
+    lookupCtr' p@(Pat ctr' _ _) p'
+      | ctr == ctr' = p
+      | otherwise = p'
+
+isData :: EvalExpr -> Bool
+isData (CtrE _) = True
+isData (App ef _) = isData ef
+isData _ = False
+
+toData :: EvalExpr -> (Ctr, [EvalExpr])
+toData (CtrE ctr) = (ctr, [])
+toData (App ef ex) = (++ [ex]) <$> toData ef
+toData _ = error "Matched expression is not data"
 
 push :: MonadState Continuation m => ContinuationCrumb -> m ()
 push c = modify' (c :)
@@ -145,6 +183,12 @@ evaluatorStep = \case
         -- perform beta reduction if possible...
         Abs name body ->
           pure $ substitute name ex body
+        Case pats
+          | isData ex -> do
+              let (ctr, xs) = toData ex
+              let Pat _ ns e = lookupPat ctr pats
+              pure $ foldr (uncurry substitute) e (zip ns xs)
+          | otherwise -> ret unmodified
         -- perform continuation calls if possible...
         Cont body -> do
           put []
@@ -155,7 +199,7 @@ evaluatorStep = \case
           pure $ App ex (Cont k)
         -- otherwise the value is irreducible and we can continue evaluation.
         _ -> ret unmodified
-  -- Neither abstractions nor variables are reducible.
+  -- Neither abstractions, constructors nor variables are reducible.
   e -> ret e
 
 eval :: EvalExpr -> EvalExpr
diff --git a/src/LambdaCalculus/Evaluator/Base.hs b/src/LambdaCalculus/Evaluator/Base.hs
index 418d722..d2d68ff 100644
--- a/src/LambdaCalculus/Evaluator/Base.hs
+++ b/src/LambdaCalculus/Evaluator/Base.hs
@@ -1,8 +1,9 @@
 module LambdaCalculus.Evaluator.Base
   ( Identity (..)
-  , Expr (..), ExprF (..), VoidF, Text
+  , Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text
   , Eval, EvalExpr, EvalExprF, EvalX, EvalXF (..)
-  , pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
+  , pattern AppFE, pattern CtrE, pattern CtrFE
+  , pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
   ) where
 
 import LambdaCalculus.Expression.Base
@@ -14,6 +15,7 @@ type EvalExpr = Expr Eval
 type instance AppArgs Eval = EvalExpr
 type instance AbsArgs Eval = Text
 type instance LetArgs Eval = VoidF EvalExpr
+type instance CtrArgs Eval = UnitF EvalExpr
 type instance XExpr   Eval = EvalX
 
 type EvalX = EvalXF EvalExpr
@@ -21,6 +23,7 @@ type EvalX = EvalXF EvalExpr
 type EvalExprF = ExprF Eval
 type instance AppArgsF Eval = Identity
 type instance LetArgsF Eval = VoidF
+type instance CtrArgsF Eval = UnitF
 type instance XExprF   Eval = EvalXF
 
 data EvalXF r
@@ -39,6 +42,12 @@ instance RecursivePhase Eval where
   projectAppArgs = Identity
   embedAppArgs = runIdentity
 
+pattern CtrE :: Ctr -> EvalExpr
+pattern CtrE c = Ctr c Unit
+
+pattern CtrFE :: Ctr -> EvalExprF r
+pattern CtrFE c = CtrF c Unit
+
 pattern Cont :: EvalExpr -> EvalExpr
 pattern Cont e = ExprX (Cont_ e)
 
@@ -54,7 +63,11 @@ pattern CallCCF = ExprXF CallCC_
 pattern AppFE :: r -> r -> EvalExprF r
 pattern AppFE ef ex = AppF ef (Identity ex)
 
-{-# COMPLETE Var,  App,   Abs,  Let,  Cont,  CallCC  #-}
-{-# COMPLETE VarF, AppF,  AbsF, LetF, ContF, CallCCF #-}
-{-# COMPLETE VarF, AppFE, AbsF, LetF, ExprXF         #-}
-{-# COMPLETE VarF, AppFE, AbsF, LetF, ContF, CallCCF #-}
+{-# COMPLETE Var,  App,   Abs,  Let,  Ctr,   Case,  Cont,  CallCC  #-}
+{-# COMPLETE VarF, AppF,  AbsF, LetF, CtrF,  CaseF, ContF, CallCCF #-}
+{-# COMPLETE VarF, AppFE, AbsF, LetF, CtrF,  CaseF, ExprXF         #-}
+{-# COMPLETE VarF, AppFE, AbsF, LetF, CtrF,  CaseF, ContF, CallCCF #-}
+{-# COMPLETE Var,  App,   Abs,  Let,  CtrE,  Case,  Cont,  CallCC  #-}
+{-# COMPLETE VarF, AppF,  AbsF, LetF, CtrFE, CaseF, ContF, CallCCF #-}
+{-# COMPLETE VarF, AppFE, AbsF, LetF, CtrFE, CaseF, ExprXF         #-}
+{-# COMPLETE VarF, AppFE, AbsF, LetF, CtrFE, CaseF, ContF, CallCCF #-}
diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs
index 6de24af..965738e 100644
--- a/src/LambdaCalculus/Expression.hs
+++ b/src/LambdaCalculus/Expression.hs
@@ -1,20 +1,23 @@
 module LambdaCalculus.Expression
-  ( Expr (..), ExprF (..), DefF (..), VoidF, Text
+  ( Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), DefF (..), VoidF, UnitF (..), Text
   , Eval, EvalExpr, EvalX, EvalXF (..), Identity (..)
-  , pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
-  , Parse, AST, ASTF, NonEmptyDefFs (..), NonEmpty (..), simplify
-  , pattern LetFP
+  , pattern AppFE, pattern CtrE, pattern CtrFE,
+    pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF
+  , Parse, AST, ASTF, ASTX, ASTXF (..), NonEmptyDefFs (..), NonEmpty (..), simplify
+  , pattern LetFP, pattern PNat, pattern PNatF, pattern PList, pattern PListF
+  , pattern PChar, pattern PCharF, pattern PStr, pattern PStrF
   , ast2eval, eval2ast
   ) where
 
 import LambdaCalculus.Evaluator.Base
-import LambdaCalculus.Evaluator
+import LambdaCalculus.Evaluator (alphaConvert, substitute)
 import LambdaCalculus.Syntax.Base
 
 import Data.Functor.Foldable (cata, hoist)
 import Data.HashSet qualified as HS
 import Data.List (foldl')
 import Data.List.NonEmpty (toList)
+import Data.Text (unpack)
 
 -- | Convert from an abstract syntax tree to an evaluator expression.
 ast2eval :: AST -> EvalExpr
@@ -25,6 +28,19 @@ ast2eval = substitute "callcc" CallCC . cata \case
   LetF ds e ->
     let letExpr name val body' = App (Abs name body') val
     in foldr (uncurry letExpr) e $ getNonEmptyDefFs ds
+  CtrF ctr es -> foldl' App (CtrE ctr) es
+  CaseF ps -> Case ps
+  PNatF n -> int2ast n
+  PListF es -> mkList es
+  PStrF s -> mkList $ map (App (CtrE CChar) . int2ast . fromEnum) $ unpack s
+  PCharF c -> App (CtrE CChar) (int2ast $ fromEnum c)
+  where
+    int2ast :: Int -> EvalExpr
+    int2ast 0 = CtrE CZero
+    int2ast n = App (CtrE CSucc) (int2ast (n - 1))
+
+    mkList :: [EvalExpr] -> EvalExpr
+    mkList = foldr (App . App (CtrE CCons)) (CtrE CNil)
 
 -- | Convert from an evaluator expression to an abstract syntax tree.
 eval2ast :: EvalExpr -> AST
@@ -40,4 +56,6 @@ eval2ast = hoist go . alphaConvert (HS.singleton "callcc")
       CallCCF -> VarF "callcc"
       AppFE ef ex -> AppF ef (ex :| [])
       AbsF n e -> AbsF (n :| []) e
+      CtrFE ctr -> CtrF ctr []
+      CaseF ps -> CaseF ps
       ContF e -> AbsF ("!" :| []) e
diff --git a/src/LambdaCalculus/Expression/Base.hs b/src/LambdaCalculus/Expression/Base.hs
index 2253989..b0bb619 100644
--- a/src/LambdaCalculus/Expression/Base.hs
+++ b/src/LambdaCalculus/Expression/Base.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE UndecidableInstances #-}
 module LambdaCalculus.Expression.Base
-  ( Text, VoidF, absurd'
-  , Expr (..), Def, AppArgs, AbsArgs, LetArgs, XExpr
-  , ExprF (..), DefF (..), AppArgsF, LetArgsF, XExprF
-  , RecursivePhase, projectAppArgs, projectLetArgs, projectXExpr, projectDef
-  , embedAppArgs, embedLetArgs, embedXExpr, embedDef
+  ( Text, VoidF, UnitF (..), absurd'
+  , Expr (..), Ctr (..), Pat, Def, AppArgs, AbsArgs, LetArgs, CtrArgs, XExpr
+  , ExprF (..), PatF (..), DefF (..), AppArgsF, LetArgsF, CtrArgsF, XExprF
+  , RecursivePhase, projectAppArgs, projectLetArgs, projectCtrArgs, projectXExpr, projectDef
+  , embedAppArgs, embedLetArgs, embedCtrArgs, embedXExpr, embedDef
   ) where
 
 import Data.Functor.Foldable (Base, Recursive, Corecursive, project, embed)
@@ -20,13 +20,25 @@ data Expr phase
   | Abs !(AbsArgs phase) !(Expr phase)
   -- | Let expression: `let x_0 = v_0 ... ; x_n = v_n in e`.
   | Let !(LetArgs phase) !(Expr phase)
+  -- | Data constructor, e.g. `(x, y)` or `Left`.
+  | Ctr !Ctr !(CtrArgs phase)
+  -- | Case expression to pattern match against a value,
+  -- e.g. `case { Left x1 -> e1 ; Right x2 -> e2 }`.
+  | Case ![Pat phase]
   -- | Additional phase-specific constructors.
   | ExprX !(XExpr phase)
 
+type family AppArgs phase
+type family AbsArgs phase
+type family LetArgs phase
+type family CtrArgs phase
+type family XExpr phase
+
 deriving instance
   ( Eq (AppArgs phase)
   , Eq (AbsArgs phase)
   , Eq (LetArgs phase)
+  , Eq (CtrArgs phase)
   , Eq (XExpr   phase)
   ) => Eq (Expr phase)
 
@@ -34,13 +46,36 @@ deriving instance
   ( Show (AppArgs phase)
   , Show (AbsArgs phase)
   , Show (LetArgs phase)
+  , Show (CtrArgs phase)
   , Show (XExpr   phase)
   ) => Show (Expr phase)
 
-type family AppArgs phase
-type family AbsArgs phase
-type family LetArgs phase
-type family XExpr phase
+-- | Data constructors (used in pattern matching and literals).
+data Ctr
+  -- | `() : ★`
+  = CUnit
+  -- | `(x : a, y : b) : a * b`
+  | CPair
+  -- | `Left (x : a) : forall b. a + b`
+  | CLeft
+  -- | `Right (x : b) : forall a. a + b`
+  | CRight
+  -- | `0 : Nat`
+  | CZero
+  -- | `1+ (n : Nat) : Nat`
+  | CSucc
+  -- | `[] : forall a. List a`
+  | CNil
+  -- | `(x : a) :: (xs : List a) : List a`
+  | CCons
+  -- | `Char :: Nat -> Char`
+  | CChar
+  deriving (Eq, Show)
+
+-- | A single pattern of a case expression, e.g. `(x, y) -> e`.
+type Pat phase = PatF (Expr phase)
+data PatF r = Pat { patCtr :: !Ctr, patNames :: ![Text], patBody :: !r }
+  deriving (Eq, Functor, Foldable, Traversable, Show)
 
 -- | A definition, mapping a name to a value.
 type Def phase = (Text, Expr phase)
@@ -54,17 +89,24 @@ data ExprF phase r
   | AppF !r !(AppArgsF phase r)
   | AbsF !(AbsArgs phase) r
   | LetF !(LetArgsF phase r) r
+  | CtrF Ctr (CtrArgsF phase r)
+  | CaseF [PatF r]
   | ExprXF !(XExprF phase r)
 
 type instance Base (Expr phase) = ExprF phase
 
 type family AppArgsF phase :: Type -> Type
 type family LetArgsF phase :: Type -> Type
+type family CtrArgsF phase :: Type -> Type
 type family XExprF phase :: Type -> Type
 
 data DefF r = DefF !Text !r
   deriving (Eq, Functor, Show)
 
+-- | A contractible data type with one extra type parameter.
+data UnitF a = Unit
+  deriving (Eq, Functor, Foldable, Traversable, Show)
+
 -- | An empty type with one extra type parameter.
 data VoidF a
   deriving (Eq, Functor, Foldable, Traversable, Show)
@@ -75,6 +117,7 @@ absurd' x = case x of {}
 instance
   ( Functor (AppArgsF phase)
   , Functor (LetArgsF phase)
+  , Functor (CtrArgsF phase)
   , Functor (XExprF phase)
   ) => Functor (ExprF phase) where
   fmap f = \case
@@ -82,11 +125,14 @@ instance
     AppF ef exs -> AppF (f ef) (fmap f exs)
     AbsF ns e -> AbsF ns (f e)
     LetF ds e -> LetF (fmap f ds) (f e)
+    CtrF c es -> CtrF c (fmap f es)
+    CaseF ps -> CaseF (fmap (fmap f) ps)
     ExprXF q -> ExprXF (fmap f q)
 
 instance
   ( Foldable (AppArgsF phase)
   , Foldable (LetArgsF phase)
+  , Foldable (CtrArgsF phase)
   , Foldable (XExprF   phase)
   ) => Foldable (ExprF phase) where
   foldMap f = \case
@@ -94,11 +140,14 @@ instance
     AppF ef exs -> f ef <> foldMap f exs
     AbsF _ e -> f e
     LetF ds e -> foldMap f ds <> f e
+    CtrF _ es -> foldMap f es
+    CaseF ps -> foldMap (foldMap f) ps
     ExprXF q -> foldMap f q
 
 instance
   ( Traversable (AppArgsF phase)
   , Traversable (LetArgsF phase)
+  , Traversable (CtrArgsF phase)
   , Traversable (XExprF   phase)
   ) => Traversable (ExprF phase) where
   traverse f = \case
@@ -106,21 +155,27 @@ instance
     AppF ef exs -> AppF <$> f ef <*> traverse f exs
     AbsF ns e -> AbsF ns <$> f e
     LetF ds e -> LetF <$> traverse f ds <*> f e
+    CtrF c es -> CtrF c <$> traverse f es
+    CaseF ps -> CaseF <$> traverse (traverse f) ps
     ExprXF q -> ExprXF <$> traverse f q
 
 class Functor (ExprF phase) => RecursivePhase phase where
   projectAppArgs :: AppArgs phase -> AppArgsF phase (Expr phase)
   projectLetArgs :: LetArgs phase -> LetArgsF phase (Expr phase)
+  projectCtrArgs :: CtrArgs phase -> CtrArgsF phase (Expr phase)
   projectXExpr   :: XExpr   phase -> XExprF   phase (Expr phase)
 
   embedAppArgs :: AppArgsF phase (Expr phase) -> AppArgs phase
   embedLetArgs :: LetArgsF phase (Expr phase) -> LetArgs phase
+  embedCtrArgs :: CtrArgsF phase (Expr phase) -> CtrArgs phase
   embedXExpr   :: XExprF   phase (Expr phase) -> XExpr   phase
 
   default projectAppArgs :: AppArgs phase ~  AppArgsF phase (Expr phase)
                          => AppArgs phase -> AppArgsF phase (Expr phase)
   default projectLetArgs :: LetArgs phase ~  LetArgsF phase (Expr phase)
                          => LetArgs phase -> LetArgsF phase (Expr phase)
+  default projectCtrArgs :: CtrArgs phase ~  CtrArgsF phase (Expr phase)
+                         => CtrArgs phase -> CtrArgsF phase (Expr phase)
   default projectXExpr   :: XExpr   phase ~  XExprF   phase (Expr phase)
                          => XExpr   phase -> XExprF   phase (Expr phase)
 
@@ -128,15 +183,19 @@ class Functor (ExprF phase) => RecursivePhase phase where
                        => AppArgsF phase (Expr phase) -> AppArgs phase
   default embedLetArgs :: LetArgsF phase (Expr phase) ~  LetArgs phase
                        => LetArgsF phase (Expr phase) -> LetArgs phase
+  default embedCtrArgs :: CtrArgsF phase (Expr phase) ~  CtrArgs phase
+                       => CtrArgsF phase (Expr phase) -> CtrArgs phase
   default embedXExpr   :: XExprF   phase (Expr phase) ~  XExpr   phase
                        => XExprF   phase (Expr phase) -> XExpr   phase
 
   projectAppArgs = id
   projectLetArgs = id
+  projectCtrArgs = id
   projectXExpr   = id
 
   embedAppArgs = id
   embedLetArgs = id
+  embedCtrArgs = id
   embedXExpr   = id
 
 projectDef :: Def phase -> DefF (Expr phase)
@@ -151,6 +210,8 @@ instance RecursivePhase phase => Recursive (Expr phase) where
     App ef exs -> AppF ef (projectAppArgs exs)
     Abs ns e -> AbsF ns e
     Let ds e -> LetF (projectLetArgs ds) e
+    Ctr c es -> CtrF c (projectCtrArgs es)
+    Case ps -> CaseF ps
     ExprX q -> ExprXF (projectXExpr q)
 
 instance RecursivePhase phase => Corecursive (Expr phase) where
@@ -159,6 +220,8 @@ instance RecursivePhase phase => Corecursive (Expr phase) where
     AppF ef exs -> App ef (embedAppArgs exs)
     AbsF ns e -> Abs ns e
     LetF ds e -> Let (embedLetArgs ds) e
+    CtrF c es -> Ctr c (embedCtrArgs es)
+    CaseF ps -> Case ps
     ExprXF q -> ExprX (embedXExpr q)
 
 ---
diff --git a/src/LambdaCalculus/Syntax/Base.hs b/src/LambdaCalculus/Syntax/Base.hs
index 9dee3ca..81161c3 100644
--- a/src/LambdaCalculus/Syntax/Base.hs
+++ b/src/LambdaCalculus/Syntax/Base.hs
@@ -1,14 +1,16 @@
 module LambdaCalculus.Syntax.Base
-  ( Expr (..), ExprF (..), Def, DefF (..), VoidF, Text, NonEmpty (..)
-  , Parse, AST, ASTF, NonEmptyDefFs (..)
-  , pattern LetFP
+  ( Expr (..), ExprF (..), Ctr (..), Pat, Def, DefF (..), PatF (..), VoidF, Text, NonEmpty (..)
+  , Parse, AST, ASTF, ASTX, ASTXF (..), NonEmptyDefFs (..)
+  , pattern LetFP, pattern PNat, pattern PNatF, pattern PList, pattern PListF
+  , pattern PChar, pattern PCharF, pattern PStr, pattern PStrF
   , simplify
   ) where
 
 import LambdaCalculus.Expression.Base
 
 import Data.Functor.Foldable (embed, project)
-import Data.List.NonEmpty (NonEmpty (..))
+import Data.List.NonEmpty (NonEmpty (..), toList)
+import Data.Text qualified as T
 
 data Parse
 -- | The abstract syntax tree reflects the structure of the externally-visible syntax.
@@ -31,12 +33,27 @@ type AST = Expr Parse
 type instance AppArgs Parse = NonEmpty AST
 type instance AbsArgs Parse = NonEmpty Text
 type instance LetArgs Parse = NonEmpty (Def Parse)
-type instance XExpr   Parse = VoidF AST
+type instance CtrArgs Parse = [AST]
+type instance XExpr   Parse = ASTX
+
+type ASTX = ASTXF AST
 
 type ASTF = ExprF Parse
 type instance AppArgsF Parse = NonEmpty
 type instance LetArgsF Parse = NonEmptyDefFs
-type instance XExprF   Parse = VoidF
+type instance CtrArgsF Parse = []
+type instance XExprF   Parse = ASTXF
+
+data ASTXF r
+  -- | A natural number literal, e.g. `10`.
+  = PNat_ Int
+  -- | A list literal, e.g. `[x, y, z]`.
+  | PList_ [r]
+  -- | A character literal, e.g. `'a`.
+  | PChar_ Char
+  -- | A string literal, e.g. `"abcd"`.
+  | PStr_ Text
+  deriving (Eq, Functor, Foldable, Traversable, Show)
 
 instance RecursivePhase Parse where
   projectLetArgs = NonEmptyDefFs
@@ -45,22 +62,70 @@ instance RecursivePhase Parse where
 newtype NonEmptyDefFs r = NonEmptyDefFs { getNonEmptyDefFs :: NonEmpty (Text, r) }
   deriving (Eq, Functor, Foldable, Traversable, Show)
 
+
 pattern LetFP :: NonEmpty (Text, r) -> r -> ASTF r
 pattern LetFP ds e = LetF (NonEmptyDefFs ds) e
 
-{-# COMPLETE VarF, AppF, AbsF, LetFP, ExprXF #-}
+pattern PNat :: Int -> AST
+pattern PNat n = ExprX (PNat_ n)
 
--- | Combine nested expressions into compound expressions when possible.
+pattern PNatF :: Int -> ASTF r
+pattern PNatF n = ExprXF (PNat_ n)
+
+pattern PList :: [AST] -> AST
+pattern PList es = ExprX (PList_ es)
+
+pattern PListF :: [r] -> ASTF r
+pattern PListF es = ExprXF (PList_ es)
+
+pattern PChar :: Char -> AST
+pattern PChar c = ExprX (PChar_ c)
+
+pattern PCharF :: Char -> ASTF r
+pattern PCharF c = ExprXF (PChar_ c)
+
+pattern PStrF :: Text -> ASTF r
+pattern PStrF s = ExprXF (PStr_ s)
+
+pattern PStr :: Text -> AST
+pattern PStr s = ExprX (PStr_ s)
+
+{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, ExprXF                       #-}
+{-# COMPLETE Var,  App,  Abs,  Let,   Ctr,  Case,  PNat,  PList,  PChar,  PStr  #-}
+{-# COMPLETE VarF, AppF, AbsF, LetF , CtrF, CaseF, PNatF, PListF, PCharF, PStrF #-}
+{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, PNatF, PListF, PCharF, PStrF #-}
+
+-- | Combine nested expressions into compound expressions or literals when possible.
 simplify :: AST -> AST
-simplify = simplify' . embed . fmap simplify' . project
+simplify = simplify' . embed . fmap simplify . project
   where
-    simplify' (App (App f es1) es2) = simplify' $ App f (es1 <> es2)
+    -- Combine sequences of nat constructors into literals.
+    simplify' (Ctr CZero [])                  = PNat 0
+    simplify' (Ctr CSucc [PNat n])            = PNat (n + 1)
+    -- Combine sequences of string constructors into string literals.
+    simplify' (Ctr CChar [PNat n])            = PChar (toEnum n)
+    simplify' o@(Ctr CCons [PChar c, PList []])
+      | c /= '"' = PStr (T.singleton c)
+      | otherwise = o
+    simplify' o@(Ctr CCons [PChar c, PStr  cs])
+      | c /= '"' = PStr (T.cons c cs)
+      | otherwise = o
+    -- Combine sequences of list contructors into list literals.
+    simplify' (Ctr CNil  [])                  = PList []
+    simplify' (Ctr CCons [x, PList xs])       = PList (x : xs)
+    -- Move applications into constructors.
+    simplify' (App (Ctr ctr es1) es2) = simplify' $ Ctr ctr (es1 <> toList es2)
+    -- Combine reducible applications into let expressions.
     simplify' (App (Abs (nx :| ns) eb) (ex :| es)) = simplify' $ app' es $ Let ((nx, ex) :| []) $ abs' ns eb
       where app' []        e = e
             app' (ex2:es2) e = App e (ex2 :| es2)
 
             abs' []        e = e
             abs' (nx2:ns2) e = Abs (nx2 :| ns2) e
+    -- Combine sequences of nested applications into n-ary applications.
+    simplify' (App (App f es1) es2) = simplify' $ App f (es1 <> es2)
+    -- Combine sequences of nested abstractions into n-argument abstractions.
     simplify' (Abs ns1 (Abs ns2 e)) = simplify' $ Abs (ns1 <> ns2) e
+    -- Combine sequences of nested let expressions into n-definition let expressions.
     simplify' (Let ds1 (Let ds2 e)) = simplify' $ Let (ds1 <> ds2) e
     simplify' e = e
diff --git a/src/LambdaCalculus/Syntax/Parser.hs b/src/LambdaCalculus/Syntax/Parser.hs
index 3991202..c3ed956 100644
--- a/src/LambdaCalculus/Syntax/Parser.hs
+++ b/src/LambdaCalculus/Syntax/Parser.hs
@@ -7,6 +7,7 @@ import LambdaCalculus.Syntax.Base
 
 import Data.List.NonEmpty (fromList)
 import Data.Text qualified as T
+import Prelude hiding (succ, either)
 import Text.Parsec hiding (label, token)
 import Text.Parsec qualified
 import Text.Parsec.Text (Parser)
@@ -18,7 +19,7 @@ token :: Char -> Parser ()
 token ch = label [ch] $ char ch *> spaces
 
 keywords :: [Text]
-keywords = ["let", "in"]
+keywords = ["let", "in", "Left", "Right", "S", "Z", "Char"]
 
 -- | A keyword is an exact string which is not part of an identifier.
 keyword :: Text -> Parser ()
@@ -45,28 +46,113 @@ many2 :: Parser a -> Parser (a, NonEmpty a)
 many2 p = (,) <$> p <*> many1' p
 
 grouping :: Parser AST
-grouping = label "grouping" $ between (token '(') (token ')') expression
+grouping = label "grouping" $ between (token '(') (token ')') ambiguous
 
 application :: Parser AST
-application = uncurry App <$> many2 applicationTerm
-  where applicationTerm = abstraction <|> let_ <|> grouping <|> variable
+application = uncurry App <$> many2 block
 
 abstraction :: Parser AST
-abstraction = label "lambda abstraction" $ Abs <$> between lambda (token '.') (many1' identifier) <*> expression
+abstraction = label "lambda abstraction" $ Abs <$> between lambda (token '.') (many1' identifier) <*> ambiguous
   where lambda = label "lambda" $ (char '\\' <|> char 'λ') *> spaces
 
 let_ :: Parser AST
-let_ = Let <$> between (keyword "let") (keyword "in") (fromList <$> definitions) <*> expression
+let_ = Let <$> between (keyword "let") (keyword "in") (fromList <$> definitions) <*> ambiguous
   where
     definitions :: Parser [Def Parse]
     definitions = flip sepBy1 (token ';') do
       name <- identifier
       token '='
-      value <- expression
+      value <- ambiguous
       pure (name, value)
 
-expression :: Parser AST
-expression = label "expression" $ abstraction <|> let_ <|> try application <|> grouping <|> variable
+ctr :: Parser AST
+ctr = pair <|> unit <|> either <|> nat <|> list <|> str
+  where
+    unit, pairCtr, tuple, either, left, right,
+      zero, succ, natLit, consCtr, cons, charCtr, charLit, strLit :: Parser AST
+    unit = Ctr CUnit [] <$ keyword "()"
+    pair = pairCtr <|> tuple
+    pairCtr = Ctr CPair [] <$ keyword "(,)"
+    tuple = try $ between (token '(') (token ')') do
+      e1 <- ambiguous
+      token ','
+      e2 <- ambiguous
+      pure $ Ctr CPair [e1, e2]
+    either = left <|> right
+    left = Ctr CLeft [] <$ keyword "Left"
+    right = Ctr CRight [] <$ keyword "Right"
+    nat = zero <|> succ <|> natLit
+    zero = Ctr CZero [] <$ keyword "Z"
+    succ = Ctr CSucc [] <$ keyword "S"
+    natLit = (PNat . read <$> many1 digit) <* spaces
+    list = cons <|> consCtr <|> listLit
+    consCtr = Ctr CCons [] <$ keyword "(:)"
+    cons = try $ between (token '(') (token ')') do
+      e1 <- ambiguous
+      token ':'
+      e2 <- ambiguous
+      pure $ Ctr CCons [e1, e2]
+    listLit = fmap PList $ between (token '[') (token ']') $ sepEndBy ambiguous (token ',')
+    str = charCtr <|> charLit <|> strLit
+    charCtr = Ctr CChar [] <$ keyword "Char"
+    charLit = fmap PChar $ char '\'' *> anyChar <* spaces
+    strLit = fmap (PStr . T.pack) $ between (token '"') (token '"') $ many (noneOf "\"")
+
+pat :: Parser (Pat Parse)
+pat = label "case alternate" $ do
+  (c, ns) <- label "pattern" $
+    pair <|> unit <|> left <|> right <|> zero <|> succ <|> nil <|> cons <|> char'
+  keyword "->"
+  e <- ambiguous
+  pure $ Pat c ns e
+  where pair = try $ between (token '(') (token ')') do
+          e1 <- identifier
+          token ','
+          e2 <- identifier
+          pure (CPair, [e1, e2])
+        unit = (CUnit, []) <$ keyword "()"
+        left = do
+          keyword "Left"
+          e <- identifier
+          pure (CLeft, [e])
+        right = do
+          keyword "Right"
+          e <- identifier
+          pure (CRight, [e])
+        zero = (CZero, []) <$ keyword "Z"
+        succ = do
+          keyword "S"
+          e <- identifier
+          pure (CSucc, [e])
+        nil = (CNil, []) <$ keyword "[]"
+        cons = try $ between (token '(') (token ')') do
+          e1 <- identifier
+          token ':'
+          e2 <- identifier
+          pure (CCons, [e1, e2])
+        char' = do
+          keyword "Char"
+          e <- identifier
+          pure (CChar, [e])
+
+case_ :: Parser AST
+case_ = label "case patterns" $ do
+  token '{'
+  pats <- sepEndBy pat (token ';')
+  token '}'
+  pure $ Case pats
+
+-- | Guaranteed to consume a finite amount of input
+finite :: Parser AST
+finite = label "finite expression" $ variable <|> ctr <|> case_ <|> grouping
+
+-- | Guaranteed to consume input, but may continue until it reaches a terminator
+block :: Parser AST
+block = label "block expression" $ finite <|> abstraction <|> let_
+
+-- | Not guaranteed to consume input at all, may continue until it reaches a terminator
+ambiguous :: Parser AST
+ambiguous = label "any expression" $ try application <|> block
 
 parseAST :: Text -> Either ParseError AST
-parseAST = parse (spaces *> expression <* eof) "input"
+parseAST = parse (spaces *> ambiguous <* eof) "input"
diff --git a/src/LambdaCalculus/Syntax/Printer.hs b/src/LambdaCalculus/Syntax/Printer.hs
index f96f737..5b0743f 100644
--- a/src/LambdaCalculus/Syntax/Printer.hs
+++ b/src/LambdaCalculus/Syntax/Printer.hs
@@ -5,8 +5,8 @@ import LambdaCalculus.Syntax.Base
 import Data.Functor.Base (NonEmptyF (NonEmptyF))
 import Data.Functor.Foldable (cata)
 import Data.List.NonEmpty (toList)
-import Data.Text.Lazy (fromStrict, toStrict, intercalate, unwords)
-import Data.Text.Lazy.Builder (Builder, fromText, fromLazyText, toLazyText)
+import Data.Text.Lazy (fromStrict, toStrict, intercalate, unwords, singleton)
+import Data.Text.Lazy.Builder (Builder, fromText, fromLazyText, toLazyText, fromString)
 import Prelude hiding (unwords)
 
 -- I'm surprised this isn't in base somewhere.
@@ -52,7 +52,7 @@ ambiguous (_, t) = group t
 unparseAST :: AST -> Text
 unparseAST = toStrict . toLazyText . snd . cata \case
   VarF name -> tag Finite $ fromText name
-  AppF ef (unsnoc -> (exs, efinal)) -> tag Ambiguous $ foldr (\e es' -> ambiguous e <> " " <> es') (final efinal) (ef : exs)
+  AppF ef exs -> unparseApp ef exs
   AbsF names body -> tag Block $
     let names' = fromLazyText (unwords $ map fromStrict $ toList names)
     in "λ" <> names' <> ". " <> unambiguous body
@@ -61,3 +61,36 @@ unparseAST = toStrict . toLazyText . snd . cata \case
       unparseDef (name, val) = fromText name <> " = " <> unambiguous val
       defs' = fromLazyText (intercalate "; " $ map (toLazyText . unparseDef) $ toList defs)
     in "let " <> defs' <> " in " <> unambiguous body
+  CtrF ctr e -> unparseCtr ctr e
+  CaseF pats ->
+    let pats' = fromLazyText $ intercalate "; " $ map (toLazyText . unparsePat) pats
+    in tag Finite $ "{ " <> pats' <> " }"
+  PNatF n -> tag Finite $ fromString $ show n
+  PListF es ->
+    let es' = fromLazyText $ intercalate ", " $ map (toLazyText . unambiguous) es
+    in tag Finite $ "[" <> es' <> "]"
+  PStrF s -> tag Finite $ "\"" <> fromText s <> "\""
+  PCharF c -> tag Finite $ "'" <> fromLazyText (singleton c)
+  where
+    unparseApp :: Tagged Builder -> NonEmpty (Tagged Builder) -> Tagged Builder
+    unparseApp ef (unsnoc -> (exs, efinal))
+      = tag Ambiguous $ foldr (\e es' -> ambiguous e <> " " <> es') (final efinal) (ef : exs)
+
+    unparseCtr :: Ctr -> [Tagged Builder] -> Tagged Builder
+    -- Fully-applied special syntax forms
+    unparseCtr CPair [x, y] = tag Finite $ "(" <> unambiguous x <> ", "  <> unambiguous y <> ")"
+    unparseCtr CCons [x, y] = tag Finite $ "(" <> unambiguous x <> " : " <> unambiguous y <> ")"
+    -- Partially-applied syntax forms
+    unparseCtr CUnit  [] = tag Finite "()"
+    unparseCtr CPair  [] = tag Finite "(,)"
+    unparseCtr CLeft  [] = tag Finite "Left"
+    unparseCtr CRight [] = tag Finite "Right"
+    unparseCtr CZero  [] = tag Finite "Z"
+    unparseCtr CSucc  [] = tag Finite "S"
+    unparseCtr CNil   [] = tag Finite "[]"
+    unparseCtr CCons  [] = tag Finite "(:)"
+    unparseCtr CChar  [] = tag Finite "Char"
+    unparseCtr ctr (x:xs) = unparseApp (unparseCtr ctr []) (x :| xs)
+
+    unparsePat (Pat ctr ns e)
+      = unambiguous (unparseCtr ctr (map (tag Finite . fromText) ns)) <> " -> " <> unambiguous e