diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,14 @@
+# 0.5.0.0
+
+- Modularized library
+
+- `Fcf.Utils`:
+
+    + Added `TError`
+    + Renamed `Collapse` to `Constraints`
+
+- `Fcf.Data.List`: Added `Cons`, `Last`, `Init`, `Elem`
+
 # 0.4.0.0
 
 - New functions (blmage)
diff --git a/first-class-families.cabal b/first-class-families.cabal
--- a/first-class-families.cabal
+++ b/first-class-families.cabal
@@ -1,5 +1,5 @@
 name:                first-class-families
-version:             0.4.0.0
+version:             0.5.0.0
 synopsis:
   First class type families
 description:
@@ -24,8 +24,17 @@
   hs-source-dirs:      src
   exposed-modules:
     Fcf
+    Fcf.Core
+    Fcf.Combinators
+    Fcf.Data.Bool
+    Fcf.Data.Common
+    Fcf.Data.List
+    Fcf.Data.Nat
+    Fcf.Classes
+    Fcf.Utils
   build-depends:
-    base >= 4.9 && < 5
+    -- This upper bound is conservative.
+    base >= 4.9 && < 4.13
   ghc-options:         -Wall
   default-language:    Haskell2010
 
diff --git a/src/Fcf.hs b/src/Fcf.hs
--- a/src/Fcf.hs
+++ b/src/Fcf.hs
@@ -1,12 +1,4 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
 
 -- | First-class type families
 --
@@ -39,361 +31,117 @@
 -- >     TypeOperators,
 -- >     UndecidableInstances #-}
 
