diff --git a/quantification.cabal b/quantification.cabal
--- a/quantification.cabal
+++ b/quantification.cabal
@@ -1,22 +1,23 @@
-name:                quantification
-version:             0.1.2
-synopsis:            Data types and typeclasses to deal with universally and existentially quantified types
-description:         Please see README.md
-homepage:            https://github.com/andrewthad/quantification#readme
-license:             BSD3
-license-file:        LICENSE
-author:              Andrew Martin
-maintainer:          andrew.thaddeus@gmail.com
-copyright:           2016 Andrew Martin
-category:            Web
-build-type:          Simple
-cabal-version:       >=1.10
+name: quantification
+version: 0.2
+synopsis: Rage against the quantification
+description: Data types and typeclasses to deal with universally and existentially quantified types
+homepage: https://github.com/andrewthad/quantification#readme
+license: BSD3
+license-file: LICENSE
+author: Andrew Martin
+maintainer: andrew.thaddeus@gmail.com
+copyright: 2016 Andrew Martin
+category: Web
+build-type: Simple
+cabal-version: >=1.10
 
 library
   hs-source-dirs: src
   exposed-modules:
     Data.Exists
     Data.Monoid.Lifted
+    Topaz.Rec
   build-depends: 
       base >= 4.9 && < 5
     , ghc-prim >= 0.5 && < 0.6
@@ -24,6 +25,7 @@
     , aeson >= 0.11 && < 1.2
     , text >= 1.0 && < 2.0
     , path-pieces >= 0.2 && < 0.3
+    , vector >= 0.11 && < 0.13
   default-language: Haskell2010
 
 source-repository head
diff --git a/src/Data/Exists.hs b/src/Data/Exists.hs
--- a/src/Data/Exists.hs
+++ b/src/Data/Exists.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PolyKinds #-}
@@ -6,6 +9,8 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE CPP #-}
 
 {-# OPTIONS_GHC -Wall #-}
@@ -36,19 +41,33 @@
   , HashableForall(..)
   , PathPieceForall(..)
   , FromJSONForall(..)
+  , FromJSONExists(..)
   , ToJSONForall(..)
 #if MIN_VERSION_aeson(1,0,0) 
   , ToJSONKeyForall(..)
-  , FromJSONKeyForall(..)
+  , FromJSONKeyExists(..)
 #endif
+  , StorableForall(..)
     -- * Higher Rank Classes
   , EqForall2(..)
   , EqForallPoly2(..)
+  , ShowForall2(..)
+    -- * More Type Classes
+  , Sing
+  , SingList(..)
+  , Reify(..)
+  , Unreify(..)
     -- * Functions
+    -- ** Show
   , showsForall
   , showForall
+  , showsForall2
+  , showForall2
+    -- ** Defaulting
   , defaultEqForallPoly
   , defaultCompareForallPoly
+    -- ** Other
+  , unreifyList
   ) where
 
 import Data.Proxy (Proxy(..))
@@ -57,12 +76,13 @@
 import Data.Aeson (ToJSON(..),FromJSON(..))
 import Data.Hashable (Hashable(..))
 import Data.Text (Text)
