diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -24,6 +24,9 @@
 
 a' :: Bool
 a' = consume y' (\b f -> b && f == 0.2)
+
+q :: Bool
+q = select x' $ \b (f :: Float)-> b && f == 0.2
 ```
 
 This package is extremely experimental, and is subject to arbitrarily large changes.
diff --git a/src/Data/ForAll.hs b/src/Data/ForAll.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ForAll.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+module Data.ForAll (type ForAll) where
+
+import GHC.Exts (Constraint)
+
+type family ForAll c xs :: Constraint where
+  ForAll c '[] = ()
+  ForAll c (x ': xs) = (c x, ForAll c xs)
+
diff --git a/src/Data/Prodder.hs b/src/Data/Prodder.hs
--- a/src/Data/Prodder.hs
+++ b/src/Data/Prodder.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
@@ -31,8 +34,18 @@
   , tailN
   , initN
   , dropFirst
-  , Consume(consume, produce, extend1, cmap)
+  , Consume(consume, extend1, cmap, produceB)
+  , produce
+  , empty
+  , ToList(toList)
+  , type ForAll
+    -- ** Efficient Iterative Construction
+  , buildProd
+  , ProdBuilder
+  , consB
+  , emptyB
     -- * Type families
+  , Index
   , IndexIn
   , HasIndexIn
   , Consumer
@@ -45,20 +58,50 @@
   , Strengthen(strengthen)
     -- * Transforming extensible products
   , remap
+    -- * Picking out individual components of a product
+  , Selection(select)
+  , type FieldsFromSelector
+  , type Selector
+    -- * Efficiently building 'Prod's
   ) where
 
+import Data.ForAll (type ForAll)
 import Control.Monad (unless)
 import Control.Exception (catch, SomeException)
-import GHC.Exts (Any)
+import GHC.Exts (Any, Constraint)
 import Unsafe.Coerce (unsafeCoerce)
+import Data.Functor.Identity (Identity (..))
 import Data.Vector (Vector)
 import qualified Data.Vector as V
-import GHC.TypeLits (KnownNat, type (+), type (-), natVal, type (<=))
+import qualified Data.Vector.Mutable as MV
+import GHC.TypeLits (KnownNat, type (+), type (-), natVal, type (<=), Nat)
 import Data.Proxy (Proxy(Proxy))
+import Control.Monad.ST
+import Data.STRef (newSTRef, STRef, writeSTRef, readSTRef)
 
 -- | An extensible product type
-data Prod (xs :: [*]) = UnsafeProd { unProd :: Vector Any }
+newtype Prod (xs :: [*]) = UnsafeProd { unProd :: Vector Any }
 
+-- | A type for constructing products with linear memory use.
+newtype ProdBuilder (xs :: [*]) = UnsafeProdBuilder { unProdBuilder :: forall s. STRef s Int -> V.MVector s Any -> ST s () }
+
+-- | Cons an element onto the head of a 'ProdBuilder'.
+consB :: x -> ProdBuilder xs -> ProdBuilder (x ': xs)
+consB x (UnsafeProdBuilder b) = UnsafeProdBuilder \ref v -> withIncrement ref \i -> do
+  MV.write v i (unsafeCoerce x)
+
+-- | Empty 'ProdBuilder'.
+emptyB :: ProdBuilder '[]
+emptyB = UnsafeProdBuilder \_ _ -> pure ()
+
+-- | Execute a 'ProdBuilder', pulling out a 'Prod'.
+buildProd :: forall xs. (KnownNat (Length xs)) => ProdBuilder xs -> Prod xs
+buildProd (UnsafeProdBuilder bs) = UnsafeProd $ V.create do
+  ref <- newSTRef 0
+  x <- MV.new (fromInteger $ natVal (Proxy @(Length xs)))
+  bs ref x
+  pure x
+
 type role Prod representational
 
 -- | A type family for computing the index of a type in a list of types.
@@ -66,6 +109,11 @@
   IndexIn x (x ': xs) = 0
   IndexIn x (y ': xs) = 1 + IndexIn x xs
 
+-- | A type family for indexing into lists of types.
+type family Index (n :: Nat) (xs :: [k]) where
+  Index 0 (x ': xs) = x
+  Index n (_ ': xs) = Index (n - 1) xs
+
 -- | A type family for computing the length of a type level list
 type family Length (xs :: [k]) where
   Length '[] = 0
@@ -147,28 +195,46 @@
 -- extensible products.
 class Consume xs where
   consume :: forall r. Prod xs -> Consumer xs r -> r
-  produce :: (forall r. Consumer xs r -> r) -> Prod xs
-  extend1 :: x -> Consumer xs (Prod (x ': xs))
+  produceB :: (forall r. Consumer xs r -> r) -> ProdBuilder xs
+  extend1 :: x -> Consumer xs (ProdBuilder (x ': xs))
   cmap :: (r -> r') -> Consumer xs r -> Consumer xs r' 
 
+produce :: (KnownNat (Length xs), Consume xs) => (forall r. Consumer xs r -> r) -> Prod xs
+produce f = buildProd $ produceB f
+
+empty :: Prod '[]
+empty = buildProd $ produceB id
+
 instance Consume '[] where
   consume = flip const
   {-# INLINE CONLIKE consume #-}
-  produce x = UnsafeProd V.empty
-  {-# INLINE CONLIKE produce #-}
-  extend1 x = UnsafeProd (V.singleton (unsafeCoerce x))
+  produceB x = UnsafeProdBuilder \ref v -> pure ()
+  {-# INLINE CONLIKE produceB #-}
+  extend1 x = UnsafeProdBuilder \ref v -> withIncrement ref \i -> MV.write v i (unsafeCoerce x)
   {-# INLINE CONLIKE extend1 #-}
   cmap f x = f x
   {-# INLINE CONLIKE cmap #-}
 
+withIncrement :: STRef s Int -> (Int -> ST s x) -> ST s x
+withIncrement ref f = do
+  i <- readSTRef ref
+  x <- f i
+  writeSTRef ref (i + 1)
+  pure x
+
 instance Consume xs => Consume (x ': xs) where
   consume (UnsafeProd v) g = consume @xs (UnsafeProd (V.tail v)) $ g (unsafeCoerce $ v V.! 0)
   {-# INLINE CONLIKE consume #-}
-  produce g = g (extend1 @xs)
-  {-# INLINE CONLIKE produce #-}
+  produceB g = g (extend1 @xs)
+  {-# INLINE CONLIKE produceB #-}
   cmap f = fmap (cmap @xs f)
   {-# INLINE CONLIKE cmap #-}
-  extend1 (x1 :: x1) x = cmap @xs @(Prod (x ': xs)) @(Prod (x1 ': x ': xs)) (UnsafeProd . (V.singleton (unsafeCoerce x1) V.++) . unProd) (extend1 @xs x)
+  extend1 (x1 :: x1) x = cmap @xs @(ProdBuilder (x ': xs)) @(ProdBuilder (x1 ': x ': xs)) f (extend1 @xs x) where
+    f (UnsafeProdBuilder b) = UnsafeProdBuilder \ref v -> (withIncrement ref \i -> MV.write v i (unsafeCoerce x1)) >> b ref v
+    
+      
+     
+  -- cmap @xs @(Prod (x ': xs)) @(Prod (x1 ': x ': xs)) (UnsafeProd . (V.singleton (unsafeCoerce x1) V.++) . unProd) (extend1 @xs x)
   {-# INLINE CONLIKE extend1 #-}
 
 instance Eq (Prod '[]) where
@@ -188,3 +254,38 @@
 instance Strengthen xs '[] where
   strengthen = const (UnsafeProd V.empty)
   {-# INLINE CONLIKE strengthen #-}
+
+-- | A typeclass for creating a selection function which is valid on the given definition.
+type family Selector def fields a where
+  Selector def (field ': fields) a = Index field def -> Selector def fields a
+  Selector def '[] a = a
+
+-- | Extracts the fields intended from the given selector type.
+type family FieldsFromSelector def selector where
+  FieldsFromSelector def (a -> b) = IndexIn a def ': FieldsFromSelector def b
+  FieldsFromSelector def (Identity a) = '[]
+
+-- | A class for constructing the select function inductively.
+class Selection def selector a where
+  select :: Prod def -> selector -> a
+
+instance Selection def a a where
+  select _prod s = s
+  {-# INLINE CONLIKE select #-}
+
+instance (HasIndexIn x def, Selection def xs a) => Selection def (x -> xs) a where
+  select prod f = select @_ @_ @a prod (f (extract @x prod))
+  {-# INLINE CONLIKE select #-}
+
+-- | A class for turning a 'Prod' into a regular list using a
+-- function which takes an argument only constrained by a 'Constraint'
+-- each element of the product has.
+class ForAll c xs => ToList c xs where
+  toList :: (forall a. c a => a -> b) -> Prod xs -> [b]
+
+instance ToList c '[] where
+  toList _f _p = []
+
+instance (c x, ToList c xs) => ToList c (x ': xs) where
+  toList f p = f x : toList @c f (dropFirst p) where
+    x = extract @x p
diff --git a/src/Data/Summer.hs b/src/Data/Summer.hs
--- a/src/Data/Summer.hs
+++ b/src/Data/Summer.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -33,6 +35,7 @@
   , inject
   , inspect
   , consider
+  , considerFirst
   , Match(match, override, unmatch)
   , Unmatch
   -- * Type families
@@ -47,6 +50,9 @@
   -- * Transforming extensible sums
   , inmap
   , smap
+  -- * Applying Polymorphic Functions
+  , ApplyFunction(apply)
+  , type ForAll
   ) where
 
 import Control.Exception (catch, SomeException)
@@ -58,6 +64,7 @@
 import Control.Monad (unless)
 import Generics.SOP (Generic(..))
 import qualified Generics.SOP as SOP
+import Data.ForAll (type ForAll)
 
 -- | The extensible sum type, allowing inhabitants to be of any of the
 -- types in the given type list.
@@ -234,3 +241,16 @@
 instance (Unmatch xs ys, x `HasTagIn` ys) => Unmatch (x ': xs) ys where
   unmatchGo f = unmatchGo @xs (f (UnsafeInj (tag @x @ys) . unsafeCoerce @x))
   {-# INLINE CONLIKE unmatchGo #-}
+
+-- | Using functions which only require constraints which are satisfied by
+-- all members of the sum.
+class ForAll c xs => ApplyFunction c xs where
+  apply :: (forall a. c a => a -> y) -> Sum xs -> y
+
+instance ApplyFunction c '[] where
+  apply _f x = error "Impossible: empty sum"
+
+instance (c x, ApplyFunction c xs) => ApplyFunction c (x ': xs) where
+  apply f x = case considerFirst x of
+    Right x' -> f x'
+    Left xs -> apply @c f xs
diff --git a/summer.cabal b/summer.cabal
--- a/summer.cabal
+++ b/summer.cabal
@@ -1,6 +1,6 @@
 cabal-version:       2.4
 name:                summer
-version:             0.2.0.1
+version:             0.3.0.0
 synopsis:            An implementation of extensible products and sums
 description:         An implementation of extensible products and sums.
 license:             MIT
@@ -20,6 +20,7 @@
 
 library
   exposed-modules:     Data.Summer, Data.Prodder
+  other-modules:       Data.ForAll
   build-depends:       base >=4.12 && <4.16, vector >=0.12, generics-sop >=0.5
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
@@ -11,6 +12,12 @@
 main :: IO ()
 main = sumTest >> prodTest
 
+require :: Bool -> String -> IO ()
+require p s = unless p $ fail s
+
+requires :: [(Bool, String)] -> IO ()
+requires = mapM_ (uncurry require)
+
 prodTest :: IO ()
 prodTest = catchAndDisplay
   [ indexTest
@@ -27,43 +34,71 @@
     indexTest = do
       let index' = index @Int @'[Bool, Int]
           index'' = index @Bool @'[Bool, Int]
-      unless (index' == 1) $ fail ("Index " <> show index' <> " does not equal 1")
-      unless (index'' == 0) $ fail ("Index " <> show index'' <> " does not equal 0")
+      requires
+        [ (index' == 1, "Index " <> show index' <> " does not equal 1")
+        , (index'' == 0, "Index " <> show index'' <> " does not equal 0")
+        ]
     remapTest = do
       let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)
       let y = remap ((+ 10000000000000000000000000000) . toInteger @Int) x
       let z = remap not x
-      unless (y == produce (\f -> f 10000000000000000000000000010 True)) $ fail "Remapping does not work 1"
-      unless (z == produce (\f -> f 10 False)) $ fail "Remapping does not work 2"
+      requires
+        [ (y == produce (\f -> f 10000000000000000000000000010 True), "Remapping does not work 1")
+        , (z == produce (\f -> f 10 False), "Remapping does not work 2")
+        ]
     consumeAndProduceTest = do
       let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)
           y :: Bool = consume x (\n b -> n == 10 && b)
-      unless y $ fail "Consuming and producing does not work"
+      require y "Consuming and producing does not work"
     extractTest = do
       let x :: Prod '[Int, Bool] = produce (\f -> f 10 True)
           y :: Bool = extract x
           z :: Int = extract x
-      unless (z == 10 && y) $ fail "Extracting does not work"
+      require (z == 10 && y) "Extracting does not work"
     strengthenTest = do
       let x :: Prod '[Int, Bool, Float] = produce (\f -> f 10 True 0.1)
           y :: Prod '[Bool, Int, Float] = strengthen x
           z :: Prod '[Bool, Int] = strengthen x
-      unless (y == produce (\f -> f True 10 0.1)) $ fail "strengthen doesn't work 1"
-      unless (z == produce (\f -> f True 10)) $ fail "strengthen doesn't work 2"
+      requires
+        [ (y == produce (\f -> f True 10 0.1), "strengthen doesn't work 1")
+        , (z == produce (\f -> f True 10), "strengthen doesn't work 2")
+        ]
     initNTest = do
       let x :: Prod '[Int, Bool, Char, Float] = produce (\f -> f 10 True 'a' 0.2)
-      unless (initN @0 x == produce id) $ fail "tailN does not work 0"
-      unless (initN @1 x == produce (\f -> f 10)) $ fail "tailN does not work 1"
-      unless (initN @2 x == produce (\f -> f 10 True)) $ fail "tailN does not work 2"
-      unless (initN @3 x == produce (\f -> f 10 True 'a')) $ fail "tailN does not work 3"
-      unless (initN @4 x == produce (\f -> f 10 True 'a' 0.2)) $ fail "tailN does not work 4"
+      requires
+        [ (initN @0 x == produce id, "tailN does not work 0")
+        , (initN @1 x == produce (\f -> f 10), "tailN does not work 1")
+        , (initN @2 x == produce (\f -> f 10 True), "tailN does not work 2")
+        , (initN @3 x == produce (\f -> f 10 True 'a'), "tailN does not work 3")
+        , (initN @4 x == produce (\f -> f 10 True 'a' 0.2), "tailN does not work 4")
+        ]
     tailNTest = do
       let x :: Prod '[Int, Bool, Char, Float] = produce (\f -> f 10 True 'a' 0.2)
-      unless (tailN @0 x == x) $ fail "tailN does not work 0"
-      unless (tailN @1 x == produce (\f -> f True 'a' 0.2)) $ fail "tailN does not work 1"
-      unless (tailN @2 x == produce (\f -> f 'a' 0.2)) $ fail "tailN does not work 2"
-      unless (tailN @3 x == produce (\f -> f 0.2)) $ fail "tailN does not work 3"
-      unless (tailN @4 x == produce id) $ fail "tailN does not work 3"
+      requires
+        [ (tailN @0 x == x, "tailN does not work 0")
+        , (tailN @1 x == produce (\f -> f True 'a' 0.2), "tailN does not work 1")
+        , (tailN @2 x == produce (\f -> f 'a' 0.2), "tailN does not work 2")
+        , (tailN @3 x == produce (\f -> f 0.2), "tailN does not work 3")
+        , (tailN @4 x == produce id, "tailN does not work 3")
+        ]
+    selectTest = do
+      let x :: Prod '[Int, Bool, Char, Float] = produce (\f -> f 10 True 'a' 0.2)
+      requires
+        [ (select x (\(n :: Int) -> n == 10), "select does not work 0")
+        , (select x (\(f :: Float) -> f == 0.2), "select does not work 1")
+        , (select x (\(b :: Bool) (f :: Float) -> b && f == 0.2), "select does not work 2")
+        ]
+    prodBuilderTest = do
+      requires
+        [ (empty == buildProd emptyB, "prodBuilder does not work 0")
+        , (produce (\f -> f "Hello") == buildProd (consB "Hello" emptyB), "prodBuilder does not work 1")
+        ]
+    toListTest = do
+      let x :: Prod '[String, Bool] = produce \f -> f "Hello" True
+      requires
+        [ (toList @Show show x == [show "Hello", show True], "toList does not work 0")
+        , (toList @Eq (\a -> a == a) x == [True, True], "toList does not work 1")
+        ]
 
 sumTest :: IO ()
 sumTest = catchAndDisplay
@@ -83,7 +118,7 @@
     tagTest = do
       let tag' = tag @Int @'[Bool, Int]
           tag'' = tag @Bool @'[Bool, Int]
-      unless (tag' == 1) $ fail ("Tag " <> show tag' <> " does not equal 1")
+      require (tag' == 1) ("Tag " <> show tag' <> " does not equal 1")
     eqTest = do
       let x :: Sum '[Int, Bool] = Inj (10 :: Int)
           y :: Sum '[Int, Bool] = Inj True
@@ -92,44 +127,57 @@
           a :: Sum '[Int, Bool] = Inj (10 :: Int)
           b :: Sum '[Int, Bool] = Inj False
           c :: Sum '[Int, Bool] = Inj True
-      unless (x /= y) $ fail "10 equals True"
-      unless (x /= z) $ fail "10 equals 11"
-      unless (x == a) $ fail "10 does not equal 10"
-      unless (y /= b) $ fail "True equals False"
-      unless (y == c) $ fail "True does not equal True"
+      requires
+        [ (x /= y, "10 equals True")
+        , (x /= z, "10 equals 11")
+        , (x == a, "10 does not equal 10")
+        , (y /= b, "True equals False")
+        , (y == c, "True does not equal True")
+        ]
     noOpWeakenTest = do
       let x :: Sum '[Int, Bool]  = Inj (10 :: Int)
           y :: Sum '[Int, Bool, Integer] = noOpWeaken x
-      unless (y == Inj (10 :: Int)) $ fail "y does not equal Inj 10"
+      require (y == Inj (10 :: Int)) "y does not equal Inj 10"
       pure ()
     weakenTest = do
       let x :: Sum '[Int, Bool] = Inj (10 :: Int)
           y :: Sum '[Bool, Int] = weaken x
           z :: Sum '[Integer, Bool, Float, Int] = weaken y
-      unless (y == Inj (10 :: Int)) $ fail "y does not equal Inj 10"
-      unless (z == Inj (10 :: Int)) $ fail "y does not equal Inj 10"
+      requires
+        [ (y == Inj (10 :: Int), "y does not equal Inj 10")
+        , (z == Inj (10 :: Int), "y does not equal Inj 10")
+        ]
     matchTest = do
       let x :: Sum '[Int, Bool] = Inj (10 :: Int)
-      unless (match x (== 10) id) $ fail "x does not match 10"
+      require (match x (== 10) id) "x does not match 10"
     considerTest = do
       let x :: Sum '[Int, Bool] = Inj (10 :: Int)
           y :: Sum '[Int, Bool] = Inj True
-      unless (consider @Int x == Right 10) $ fail "x at Int is not considered to be 10"
-      unless (consider @Int y == Left (Inj True)) $ fail $ "x is not considered to be Left (Inj True)"
-      unless (consider @Bool y == Right True) $ fail "x at Bool is not considered to be Right True"
+      requires
+        [ (consider @Int x == Right 10, "x at Int is not considered to be 10"),
+          (consider @Int y == Left (Inj True), "x is not considered to be Left (Inj True)"),
+          (consider @Bool y == Right True, "x at Bool is not considered to be Right True")
+        ]
     inmapTest = do
       let x :: Sum '[Int, Bool] = Inj (10 :: Int)
           y :: Sum '[Int, Bool] = inmap (== (10 :: Int)) x
           z :: Sum '[Int, Bool] = inmap (== True) x
-      unless (y == Inj True) $ fail "x did not get mapped to True"
-      unless (z == Inj (10 :: Int)) $ fail "x did not get left alone"
+      requires
+        [ (y == Inj True, "x did not get mapped to True")
+        , (z == Inj (10 :: Int), "x did not get left alone")
+        ]
     smapTest = do
       let x :: Sum '[Int, Bool] = Inj (10 :: Int)
           y :: Sum '[Bool, Int] = smap (== (10 :: Int)) x
           z :: Sum '[Bool, Int] = smap (== True) x
-      unless (y == Inj True) $ fail "x did not get mapped to True"
-      unless (z == Inj (10 :: Int)) $ fail "x did not get left alone"
+      requires
+        [ (y == Inj True, "x did not get mapped to True")
+        , (z == Inj (10 :: Int), "x did not get left alone")
+        ]
     unmatchTest = do
       let x :: Sum '[Int, Bool] = Inj True
           y = \f g -> f 100
-      unless (x == unmatch (match x)) $ fail "match and unmatch are not an inverse pair"
+      require (x == unmatch (match x)) "match and unmatch are not an inverse pair"
+    applyTest = do
+      let x :: Sum '[Int, Bool] = Inj False
+      require (apply @Show show x == "False") "apply does not work 0"