diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -35,7 +35,7 @@
   , vec1, vec2, vec3, vec4
   , un1, un2, un3, un4
   , get0, get1, get2, get3
-  , get, swizzle
+  , get, swizzle, split
   ) where
 
 import Prelude hiding (foldr,sum)
@@ -43,7 +43,7 @@
 -- #include "Typeable.h"
 
 import Control.Applicative (Applicative(..),liftA2,(<$>))
-import Data.Foldable (Foldable(..),sum)
+import Data.Foldable (Foldable(..),toList,sum)
 import Data.Traversable (Traversable(..))
 import Data.Maybe (isJust)
 -- import Data.Typeable
@@ -240,32 +240,77 @@
 
 -}
 
+{--------------------------------------------------------------------
+    Instances for standard classes
+--------------------------------------------------------------------}
+
+instance Eq a => Eq (Vec n a) where
+  ZVec    == ZVec    = True
+  a :< as == b :< bs = a==b && as==bs
+
+instance Ord a => Ord (Vec n a) where
+  ZVec      `compare` ZVec      = EQ
+  (a :< as) `compare` (b :< bs) =
+    case a `compare` b of
+      LT -> LT
+      GT -> GT
+      EQ -> as `compare` bs
+
+instance Show a => Show (Vec n a) where
+  show v = "elemsV " ++ show (toList v)
+
 instance Functor (Vec n) where
   fmap _ ZVec     = ZVec
   fmap f (a :< u) = f a :< fmap f u
 
+instance IsNat n => Applicative (Vec n) where
+  pure  = pureV
+  (<*>) = applyV
 
--- | @n@ a vector length.
-class {- Typeable n => -} IsNat n where
-  nat    :: Nat n
-  pureV  :: a   -> Vec n a
-  elemsV :: [a] -> Vec n a
-  peekV  :: Storable a => Ptr a -> IO (Vec n a)
-  pokeV  :: Storable a => Ptr a -> Vec n a -> IO ()
+applyV :: Vec n (a -> b) -> Vec n a -> Vec n b
+ZVec      `applyV` ZVec      = ZVec
+(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)
 
-{-
--- TODO: remove all but nat from the class. Define the rest outside of the
--- class by using nat. Then break this module into Nat and Vec. For instance,
+-- Without -fno-warn-incomplete-patterns above,
+-- the previous two instances lead to warnings about non-exhaustive
+-- pattern matches, although the other possibilities
+-- are type-incorrect.  According to SLPJ:
+-- 
+--   The overlap warning checker simply doesn't take account of GADTs.
+--   There's a long-standing project suggestion to fix this:
+--   http://hackage.haskell.org/trac/ghc/wiki/ProjectSuggestions .
+--   Perhaps a good GSoc project.
 
-pureV :: IsNat n => a -> Vec n a
-pureV = pureN nat
+instance Foldable (Vec n) where
+  foldr _  b ZVec     = b
+  foldr h b (a :< as) = a `h` foldr h b as
 
-pureN :: Nat n -> a -> Vec n a
-pureN Zero     _ = ZVec
-pureN (Succ n) a = a :< pureN n a
--}
+instance Traversable (Vec n) where
+  traverse _ ZVec      = pure ZVec
+  traverse f (a :< as) = liftA2 (:<) (f a) (traverse f as)
 
+instance (IsNat n, Num a) => AdditiveGroup (Vec n a) where
+  { zeroV = pure 0; (^+^) = liftA2 (+) ; negateV = fmap negate }
 
+instance (IsNat n, Num a) => VectorSpace (Vec n a) where
+  type Scalar (Vec n a) = Vec1 a
+  (*^) (s :< ZVec) = fmap (s *)
+
+instance (IsNat n, Num a) => InnerSpace (Vec n a) where
+   -- u <.> v = vec1 (sum (liftA2 (*) u v))
+   (<.>) = (result.result) (vec1 . sum) (liftA2 (*))
+
+instance (IsNat n, Storable a) => Storable (Vec n a) where
+   sizeOf    = const (fromIntegral (natToZ (nat :: Nat n))
+                      * sizeOf (undefined :: a))
+   alignment = const (alignment (undefined :: a))
+   peek      = peekV . castPtr
+   poke      = pokeV . castPtr
+
+{--------------------------------------------------------------------
+    IsNat
+--------------------------------------------------------------------}
+
 instance IsNat Z where
   nat          = Zero
   pureV _      = ZVec
@@ -292,36 +337,9 @@
 -- succPtr :: forall a. Storable a => Ptr a -> Ptr a
 -- succPtr p = p `plusPtr` sizeOf (undefined :: a)
 
-
 -- TODO: Optimize peekV, pokeV.  For instance, unroll the loop in the
 -- dictionary, remove the sizeOf dependence on @a@.
 
-applyV :: Vec n (a -> b) -> Vec n a -> Vec n b
-ZVec      `applyV` ZVec      = ZVec
-(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)
-
-instance IsNat n => Applicative (Vec n) where
-  pure  = pureV
-  (<*>) = applyV
-
--- Without -fno-warn-incomplete-patterns above,
--- the previous two instances lead to warnings about non-exhaustive
--- pattern matches, although the other possibilities
--- are type-incorrect.  According to SLPJ:
--- 
---   The overlap warning checker simply doesn't take account of GADTs.
---   There's a long-standing project suggestion to fix this:
---   http://hackage.haskell.org/trac/ghc/wiki/ProjectSuggestions .
---   Perhaps a good GSoc project.
-
-instance Foldable (Vec n) where
-  foldr _  b ZVec     = b
-  foldr h b (a :< as) = a `h` foldr h b as
-
-instance Traversable (Vec n) where
-  traverse _ ZVec      = pure ZVec
-  traverse f (a :< as) = liftA2 (:<) (f a) (traverse f as)
-
 infixl 1 <+>
 -- | Concatenation of vectors
 (<+>) :: Vec m a -> Vec n a -> Vec (m :+: n) a