-import Data.Functor.Classes (Eq1(..))
+import Data.Functor.Classes (Eq1(..),Show1(..))
 import Data.Functor.Sum (Sum(..))
 import Data.Functor.Product (Product(..))
 import Data.Functor.Compose (Compose(..))
 import GHC.Int (Int(..))
 import GHC.Prim (dataToTag#)
+import Foreign.Ptr (Ptr)
 import qualified Data.Aeson.Types as Aeson
 import qualified Text.Read as R
 import qualified Web.PathPieces as PP
@@ -109,12 +129,21 @@
 class ShowForall f where
   showsPrecForall :: Int -> f a -> ShowS
 
+class ShowForall2 f where
+  showsPrecForall2 :: Int -> f a b -> ShowS
+
 showsForall :: ShowForall f => f a -> ShowS
 showsForall = showsPrecForall 0
 
 showForall :: ShowForall f => f a -> String
 showForall x = showsForall x ""
 
+showsForall2 :: ShowForall2 f => f a b -> ShowS
+showsForall2 = showsPrecForall2 0
+
+showForall2 :: ShowForall2 f => f a b -> String
+showForall2 x = showsForall2 x ""
+
 class ReadForall f where
   readPrecForall :: R.ReadPrec (Exists f)
 
@@ -131,16 +160,19 @@
 class ToJSONKeyForall f where
   toJSONKeyForall :: ToJSONKeyFunctionForall f
 
-class FromJSONKeyForall f where
-  fromJSONKeyForall :: FromJSONKeyFunction (Exists f)
+class FromJSONKeyExists f where
+  fromJSONKeyExists :: FromJSONKeyFunction (Exists f)
 #endif
 
 class ToJSONForall f where
   toJSONForall :: f a -> Aeson.Value
 
 class FromJSONForall f where
-  parseJSONForall :: Aeson.Value -> Aeson.Parser (Exists f)
+  parseJSONForall :: Sing a -> Aeson.Value -> Aeson.Parser (f a)
 
+class FromJSONExists f where
+  parseJSONExists :: Aeson.Value -> Aeson.Parser (Exists f)
+
 class EnumForall f where
   toEnumForall :: Int -> Exists f
   fromEnumForall :: f a -> Int
@@ -156,8 +188,11 @@
 class SemigroupForall f where
   sappendForall :: f a -> f a -> f a
 
-class SemigroupForall f => MonoidForall f where
-  memptyForall :: f a
+class StorableForall (f :: k -> *) where
+  peekForall :: Sing a -> Ptr (f a) -> IO (f a)
+  pokeForall :: Ptr (f a) -> f a -> IO ()
+  sizeOfFunctorForall :: f a -> Int
+  sizeOfForall :: forall (a :: k). Proxy f -> Sing a -> Int
 
 --------------------
 -- Instances Below
@@ -178,9 +213,6 @@
 instance SemigroupForall Proxy where
   sappendForall _ _ = Proxy 
 
-instance MonoidForall Proxy where
-  memptyForall = Proxy
-
 instance EqForall ((:~:) a) where
   eqForall Refl Refl = True
 
@@ -213,8 +245,8 @@
     ToJSONKeyTextForall t e -> ToJSONKeyText (\(Exists a) -> t a) (\(Exists a) -> e a)
     ToJSONKeyValueForall v e -> ToJSONKeyValue (\x -> case x of Exists a -> v a) (\(Exists a) -> e a)
 
-instance (FromJSONKeyForall f, FromJSONForall f) => FromJSONKey (Exists f) where
-  fromJSONKey = fromJSONKeyForall
+instance (FromJSONKeyExists f, FromJSONExists f) => FromJSONKey (Exists f) where
+  fromJSONKey = fromJSONKeyExists
 #endif
 
 instance EqForallPoly f => Eq (Exists f) where
@@ -232,14 +264,19 @@
 instance ToJSONForall f => ToJSON (Exists f) where
   toJSON (Exists a) = toJSONForall a
 
-instance FromJSONForall f => FromJSON (Exists f) where
-  parseJSON v = parseJSONForall v
+instance FromJSONExists f => FromJSON (Exists f) where
+  parseJSON v = parseJSONExists v
 
 instance ShowForall f => Show (Exists f) where
   showsPrec p (Exists a) = showParen 
     (p >= 11) 
     (showString "Exists " . showsPrecForall 11 a)
 
+instance ShowForall2 f => Show (Exists2 f) where
+  showsPrec p (Exists2 a) = showParen 
+    (p >= 11) 
+    (showString "Exists " . showsPrecForall2 11 a)
+
 instance ReadForall f => Read (Exists f) where
   readPrec = R.parens $ R.prec 10 $ do
     R.Ident "Exists" <- R.lexP
@@ -280,6 +317,21 @@
 instance (Eq1 f, EqForallPoly g) => EqForallPoly (Compose f g) where
   eqForallPoly (Compose x) (Compose y) = liftEq eqForallPoly x y
 
+instance (Show1 f, ShowForall g) => ShowForall (Compose f g) where
+  showsPrecForall _ (Compose x) = showString "Compose " . liftShowsPrec showsPrecForall showListForall 11 x
+
+showListForall :: ShowForall f => [f a] -> ShowS
+showListForall = showList__ showsForall
+
+-- Copied from GHC.Show. I do not like to import internal modules
+-- if I can instead copy a small amount of code.
+showList__ :: (a -> ShowS) ->  [a] -> ShowS
+showList__ _     []     s = "[]" ++ s
+showList__ showx (x:xs) s = '[' : showx x (showl xs)
+  where
+    showl []     = ']' : s
+    showl (y:ys) = ',' : showx y (showl ys)
+
 instance (EqForall f, EqForall g) => EqForall (Sum f g) where
   eqForall (InL f1) (InL f2) = eqForall f1 f2
   eqForall (InR f1) (InR f2) = eqForall f1 f2
@@ -305,4 +357,35 @@
 getTagBox :: a -> Int
 getTagBox !x = I# (dataToTag# x)
 {-# INLINE getTagBox #-}
+
+type family Sing = (r :: k -> *) | r -> k
+
+type instance Sing = SingList
+
+class Unreify k where
+  unreify :: forall (a :: k) b. Sing a -> (Reify a => b) -> b
+
+class Reify a where
+  reify :: Sing a
+
+instance Reify '[] where
+  reify = SingListNil
+
+instance (Reify a, Reify as) => Reify (a ': as) where
+  reify = SingListCons reify reify
+
+class SemigroupForall f => MonoidForall f where
+  memptyForall :: Sing a -> f a
+
+data SingList :: [k] -> * where
+  SingListNil :: SingList '[]
+  SingListCons :: Sing r -> SingList rs -> SingList (r ': rs)
+
+unreifyList :: forall (as :: [k]) b. Unreify k
+  => SingList as
+  -> (Reify as => b)
+  -> b
+unreifyList SingListNil b = b
+unreifyList (SingListCons s ss) b = unreify s (unreifyList ss b)
+
 
diff --git a/src/Topaz/Rec.hs b/src/Topaz/Rec.hs
new file mode 100644
--- /dev/null
+++ b/src/Topaz/Rec.hs
@@ -0,0 +1,230 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+{-# OPTIONS_GHC -Wall #-}
+
+module Topaz.Rec
+  ( Rec(..)
+  , map
+  , traverse
+  , traverse_
+  , zipWith
+  , foldMap
+  , foldMap1
+  ) where
+
+import Prelude hiding (map,zipWith,foldMap,traverse)
+import Data.Exists
+import Data.Type.Equality
+import Data.Type.Coercion
+import Data.Foldable (foldrM)
+import Data.Proxy (Proxy(..))
+import Foreign.Ptr (castPtr,plusPtr)
+import Foreign.Storable (Storable(..))
+import Data.Semigroup (Semigroup)
+import Data.Hashable (Hashable(..))
+import qualified Data.Semigroup as SG
+import qualified Data.Vector as V
+import qualified Data.Aeson as AE
+import qualified Data.Aeson.Types as AET
+
+data Rec :: (k -> *) -> [k] -> * where
+  RecNil :: Rec f '[]
+  RecCons :: f r -> Rec f rs -> Rec f (r ': rs)
+
+instance TestEquality f => TestEquality (Rec f) where
+  testEquality RecNil RecNil = Just Refl
+  testEquality (RecCons x xs) (RecCons y ys) = do
+    Refl <- testEquality x y
+    Refl <- testEquality xs ys
+    Just Refl
+  testEquality _ _ = Nothing
+
+instance TestCoercion f => TestCoercion (Rec f) where
+  testCoercion RecNil RecNil = Just Coercion
+  testCoercion (RecCons x xs) (RecCons y ys) = do
+    Coercion <- testCoercion x y
+    Coercion <- testCoercion xs ys
+    Just Coercion
+  testCoercion _ _ = Nothing
+
+instance EqForall f => Eq (Rec f as) where
+  (==) = eqForall
+
+instance HashableForall f => HashableForall (Rec f) where
+  hashWithSaltForall s0 = go s0 where
+    go :: Int -> Rec f rs -> Int
+    go !s x = case x of
+      RecNil -> s
+      RecCons b bs -> go (hashWithSaltForall s b) bs
+
+instance HashableForall f => Hashable (Rec f as) where
+  hashWithSalt = hashWithSaltForall
+
+instance ShowForall f => ShowForall (Rec f) where
+  showsPrecForall p x = case x of
+    RecCons v vs -> showParen (p > 10)
+      $ showString "RecCons "
+      . showsPrecForall 11 v
+      . showString " "
+      . showsPrecForall 11 vs
+    RecNil -> showString "RecNil"
+
+instance ShowForall f => Show (Rec f as) where
+  showsPrec = showsPrecForall
+
+instance EqForall f => EqForall (Rec f) where
+  eqForall RecNil RecNil = True
+  eqForall (RecCons a as) (RecCons b bs) =
+    eqForall a b && eqForall as bs
+
+instance OrdForall f => Ord (Rec f as) where
+  compare = compareForall
+
+instance OrdForall f => OrdForall (Rec f) where
+  compareForall RecNil RecNil = EQ
+  compareForall (RecCons a as) (RecCons b bs) =
+    mappend (compareForall a b) (compareForall as bs)
+
+instance SemigroupForall f => Semigroup (Rec f as) where
+  (<>) = zipWith sappendForall
+
+instance (MonoidForall f, Reify as) => Monoid (Rec f as) where
+  mempty = map memptyForall (singListToRec reify)
+  mappend = zipWith sappendForall
+
+instance MonoidForall f => MonoidForall (Rec f) where
+  memptyForall SingListNil = RecNil
+  memptyForall (SingListCons s ss) = RecCons (memptyForall s) (memptyForall ss)
+
+instance SemigroupForall f => SemigroupForall (Rec f) where
+  sappendForall = zipWith sappendForall
+
+instance ToJSONForall f => AE.ToJSON (Rec f as) where
+  toJSON = toJSONForall
+
+instance ToJSONForall f => ToJSONForall (Rec f) where
+  toJSONForall = AE.toJSON . go
+    where
+    go :: forall g xs. ToJSONForall g => Rec g xs -> [AE.Value]
+    go RecNil = []
+    go (RecCons x xs) = toJSONForall x : go xs
+
+instance (FromJSONForall f, Reify as) => AE.FromJSON (Rec f as) where
+  parseJSON = parseJSONForall reify
+
+instance FromJSONForall f => FromJSONForall (Rec f) where
+  parseJSONForall s0 = AE.withArray "Rec" $ \vs -> do
+    let go :: SingList as -> Int -> AET.Parser (Rec f as)
+        go SingListNil !ix = if V.length vs == ix
+          then return RecNil
+          else fail "too many elements in array"
+        go (SingListCons s ss) !ix = if ix < V.length vs
+          then do
+            r <- parseJSONForall s (vs V.! ix)
+            rs <- go ss (ix + 1)
+            return (RecCons r rs)
+          else fail "not enough elements in array"
+    go s0 0
+
+instance StorableForall f => StorableForall (Rec f) where
+  sizeOfFunctorForall RecNil = 0
+  sizeOfFunctorForall (RecCons r rs) =
+    sizeOfFunctorForall r + sizeOfFunctorForall rs
+  sizeOfForall _ SingListNil = 0
+  sizeOfForall _ (SingListCons s ss) =
+    sizeOfForall (Proxy :: Proxy f) s + sizeOfForall (Proxy :: Proxy (Rec f)) ss
+  peekForall SingListNil _ = return RecNil
+  peekForall (SingListCons s ss) ptr = do
+    r <- peekForall s (castPtr ptr)
+    rs <- peekForall ss (plusPtr ptr (sizeOfForall (Proxy :: Proxy f) s))
+    return (RecCons r rs)
+  pokeForall _ RecNil = return ()
+  pokeForall ptr (RecCons r rs) = do
+    pokeForall (castPtr ptr) r
+    pokeForall (plusPtr ptr (sizeOfFunctorForall r)) rs
+
+instance (StorableForall f, Reify as) => Storable (Rec f as) where
+  sizeOf _ = sizeOfForall (Proxy :: Proxy (Rec f)) (reify :: SingList as)
+  alignment _ = sizeOf (undefined :: Rec f as)
+  poke = pokeForall
+  peek = peekForall (reify :: SingList as)
+
+instance FromJSONExists f => FromJSONExists (Rec f) where
+  parseJSONExists = AE.withArray "Rec" $ \vs -> 
+    foldrM go (Exists RecNil) vs
+    where
+    go :: forall g. FromJSONExists g => AE.Value -> Exists (Rec g) -> AET.Parser (Exists (Rec g))
+    go v (Exists rs) = do
+      Exists r <- parseJSONExists v :: AET.Parser (Exists g)
+      return (Exists (RecCons r rs))
+
+singListToRec :: SingList as -> Rec Sing as
+singListToRec SingListNil = RecNil
+singListToRec (SingListCons r rs) = RecCons r (singListToRec rs)
+
+map :: (forall x. f x -> g x) -> Rec f as -> Rec g as
+map _ RecNil = RecNil
+map f (RecCons x xs) = RecCons (f x) (map f xs)
+
+zipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs
+zipWith _ RecNil RecNil = RecNil
+zipWith f (RecCons a as) (RecCons b bs) =
+  RecCons (f a b) (zipWith f as bs)
+
+-- | Map each element of a record to a monoid and combine the results.
+foldMap :: forall f m rs. Monoid m
+  => (forall x. f x -> m)
+  -> Rec f rs
+  -> m
+foldMap f = go mempty
+  where
+  go :: forall ss. m -> Rec f ss -> m
+  go !m record = case record of
+    RecNil -> m
+    RecCons r rs -> go (mappend m (f r)) rs
+  {-# INLINABLE go #-}
+{-# INLINE foldMap #-}
+
+foldMap1 :: forall f m r rs. Semigroup m
+  => (forall x. f x -> m)
+  -> Rec f (r ': rs)
+  -> m
+foldMap1 f (RecCons b bs) = go (f b) bs
+  where
+  go :: forall ss. m -> Rec f ss -> m
+  go !m record = case record of
+    RecNil -> m
+    RecCons r rs -> go (m SG.<> (f r)) rs
+  {-# INLINABLE go #-}
+{-# INLINE foldMap1 #-}
+
+traverse
+  :: Applicative h
+  => (forall x. f x -> h (g x))
+  -> Rec f rs
+  -> h (Rec g rs)
+traverse _ RecNil = pure RecNil
+traverse f (RecCons x xs) = RecCons <$> f x <*> traverse f xs
+{-# INLINABLE traverse #-}
+
+traverse_
+  :: Applicative h
+  => (forall x. f x -> h b)
+  -> Rec f rs
+  -> h ()
+traverse_ _ RecNil = pure ()
+traverse_ f (RecCons x xs) = f x *> traverse_ f xs
+{-# INLINABLE traverse_ #-}
+