diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,19 @@
+Copyright Li-yao Xia (c) 2018
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the “Software”), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+of the Software, and to permit persons to whom the Software is furnished to do
+so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,8 @@
+# First-class type families [![Hackage](https://img.shields.io/hackage/v/first-class-families.svg)](https://hackage.haskell.org/package/first-class-families) [![Build Status](https://travis-ci.org/Lysxia/first-class-families.svg)](https://travis-ci.org/Lysxia/first-class-families)
+
+See `src/Fcf`.
+
+---
+
+Contributions are welcome. Feel free to open an issue or make a PR on
+[Github](https://github.com/Lysxia/first-class-families)!
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/first-class-families.cabal b/first-class-families.cabal
new file mode 100644
--- /dev/null
+++ b/first-class-families.cabal
@@ -0,0 +1,34 @@
+name:                first-class-families
+version:             0.1.0.0
+synopsis:
+  First class type families
+description:
+  First class type families,
+  eval-style defunctionalization
+  .
+  See "Fcf".
+homepage:            https://github.com/Lysxia/first-class-families#readme
+license:             MIT
+license-file:        LICENSE
+author:              Li-yao Xia
+maintainer:          lysxia@gmail.com
+copyright:           2018 Li-yao Xia
+category:            Other
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+tested-with:
+  GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3
+
+library
+  hs-source-dirs:      src
+  exposed-modules:
+    Fcf
+  build-depends:
+    base >= 4.9 && < 5
+  ghc-options:         -Wall
+  default-language:    Haskell2010
+
+source-repository head
+  type:     git
+  location: https://github.com/Lysxia/first-class-families
diff --git a/src/Fcf.hs b/src/Fcf.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf.hs
@@ -0,0 +1,156 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | First-class type families
+--
+-- For example, here is a regular type family:
+--
+-- @
+-- type family   FromMaybe (a :: k) (m :: Maybe k) :: k
+-- type instance FromMaybe a 'Nothing  = a
+-- type instance FromMaybe a ('Just b) = b
+-- @
+--
+-- With @Fcf@, it translates to a @data@ declaration:
+--
+-- @
+-- data FromMaybe :: k -> Maybe k -> 'Exp' k
+-- type instance 'Eval' (FromMaybe a 'Nothing)  = a
+-- type instance 'Eval' (FromMaybe a ('Just b)) = b
+-- @
+--
+-- - Fcfs can be higher-order.
+-- - The kind constructor 'Exp' is a monad: there's @('=<<')@ and 'Pure'.
+
+module Fcf 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
+
+-- ** 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)))
+
+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 higher-order 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 BimapPair :: (a -> Exp a') -> (b -> Exp b') -> (a, b) -> Exp (a', b')
+type instance Eval (BimapPair f g '(x, y)) = '(Eval (f x), Eval (g 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 BimapEither
+  :: (a -> Exp a') -> (b -> Exp b') -> Either a b -> Exp (Either a' b')
+type instance Eval (BimapEither f g ('Left  x)) = 'Left  (Eval (f x))
+type instance Eval (BimapEither f g ('Right y)) = 'Right (Eval (g y))
+
+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 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)))
+
+data Traverse :: (a -> Exp b) -> [a] -> Exp [b]
+type instance Eval (Traverse f '[]) = '[]
+type instance Eval (Traverse f (x ': xs)) = Eval (f x) ': Eval (Traverse f 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)
+
+-- | 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
+
+-- ** Primitives
+
+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
+
+-- * Helpful shorthands
+
+-- | Apply and evaluate a unary type function.
+type f @@ x = Eval (f x)
+
+-- * 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
+
+type family   If (b :: Bool) (x :: k) (y :: k) :: k
+type instance If 'True   x _y = x
+type instance If 'False _x  y = y