-module Fcf where
-
-import Data.Kind (Type, Constraint)
-import GHC.TypeLits (Symbol, Nat, TypeError, ErrorMessage(..))
-import qualified GHC.TypeLits as TL
-
--- * First-class type families
-
--- | Kind of type-level expressions indexed by their result type.
-type Exp a = a -> Type
-
--- | Expression evaluator.
-type family Eval (e :: Exp a) :: a
-
--- ** Monadic operations
-
-infixr 1 =<<, <=<
-infixl 4 <$>, <*>
-
-data Pure :: a -> Exp a
-type instance Eval (Pure x) = x
-
-data Pure1 :: (a -> b) -> a -> Exp b
-type instance Eval (Pure1 f x) = f x
-
-data Pure2 :: (a -> b -> c) -> a -> b -> Exp c
-type instance Eval (Pure2 f x y) = f x y
-
-data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d
-type instance Eval (Pure3 f x y z) = f x y z
-
-data (=<<) :: (a -> Exp b) -> Exp a -> Exp b
-type instance Eval (k =<< e) = Eval (k (Eval e))
-
-data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c
-type instance Eval ((f <=< g) x) = Eval (f (Eval (g x)))
-
-type LiftM = (=<<)
-
-data LiftM2 :: (a -> b -> Exp c) -> Exp a -> Exp b -> Exp c
-type instance Eval (LiftM2 f x y) = Eval (f (Eval x) (Eval y))
-
-data LiftM3 :: (a -> b -> c -> Exp d) -> Exp a -> Exp b -> Exp c -> Exp d
-type instance Eval (LiftM3 f x y z) = Eval (f (Eval x) (Eval y) (Eval z))
-
-data Join :: Exp (Exp a) -> Exp a
-type instance Eval (Join e) = Eval (Eval e)
-
-data (<$>) :: (a -> b) -> Exp a -> Exp b
-type instance Eval (f <$> e) = f (Eval e)
-
-data (<*>) :: Exp (a -> b) -> Exp a -> Exp b
-type instance Eval (f <*> e) = Eval f (Eval e)
-
--- ** More combinators
-
-data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c
-type instance Eval (Flip f y x) = Eval (f x y)
-
-data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
-type instance Eval (Uncurry f '(x, y)) = Eval (f x y)
-
-data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c
-type instance Eval (UnEither f g ('Left  x)) = Eval (f x)
-type instance Eval (UnEither f g ('Right y)) = Eval (g y)
-
-data ConstFn :: a -> b -> Exp a
-type instance Eval (ConstFn a _b) = a
-
--- ** Tuples
-
-data Fst :: (a, b) -> Exp a
-type instance Eval (Fst '(a, _b)) = a
-
-data Snd :: (a, b) -> Exp b
-type instance Eval (Snd '(_a, b)) = b
-
-infixr 3 ***
-
--- | Equivalent to 'Bimap'.
-data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
-type instance Eval ((***) f f' '(b, b')) = '(Eval (f b), Eval (f' b'))
-
--- ** Lists
-
-data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b
-type instance Eval (Foldr f y '[]) = y
-type instance Eval (Foldr f y (x ': xs)) = Eval (f x (Eval (Foldr f y xs)))
-
--- | N.B.: This is equivalent to a 'Foldr' flipped.
-data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
-type instance Eval (UnList y f xs) = Eval (Foldr f y xs)
-
-data (++) :: [a] -> [a] -> Exp [a]
-type instance Eval ((++) '[] ys) = ys
-type instance Eval ((++) (x ': xs) ys) = x ': Eval ((++) xs ys)
-
-data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
-type instance Eval (Filter _p '[]) = '[]
-type instance Eval (Filter p (a ': as)) =
-  If (Eval (p a))
-    (a ': Eval (Filter p as))
-    (Eval (Filter p as))
-
-data Head :: [a] -> Exp (Maybe a)
-type instance Eval (Head '[]) = 'Nothing
-type instance Eval (Head (a ': _as)) = 'Just a
-
-data Tail :: [a] -> Exp (Maybe [a])
-type instance Eval (Tail '[]) = 'Nothing
-type instance Eval (Tail (_a ': as)) = 'Just as
-
-data Null :: [a] -> Exp Bool
-type instance Eval (Null '[]) = 'True
-type instance Eval (Null (a ': as)) = 'False
-
-data Length :: [a] -> Exp Nat
-type instance Eval (Length '[]) = 0
-type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)
-
-data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
-type instance Eval (Find _p '[]) = 'Nothing
-type instance Eval (Find p (a ': as)) =
-  If (Eval (p a))
-    ('Just a)
-    (Eval (Find p as))
-
--- | Find the index of an element satisfying the predicate.
-data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
-type instance Eval (FindIndex _p '[]) = 'Nothing
-type instance Eval (FindIndex p (a ': as)) =
-  Eval (If (Eval (p a))
-    (Pure ('Just 0))
-    (Map ((+) 1) =<< FindIndex p as))
-
--- | Find an element associated with a key.
--- @
--- 'Lookup' :: k -> [(k, b)] -> 'Exp' ('Maybe' b)
--- @
-type Lookup (a :: k) (as :: [(k, b)]) =
-  (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))
-
--- | Modify an element at a given index.
---
--- The list is unchanged if the index is out of bounds.
-data SetIndex :: Nat -> a -> [a] -> Exp [a]
-type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as
-
-type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where
-  SetIndexImpl _n _a' '[] = '[]
-  SetIndexImpl 0 a' (_a ': as) = a' ': as
-  SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as
-
-data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
-type instance Eval (ZipWith _f '[] _bs) = '[]
-type instance Eval (ZipWith _f _as '[]) = '[]
-type instance Eval (ZipWith f (a ': as) (b ': bs)) =
-  Eval (f a b) ': Eval (ZipWith f as bs)
-
--- |
--- @
--- 'Zip' :: [a] -> [b] -> 'Exp' [(a, b)]
--- @
-type Zip = ZipWith (Pure2 '(,))
-
-data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
-type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))
-
-data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
-type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
-
--- ** Maybe
-
-data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
-type instance Eval (UnMaybe y f 'Nothing) = Eval y
-type instance Eval (UnMaybe y f ('Just x)) = Eval (f x)
-
-data FromMaybe :: k -> Maybe k -> Exp k
-type instance Eval (FromMaybe a 'Nothing)   = a
-type instance Eval (FromMaybe _a ('Just b)) = b
-
-data IsJust :: Maybe a -> Exp Bool
-type instance Eval (IsJust ('Just _a)) = 'True
-type instance Eval (IsJust 'Nothing) = 'False
-
-data IsNothing :: Maybe a -> Exp Bool
-type instance Eval (IsNothing ('Just _a)) = 'False
-type instance Eval (IsNothing 'Nothing) = 'True
-
--- ** Either
-
-data IsLeft :: Either a b -> Exp Bool
-type instance Eval (IsLeft ('Left _a)) = 'True
-type instance Eval (IsLeft ('Right _a)) = 'False
-
-data IsRight :: Either a b -> Exp Bool
-type instance Eval (IsRight ('Left _a)) = 'False
-type instance Eval (IsRight ('Right _a)) = 'True
-
--- ** Overloaded functions
-
--- | Type-level 'fmap' for type-level functors.
-data Map :: (a -> Exp b) -> f a -> Exp (f b)
-
-type instance Eval (Map f '[]) = '[]
-type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)
-
-type instance Eval (Map f 'Nothing) = 'Nothing
-type instance Eval (Map f ('Just a)) = 'Just (Eval (f a))
-
-type instance Eval (Map f ('Left x)) = 'Left x
-type instance Eval (Map f ('Right a)) = 'Right (Eval (f a))
-
-type instance Eval (Map f '(x, a)) =
-  '(x, Eval (f a))
-type instance Eval (Map f '(x, y, a)) =
-  '(x, y, Eval (f a))
-type instance Eval (Map f '(x, y, z, a)) =
-  '(x, y, z, Eval (f a))
-type instance Eval (Map f '(x, y, z, w, a)) =
-  '(x, y, z, w, Eval (f a))
-
-data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
-
-type instance Eval (Bimap f g '(x, y)) = '(Eval (f x), Eval (g y))
-
-type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))
-type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))
-
--- ** Bool
-
--- | N.B.: The order of the two branches is the opposite of "if":
--- @UnBool ifFalse ifTrue bool@.
---
--- This mirrors the default order of constructors:
---
--- @
--- data Bool = False | True
--- ----------- False < True
--- @
-data UnBool :: Exp a -> Exp a -> Bool -> Exp a
-type instance Eval (UnBool fal tru 'False) = Eval fal
-type instance Eval (UnBool fal tru 'True ) = Eval tru
-
-infixr 2 ||
-infixr 3 &&
-
-data (||) :: Bool -> Bool -> Exp Bool
-type instance Eval ('True || b) = 'True
-type instance Eval (a || 'True) = 'True
-type instance Eval ('False || b) = b
-type instance Eval (a || 'False) = a
-
-data (&&) :: Bool -> Bool -> Exp Bool
-type instance Eval ('False && b) = 'False
-type instance Eval (a && 'False) = 'False
-type instance Eval ('True && b) = b
-type instance Eval (a && 'True) = a
-
-data Not :: Bool -> Exp Bool
-type instance Eval (Not 'True)  = 'False
-type instance Eval (Not 'False) = 'True
-
--- | A conditional choosing the first branch whose guard @a -> 'Exp' 'Bool'@
--- accepts a given value @a@.
---
--- === Example
---
--- @
--- type UnitPrefix n = 'Eval' ('Guarded' n
---   '[ 'TyEq' 0 \'':=' 'Pure' \"\"
---    , 'TyEq' 1 \'':=' 'Pure' \"deci\"
---    , 'TyEq' 2 \'':=' 'Pure' \"hecto\"
---    , 'TyEq' 3 \'':=' 'Pure' \"kilo\"
---    , 'TyEq' 6 \'':=' 'Pure' \"mega\"
---    , 'TyEq' 9 \'':=' 'Pure' \"giga\"
---    , 'Otherwise' \'':=' 'Error' "Something else"
---    ])
--- @
-data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b
-type instance Eval (Guarded x ((p ':= y) ': ys)) =
-    Eval (If (Eval (p x)) y (Guarded x ys))
-
--- | A fancy-looking pair type to use with 'Guarded'.
-data Guard a b = a := b
-infixr 0 :=
+module Fcf
+  ( -- * First-class type families
 
--- | A catch-all guard for 'Guarded'.
-type Otherwise = ConstFn 'True
+    Exp
+  , Eval
+  , type (@@)
 
--- ** Nat
+    -- ** Functional combinators
 
-data (+) :: Nat -> Nat -> Exp Nat
-type instance Eval ((+) a b) = a TL.+ b
+  , Pure
+  , Pure1
+  , Pure2
+  , Pure3
+  , type (=<<)
+  , type (<=<)
+  , LiftM
+  , LiftM2
+  , LiftM3
+  , Join
+  , type (<$>)
+  , type (<*>)
+  , Flip
+  , ConstFn
+  , type ($)
 
-data (-) :: Nat -> Nat -> Exp Nat
-type instance Eval ((-) a b) = a TL.- b
+    -- * Operations on common types
 
-data (*) :: Nat -> Nat -> Exp Nat
-type instance Eval ((Fcf.*) a b) = a TL.* b
+    -- ** Pairs
 
-data (^) :: Nat -> Nat -> Exp Nat
-type instance Eval ((^) a b) = a TL.^ b
+  , Uncurry
+  , Fst
+  , Snd
+  , type (***)
 
-data (<=) :: Nat -> Nat -> Exp Bool
-type instance Eval ((<=) a b) = a TL.<=? b
+    -- ** Either
 
-data (>=) :: Nat -> Nat -> Exp Bool
-type instance Eval ((>=) a b) = b TL.<=? a
+  , UnEither
+  , IsLeft
+  , IsRight
 
-data (<) :: Nat -> Nat -> Exp Bool
-type instance Eval ((<) a b) = Eval (Not =<< (a >= b))
+    -- ** Maybe
 
-data (>) :: Nat -> Nat -> Exp Bool
-type instance Eval ((>) a b) = Eval (Not =<< (a <= b))
+  , UnMaybe
+  , FromMaybe
+  , IsNothing
+  , IsJust
 
--- ** Other
+    -- ** Lists
 
-data Error :: Symbol -> Exp a
-type instance Eval (Error msg) = TypeError ('Text msg)
+  , Foldr
+  , UnList
+  , type (++)
+  , Filter
+  , Head
+  , Tail
+  , Null
+  , Length
+  , Find
+  , FindIndex
+  , Lookup
+  , SetIndex
+  , ZipWith
+  , Zip
+  , Unzip
+  , Cons2
 
-data Collapse :: [Constraint] -> Exp Constraint
-type instance Eval (Collapse '[]) = () ~ ()
-type instance Eval (Collapse (a ': as)) = (a, Eval (Collapse as))
+    -- ** Bool
 
-data TyEq :: a -> b -> Exp Bool
-type instance Eval (TyEq a b) = TyEqImpl a b
+  , UnBool
+  , type (||)
+  , type (&&)
+  , Not
 
-type family TyEqImpl (a :: k) (b :: k) :: Bool where
-  TyEqImpl a a = 'True
-  TyEqImpl a b = 'False
+    -- *** Multi-way if
 
-infixr 0 $
+  , Guarded
+  , Guard((:=))
+  , Otherwise
 
--- | Note that this denotes the identity function, so @($) f@ can usually be
--- replaced with @f@.
-data ($) :: (a -> Exp b) -> a -> Exp b
-type instance Eval (($) f a) = Eval (f a)
+    -- ** Nat
 
--- | A stuck type that can be used like a type-level 'undefined'.
-type family Stuck :: a
+  , type (+)
+  , type (-)
+  , type (Fcf.Data.Nat.*)
+  , type (^)
+  , type (<=)
+  , type (>=)
+  , type (<)
+  , type (>)
 
--- * Helpful shorthands
+    -- * Overloaded operations
 
--- | Apply and evaluate a unary type function.
-type f @@ x = Eval (f x)
+  , Map
+  , Bimap
 
--- * Reification
+    -- * Miscellaneous
 
-class IsBool (b :: Bool) where
-  _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r
+  , Error
+  , Constraints
+  , TyEq
+  , Stuck
+  , IsBool(_If)
+  , If
 
-instance IsBool 'True  where _If a _ = a
-instance IsBool 'False where _If _ b = b
+  ) where
 
-type family   If (b :: Bool) (x :: k) (y :: k) :: k
-type instance If 'True   x _y = x
-type instance If 'False _x  y = y
+import Fcf.Core
+import Fcf.Combinators
+import Fcf.Data.Bool
+import Fcf.Data.Common
+import Fcf.Data.List
+import Fcf.Data.Nat
+import Fcf.Classes
+import Fcf.Utils
diff --git a/src/Fcf/Classes.hs b/src/Fcf/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Classes.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators #-}
+
+-- | Overloaded functions.
+module Fcf.Classes
+  ( Map
+  , Bimap
+  ) where
+
+import Fcf.Core
+
+-- | Type-level 'fmap' for type-level functors.
+data Map :: (a -> Exp b) -> f a -> Exp (f b)
+
+-- []
+type instance Eval (Map f '[]) = '[]
+type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)
+
+-- Maybe
+type instance Eval (Map f 'Nothing) = 'Nothing
+type instance Eval (Map f ('Just a)) = 'Just (Eval (f a))
+
+-- Either
+type instance Eval (Map f ('Left x)) = 'Left x
+type instance Eval (Map f ('Right a)) = 'Right (Eval (f a))
+
+-- Tuples
+type instance Eval (Map f '(x, a)) =
+  '(x, Eval (f a))
+type instance Eval (Map f '(x, y, a)) =
+  '(x, y, Eval (f a))
+type instance Eval (Map f '(x, y, z, a)) =
+  '(x, y, z, Eval (f a))
+type instance Eval (Map f '(x, y, z, w, a)) =
+  '(x, y, z, w, Eval (f a))
+
+-- | Type-level 'Data.Bifunctor.bimap'.
+data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
+
+-- (,)
+type instance Eval (Bimap f g '(x, y)) = '(Eval (f x), Eval (g y))
+
+-- Either
+type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))
+type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))
diff --git a/src/Fcf/Combinators.hs b/src/Fcf/Combinators.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Combinators.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | General fcf combinators.
+module Fcf.Combinators
+  ( Pure
+  , Pure1
+  , Pure2
+  , Pure3
+  , type (=<<)
+  , type (<=<)
+  , LiftM
+  , LiftM2
+  , LiftM3
+  , Join
+  , type (<$>)
+  , type (<*>)
+  , Flip
+  , ConstFn
+  , type ($)
+  ) where
+
+import Fcf.Core
+
+-- ** Monadic operations
+
+infixr 1 =<<, <=<
+infixl 4 <$>, <*>
+
+data Pure :: a -> Exp a
+type instance Eval (Pure x) = x
+
+data Pure1 :: (a -> b) -> a -> Exp b
+type instance Eval (Pure1 f x) = f x
+
+data Pure2 :: (a -> b -> c) -> a -> b -> Exp c
+type instance Eval (Pure2 f x y) = f x y
+
+data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d
+type instance Eval (Pure3 f x y z) = f x y z
+
+data (=<<) :: (a -> Exp b) -> Exp a -> Exp b
+type instance Eval (k =<< e) = Eval (k (Eval e))
+
+data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c
+type instance Eval ((f <=< g) x) = Eval (f (Eval (g x)))
+
+type LiftM = (=<<)
+
+data LiftM2 :: (a -> b -> Exp c) -> Exp a -> Exp b -> Exp c
+type instance Eval (LiftM2 f x y) = Eval (f (Eval x) (Eval y))
+
+data LiftM3 :: (a -> b -> c -> Exp d) -> Exp a -> Exp b -> Exp c -> Exp d
+type instance Eval (LiftM3 f x y z) = Eval (f (Eval x) (Eval y) (Eval z))
+
+data Join :: Exp (Exp a) -> Exp a
+type instance Eval (Join e) = Eval (Eval e)
+
+data (<$>) :: (a -> b) -> Exp a -> Exp b
+type instance Eval (f <$> e) = f (Eval e)
+
+data (<*>) :: Exp (a -> b) -> Exp a -> Exp b
+type instance Eval (f <*> e) = Eval f (Eval e)
+
+data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c
+type instance Eval (Flip f y x) = Eval (f x y)
+
+data ConstFn :: a -> b -> Exp a
+type instance Eval (ConstFn a _b) = a
+
+-- | Note that this denotes the identity function, so @($) f@ can usually be
+-- replaced with @f@.
+data ($) :: (a -> Exp b) -> a -> Exp b
+type instance Eval (($) f a) = Eval (f a)
+
+infixr 0 $
diff --git a/src/Fcf/Core.hs b/src/Fcf/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Core.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators #-}
+
+-- | The 'Eval' family.
+
+module Fcf.Core
+  ( Exp
+  , Eval
+  , type (@@)
+  ) where
+
+import Data.Kind (Type)
+
+-- * First-class type families
+
+-- | Kind of type-level expressions indexed by their result type.
+type Exp a = a -> Type
+
+-- | Expression evaluator.
+type family Eval (e :: Exp a) :: a
+
+-- ** Miscellaneous
+
+-- | Apply and evaluate a unary type function.
+type f @@ x = Eval (f x)
+
diff --git a/src/Fcf/Data/Bool.hs b/src/Fcf/Data/Bool.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/Bool.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Booleans.
+--
+-- Note that the operations from this module conflict with
+-- "Data.Type.Bool".
+module Fcf.Data.Bool
+  ( UnBool
+  , type (||)
+  , type (&&)
+  , Not
+
+    -- *** Multi-way if
+
+  , Guarded
+  , Guard((:=))
+  , Otherwise
+  ) where
+
+import Fcf.Core
+import Fcf.Combinators (ConstFn)
+import Fcf.Utils
+
+-- | N.B.: The order of the two branches is the opposite of "if":
+-- @UnBool ifFalse ifTrue bool@.
+--
+-- This mirrors the default order of constructors:
+--
+-- @
+-- data Bool = False | True
+-- ----------- False < True
+-- @
+data UnBool :: Exp a -> Exp a -> Bool -> Exp a
+type instance Eval (UnBool fal tru 'False) = Eval fal
+type instance Eval (UnBool fal tru 'True ) = Eval tru
+
+infixr 2 ||
+infixr 3 &&
+
+data (||) :: Bool -> Bool -> Exp Bool
+type instance Eval ('True || b) = 'True
+type instance Eval (a || 'True) = 'True
+type instance Eval ('False || b) = b
+type instance Eval (a || 'False) = a
+
+data (&&) :: Bool -> Bool -> Exp Bool
+type instance Eval ('False && b) = 'False
+type instance Eval (a && 'False) = 'False
+type instance Eval ('True && b) = b
+type instance Eval (a && 'True) = a
+
+data Not :: Bool -> Exp Bool
+type instance Eval (Not 'True)  = 'False
+type instance Eval (Not 'False) = 'True
+
+-- | A conditional choosing the first branch whose guard @a -> 'Exp' 'Bool'@
+-- accepts a given value @a@.
+--
+-- === Example
+--
+-- @
+-- type UnitPrefix n = 'Eval' ('Guarded' n
+--   '[ 'TyEq' 0 \'':=' 'Pure' \"\"
+--    , 'TyEq' 1 \'':=' 'Pure' \"deci\"
+--    , 'TyEq' 2 \'':=' 'Pure' \"hecto\"
+--    , 'TyEq' 3 \'':=' 'Pure' \"kilo\"
+--    , 'TyEq' 6 \'':=' 'Pure' \"mega\"
+--    , 'TyEq' 9 \'':=' 'Pure' \"giga\"
+--    , 'Otherwise' \'':=' 'Error' "Something else"
+--    ])
+-- @
+data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b
+type instance Eval (Guarded x ((p ':= y) ': ys)) =
+    Eval (If (Eval (p x)) y (Guarded x ys))
+
+-- | A fancy-looking pair type to use with 'Guarded'.
+data Guard a b = a := b
+infixr 0 :=
+
+-- | A catch-all guard for 'Guarded'.
+type Otherwise = ConstFn 'True
+
diff --git a/src/Fcf/Data/Common.hs b/src/Fcf/Data/Common.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/Common.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators #-}
+
+-- | Common data types: tuples, 'Either', 'Maybe'.
+module Fcf.Data.Common
+  ( -- ** Pairs
+
+    Uncurry
+  , Fst
+  , Snd
+  , type (***)
+
+    -- ** Either
+
+  , UnEither
+  , IsLeft
+  , IsRight
+
+    -- ** Maybe
+
+  , UnMaybe
+  , FromMaybe
+  , IsNothing
+  , IsJust
+  ) where
+
+import Fcf.Core
+
+-- ** Pairs
+
+data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c
+type instance Eval (Uncurry f '(x, y)) = Eval (f x y)
+
+data Fst :: (a, b) -> Exp a
+type instance Eval (Fst '(a, _b)) = a
+
+data Snd :: (a, b) -> Exp b
+type instance Eval (Snd '(_a, b)) = b
+
+infixr 3 ***
+
+-- | Equivalent to 'Bimap' for pairs.
+data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
+type instance Eval ((***) f f' '(b, b')) = '(Eval (f b), Eval (f' b'))
+
+-- ** Either
+
+data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c
+type instance Eval (UnEither f g ('Left  x)) = Eval (f x)
+type instance Eval (UnEither f g ('Right y)) = Eval (g y)
+
+data IsLeft :: Either a b -> Exp Bool
+type instance Eval (IsLeft ('Left _a)) = 'True
+type instance Eval (IsLeft ('Right _a)) = 'False
+
+data IsRight :: Either a b -> Exp Bool
+type instance Eval (IsRight ('Left _a)) = 'False
+type instance Eval (IsRight ('Right _a)) = 'True
+
+-- ** Maybe
+
+data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
+type instance Eval (UnMaybe y f 'Nothing) = Eval y
+type instance Eval (UnMaybe y f ('Just x)) = Eval (f x)
+
+data FromMaybe :: k -> Maybe k -> Exp k
+type instance Eval (FromMaybe a 'Nothing)   = a
+type instance Eval (FromMaybe _a ('Just b)) = b
+
+data IsNothing :: Maybe a -> Exp Bool
+type instance Eval (IsNothing ('Just _a)) = 'False
+type instance Eval (IsNothing 'Nothing) = 'True
+
+data IsJust :: Maybe a -> Exp Bool
+type instance Eval (IsJust ('Just _a)) = 'True
+type instance Eval (IsJust 'Nothing) = 'False
diff --git a/src/Fcf/Data/List.hs b/src/Fcf/Data/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/List.hs
@@ -0,0 +1,144 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Lists.
+module Fcf.Data.List
+  ( Foldr
+  , UnList
+  , Cons
+  , type (++)
+  , Filter
+  , Head
+  , Last
+  , Tail
+  , Init
+  , Null
+  , Length
+  , Find
+  , FindIndex
+  , Elem
+  , Lookup
+  , SetIndex
+  , ZipWith
+  , Zip
+  , Unzip
+  , Cons2
+  ) where
+
+import GHC.TypeLits (Nat)
+import qualified GHC.TypeLits as TL
+
+import Fcf.Core
+import Fcf.Combinators
+import Fcf.Classes
+import Fcf.Data.Common
+import Fcf.Data.Nat
+import Fcf.Utils
+
+data Cons :: a -> [a] -> Exp [a]
+type instance Eval (Cons a as) = a ': as
+
+data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b
+type instance Eval (Foldr f y '[]) = y
+type instance Eval (Foldr f y (x ': xs)) = Eval (f x (Eval (Foldr f y xs)))
+
+-- | N.B.: This is equivalent to a 'Foldr' flipped.
+data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
+type instance Eval (UnList y f xs) = Eval (Foldr f y xs)
+
+data (++) :: [a] -> [a] -> Exp [a]
+type instance Eval ((++) '[] ys) = ys
+type instance Eval ((++) (x ': xs) ys) = x ': Eval ((++) xs ys)
+
+data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
+type instance Eval (Filter _p '[]) = '[]
+type instance Eval (Filter p (a ': as)) =
+  If (Eval (p a))
+    (a ': Eval (Filter p as))
+    (Eval (Filter p as))
+
+data Head :: [a] -> Exp (Maybe a)
+type instance Eval (Head '[]) = 'Nothing
+type instance Eval (Head (a ': _as)) = 'Just a
+
+data Last :: [a] -> Exp (Maybe a)
+type instance Eval (Last '[]) = 'Nothing
+type instance Eval (Last (a ': '[])) = 'Just a
+type instance Eval (Last (a ': b ': as)) = Eval (Last (b ': as))
+
+data Init :: [a] -> Exp (Maybe [a])
+type instance Eval (Init '[]) = 'Nothing
+type instance Eval (Init (a ': '[])) = 'Just '[]
+type instance Eval (Init (a ': b ': as)) =
+  Eval (Map (Cons a) =<< (Init (b ': as)))
+
+data Tail :: [a] -> Exp (Maybe [a])
+type instance Eval (Tail '[]) = 'Nothing
+type instance Eval (Tail (_a ': as)) = 'Just as
+
+data Null :: [a] -> Exp Bool
+type instance Eval (Null '[]) = 'True
+type instance Eval (Null (a ': as)) = 'False
+
+data Length :: [a] -> Exp Nat
+type instance Eval (Length '[]) = 0
+type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)
+
+data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
+type instance Eval (Find _p '[]) = 'Nothing
+type instance Eval (Find p (a ': as)) =
+  If (Eval (p a))
+    ('Just a)
+    (Eval (Find p as))
+
+-- | Find the index of an element satisfying the predicate.
+data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
+type instance Eval (FindIndex _p '[]) = 'Nothing
+type instance Eval (FindIndex p (a ': as)) =
+  Eval (If (Eval (p a))
+    (Pure ('Just 0))
+    (Map ((+) 1) =<< FindIndex p as))
+
+type Elem a as = IsJust =<< FindIndex (TyEq a) as
+
+-- | Find an element associated with a key.
+-- @
+-- 'Lookup' :: k -> [(k, b)] -> 'Exp' ('Maybe' b)
+-- @
+type Lookup (a :: k) (as :: [(k, b)]) =
+  (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))
+
+-- | Modify an element at a given index.
+--
+-- The list is unchanged if the index is out of bounds.
+data SetIndex :: Nat -> a -> [a] -> Exp [a]
+type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as
+
+type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where
+  SetIndexImpl _n _a' '[] = '[]
+  SetIndexImpl 0 a' (_a ': as) = a' ': as
+  SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as
+
+data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
+type instance Eval (ZipWith _f '[] _bs) = '[]
+type instance Eval (ZipWith _f _as '[]) = '[]
+type instance Eval (ZipWith f (a ': as) (b ': bs)) =
+  Eval (f a b) ': Eval (ZipWith f as bs)
+
+-- |
+-- @
+-- 'Zip' :: [a] -> [b] -> 'Exp' [(a, b)]
+-- @
+type Zip = ZipWith (Pure2 '(,))
+
+data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
+type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))
+
+data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
+type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
+
diff --git a/src/Fcf/Data/Nat.hs b/src/Fcf/Data/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/Nat.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Natural numbers.
+--
+-- Note that the operators from this module conflict with "GHC.TypeLits" and
+-- "GHC.TypeNats".
+module Fcf.Data.Nat
+  ( -- * Reexported type
+    -- | From "GHC.TypeNats".
+
+    Nat
+
+    -- * Operations
+
+  , type (+)
+  , type (-)
+  , type (Fcf.Data.Nat.*)
+  , type (^)
+  , type (<=)
+  , type (>=)
+  , type (<)
+  , type (>)
+  ) where
+
+import GHC.TypeLits (Nat)
+import qualified GHC.TypeLits as TL
+
+import Fcf.Core
+import Fcf.Combinators
+import Fcf.Data.Bool (Not)
+
+data (+) :: Nat -> Nat -> Exp Nat
+type instance Eval ((+) a b) = a TL.+ b
+
+data (-) :: Nat -> Nat -> Exp Nat
+type instance Eval ((-) a b) = a TL.- b
+
+data (*) :: Nat -> Nat -> Exp Nat
+type instance Eval ((Fcf.Data.Nat.*) a b) = a TL.* b
+
+data (^) :: Nat -> Nat -> Exp Nat
+type instance Eval ((^) a b) = a TL.^ b
+
+data (<=) :: Nat -> Nat -> Exp Bool
+type instance Eval ((<=) a b) = a TL.<=? b
+
+data (>=) :: Nat -> Nat -> Exp Bool
+type instance Eval ((>=) a b) = b TL.<=? a
+
+data (<) :: Nat -> Nat -> Exp Bool
+type instance Eval ((<) a b) = Eval (Not =<< (a >= b))
+
+data (>) :: Nat -> Nat -> Exp Bool
+type instance Eval ((>) a b) = Eval (Not =<< (a <= b))
+
diff --git a/src/Fcf/Utils.hs b/src/Fcf/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Utils.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE
+    AllowAmbiguousTypes,
+    ConstraintKinds,
+    DataKinds,
+    PolyKinds,
+    RankNTypes,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators #-}
+
+-- | Miscellaneous families.
+module Fcf.Utils
+  ( Error
+  , TError
+  , Constraints
+  , TyEq
+  , Stuck
+  , IsBool(_If)
+
+    -- | From "Data.Type.Bool".
+  , If
+  ) where
+
+import Data.Kind (Constraint)
+import Data.Type.Bool (If)
+import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))
+
+import Fcf.Core
+
+-- | Type-level 'error'.
+data Error :: Symbol -> Exp a
+type instance Eval (Error msg) = TypeError ('Text msg)
+
+-- | 'TypeError' as a fcf.
+data TError :: ErrorMessage -> Exp a
+type instance Eval (TError msg) = TypeError msg
+
+-- | Conjunction of a list of constraints.
+data Constraints :: [Constraint] -> Exp Constraint
+type instance Eval (Constraints '[]) = (() :: Constraint)
+type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as))
+
+-- | Type equality.
+data TyEq :: a -> b -> Exp Bool
+type instance Eval (TyEq a b) = TyEqImpl a b
+
+type family TyEqImpl (a :: k) (b :: k) :: Bool where
+  TyEqImpl a a = 'True
+  TyEqImpl a b = 'False
+
+-- | A stuck type that can be used like a type-level 'undefined'.
+type family Stuck :: a
+
+-- * Reification
+
+class IsBool (b :: Bool) where
+  _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r
+
+instance IsBool 'True  where _If a _ = a
+instance IsBool 'False where _If _ b = b