@@ -336,6 +354,28 @@
 -- TODO: Try reimplementing many Vec functions via foldr.  Warning: some
 -- (most?) will fail because they rely on a polymorphic combining function.
 
+-- | @n@ a vector length.
+class {- Typeable n => -} IsNat n where
+  nat    :: Nat n
+  pureV  :: a   -> Vec n a
+  elemsV :: [a] -> Vec n a
+  peekV  :: Storable a => Ptr a -> IO (Vec n a)
+  pokeV  :: Storable a => Ptr a -> Vec n a -> IO ()
+
+-- Convert from vector to list via Data.Foldable.toList
+
+{-
+-- TODO: remove all but nat from the class. Define the rest outside of the
+-- class by using nat. Then break this module into Nat and Vec. For instance,
+
+pureV :: IsNat n => a -> Vec n a
+pureV = pureN nat
+
+pureN :: Nat n -> a -> Vec n a
+pureN Zero     _ = ZVec
+pureN (Succ n) a = a :< pureN n a
+-}
+
 -- Convenient nicknames
 
 type Vec0  = Vec N0
@@ -386,24 +426,7 @@
 un4 :: Vec4 a -> (a,a,a,a)
 un4 (a :< b :< c :< d :< ZVec) = (a,b,c,d)
 
-
 {--------------------------------------------------------------------
-    Vector space instances
---------------------------------------------------------------------}
-
-instance (IsNat n, Num a) => AdditiveGroup (Vec n a) where
-  { zeroV = pure 0; (^+^) = liftA2 (+) ; negateV = fmap negate }
-
-instance (IsNat n, Num a) => VectorSpace (Vec n a) where
-  type Scalar (Vec n a) = Vec1 a
-  (*^) (s :< ZVec) = fmap (s *)
-
-instance (IsNat n, Num a) => InnerSpace (Vec n a) where
-   -- u <.> v = vec1 (sum (liftA2 (*) u v))
-   (<.>) = (result.result) (vec1 . sum) (liftA2 (*))
-
-
-{--------------------------------------------------------------------
     Extract elements
 --------------------------------------------------------------------}
 
@@ -443,32 +466,33 @@
 t3 = swizzle t2 t1
 -}
 
-
-
-{--------------------------------------------------------------------
-    Some instances.  More in Type.hs
---------------------------------------------------------------------}
-
-instance Eq a => Eq (Vec n a) where
-  ZVec    == ZVec    = True
-  a :< as == b :< bs = a==b && as==bs
-
-instance Ord a => Ord (Vec n a) where
-  ZVec      `compare` ZVec      = EQ
-  (a :< as) `compare` (b :< bs) =
-    case a `compare` b of
-      LT -> LT
-      GT -> GT
-      EQ -> as `compare` bs
+-- | Split a vector
+split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a)
+split = split' nat
 
+split' :: Nat n -> Vec (n :+: m) a -> (Vec n a, Vec m a)
+split' Zero v             = (ZVec, v)
+split' (Succ n) (a :< as) = (a :< bs, cs)
+ where
+   (bs,cs) = split' n as
 
-{--------------------------------------------------------------------
-    Storage
---------------------------------------------------------------------}
+-- For instance,
+-- 
+--   *TypeUnary.Vec> split (pure 3) :: (Vec7 Int, Vec4 Int)
+--   (elemsV [3,3,3,3,3,3,3],elemsV [3,3,3,3])
+-- 
+-- Note that 'pure 3' was inferred to have type 'Vec11 Int'.
 
-instance (IsNat n, Storable a) => Storable (Vec n a) where
-   sizeOf    = const (fromIntegral (natToZ (nat :: Nat n))
-                      * sizeOf (undefined :: a))
-   alignment = const (alignment (undefined :: a))
-   peek      = peekV . castPtr
-   poke      = pokeV . castPtr
+-- I'd like to define take & drop similarly, e.g.,
+--
+--   take :: IsNat n => Vec (n :+: m) a -> Vec n a
+--   take = fst . split
+-- 
+-- However,
+-- 
+--   Could not deduce ((n :+: m0) ~ (n :+: m))
+--   from the context (IsNat n)
+--     bound by the type signature for
+--                TypeUnary.Vec.take :: IsNat n => Vec (n :+: m) a -> Vec n a
+--     at /Users/conal/Haskell/type-unary/src/TypeUnary/Vec.hs:488:1-18
+--   NB: `:+:' is a type function, and may not be injective
diff --git a/type-unary.cabal b/type-unary.cabal
--- a/type-unary.cabal
+++ b/type-unary.cabal
@@ -1,5 +1,5 @@
 Name:                type-unary
-Version:             0.0.0
+Version:             0.1.0
 Cabal-Version:       >= 1.2
 Synopsis:            Type-level and typed unary natural numbers, vectors, inequality proofs
 Category:            Data