diff --git a/src/TypeUnary/Nat.hs b/src/TypeUnary/Nat.hs
--- a/src/TypeUnary/Nat.hs
+++ b/src/TypeUnary/Nat.hs
@@ -4,7 +4,7 @@
 ----------------------------------------------------------------------
 -- |
 -- Module      :  TypeUnary.Nat
--- Copyright   :  (c) Conal Elliott 2009
+-- Copyright   :  (c) Conal Elliott 2009-2012
 -- License     :  BSD3
 -- 
 -- Maintainer  :  conal@conal.net
@@ -19,7 +19,7 @@
   -- * Value-typed natural numbers
   , Nat(..), zero, one, two, three, four
   , withIsNat, natSucc, natIsNat
-  , natToZ, natEq, natAdd
+  , natToZ, natEq, natAdd, natMul
   , IsNat(..)
   -- * Inequality proofs and indices
   , (:<:)(..), Index(..), succI, index0, index1, index2, index3
@@ -42,7 +42,8 @@
   Zero :: Nat Z
   Succ :: IsNat n => Nat n -> Nat (S n)
 
-instance Show (Nat n) where show = show . natToZ
+instance Show (Nat n) where
+  show n = show (natToZ n :: Integer)
 
 withIsNat :: (IsNat n => Nat n -> a) -> (Nat n -> a)
 withIsNat p Zero     = p Zero
@@ -72,8 +73,8 @@
                    NatIsNat n' Refl -> p n'
 -}
 
--- | Interpret a 'Nat' as an 'Integer'
-natToZ :: Nat n -> Integer
+-- | Interpret a 'Nat' as a plain number
+natToZ :: (Enum a, Num a) => Nat n -> a
 natToZ Zero     = 0
 natToZ (Succ n) = (succ . natToZ) n
 
@@ -88,6 +89,11 @@
 Zero   `natAdd` n = n
 Succ m `natAdd` n = natSucc (m `natAdd` n)
 
+-- | Product of naturals
+natMul :: forall m n. Nat m -> Nat n -> Nat (m :*: n)
+Zero   `natMul` _ = Zero
+Succ m `natMul` n = n `natAdd` (m `natMul` n)
+
 zero :: Nat N0
 zero = Zero
 
@@ -103,6 +109,9 @@
 four :: Nat N4
 four = Succ three
 
+-- TODO: Consider whether we really want definitions like natAdd, natMul,
+-- and zero, ..., four, considering that all of them can be synthesized
+-- from IsNat.
 
 infix 4 :<:
 
diff --git a/src/TypeUnary/TyNat.hs b/src/TypeUnary/TyNat.hs
--- a/src/TypeUnary/TyNat.hs
+++ b/src/TypeUnary/TyNat.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE TypeFamilies, TypeOperators, EmptyDataDecls #-}
+{-# LANGUAGE UndecidableInstances #-} -- for :*:
 {-# OPTIONS_GHC -Wall #-}
 ----------------------------------------------------------------------
 -- |
@@ -15,7 +16,7 @@
 module TypeUnary.TyNat
   (
     -- * Type-level natural numbers
-    Z, S, (:+:)
+    Z, S, (:+:), (:*:)
   , N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16
   ) where
 
@@ -36,6 +37,15 @@
 type instance Z   :+: b = b
 type instance S a :+: b = S (a :+: b)
 
+infixl 7 :*:
+
+-- | Product of type-level numbers
+type family a :*: b
+
+type instance Z   :*: b = Z
+type instance S a :*: b = b :+: (a :*: b)
+
+
 -- Generated code
 -- 
 --   putStrLn $ unlines ["type N" ++ show (n+1) ++ " = S N" ++ show n | n <- [0..15]]
@@ -57,3 +67,4 @@
 type N14 = S N13
 type N15 = S N14
 type N16 = S N15
+
diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -32,10 +32,12 @@
   , update
   , set, set0, set1, set2, set3
   , getI, setI
-  , swizzle, split, deleteV, elemsV
+  , flattenV, swizzle, split, deleteV, elemsV, unzipV
   , ToVec(..)
   ) where
 
+  -- TODO: Consider dropping "V" suffix from several of the names.
+
 import Prelude hiding (foldr,sum)
 
 -- #include "Typeable.h"
@@ -192,7 +194,7 @@
 -- And why Vec1 for Scalar?
 
 instance (IsNat n, Storable a) => Storable (Vec n a) where
-   sizeOf    = const (fromIntegral (natToZ (nat :: Nat n))
+   sizeOf    = const ((natToZ (nat :: Nat n))
                       * sizeOf (undefined :: a))
    alignment = const (alignment (undefined :: a))
    peek      = peekV . castPtr
@@ -366,7 +368,19 @@
 setI :: (IsNat n, Show i, Integral i) => i -> a -> Vec n a -> Vec n a
 setI = set . coerceToIndex
 
+{--------------------------------------------------------------------
+    Misc
+--------------------------------------------------------------------}
 
+-- | Flatten a vector of vectors (a 2D array) into a vector
+flattenV :: IsNat n => Vec n (Vec m a) -> Vec (n :*: m) a
+flattenV = flattenV' nat
+
+flattenV' :: Nat n -> Vec n (Vec m a) -> Vec (n :*: m) a
+flattenV' Zero _               = ZVec
+flattenV' (Succ n') (v :< vs') = v <+> flattenV' n' vs'
+flattenV' _ _ = error "flattenV': GHC doesn't know this case can't happen."
+
 -- | Swizzling.  Extract multiple elements simultaneously.
 swizzle :: Vec n (Index m) -> Vec m a -> Vec n a
 swizzle ZVec        _ = ZVec
@@ -455,6 +469,10 @@
 t3 = swizzle t2 t1
 -}
 
+-- | Unzip a list of pairs into a pair of lists
+unzipV :: Vec n (a,b) -> (Vec n a, Vec n b)
+unzipV ZVec = (ZVec,ZVec)
+unzipV ((a,b) :< ps) = (a :< as, b :< bs) where (as,bs) = unzipV ps
 
 {--------------------------------------------------------------------
     Conversion to vectors
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.1.16
+Version:             0.1.18
 Cabal-Version:       >= 1.2
 Synopsis:            
   Type-level and typed unary natural numbers, inequality proofs, vectors
@@ -11,7 +11,7 @@
 Author:              Conal Elliott
 Maintainer:          conal@conal.net
 Homepage:            https://github.com/conal/type-unary
-Copyright:           (c) 2009-2011 by Conal Elliott
+Copyright:           (c) 2009-2012 by Conal Elliott
 License:             BSD3
 License-File:        COPYING
 Stability:           experimental