diff --git a/hvect.cabal b/hvect.cabal
--- a/hvect.cabal
+++ b/hvect.cabal
@@ -1,6 +1,6 @@
 name:                hvect
-version:             0.1.0.0
-synopsis:            Simple heterogeneous lists
+version:             0.2.0.0
+synopsis:            Simple strict heterogeneous lists
 description:         Small, concise and simple implementation of heterogeneous lists with useful utility functions
 homepage:            https://github.com/agrafix/hvect
 bug-reports:         https://github.com/agrafix/hvect/issues
diff --git a/src/Data/HVect.hs b/src/Data/HVect.hs
--- a/src/Data/HVect.hs
+++ b/src/Data/HVect.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE UndecidableInstances #-} -- for ReverseLoop type family
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE GADTs #-}
@@ -9,9 +9,12 @@
 {-# LANGUAGE FlexibleInstances #-}
 
 module Data.HVect
-  ( HVect (..)
-  , empty, null, head
+  ( -- * typesafe strict vector
+    HVect (..)
+  , empty, null, head, tail
   , singleton
+  , length, HVectLen (..)
+  , (!!), HVectIdx (..)
   , HVectElim
   , Append, (<++>)
   , ReverseLoop, Reverse, reverse
@@ -19,14 +22,18 @@
   , Rep (..), HasRep (..)
   , curryExpl, curry
   , packExpl, pack
+    -- * type level numeric utilities
+  , Nat (..), SNat (..), sNatToInt
+  , intToSNat, AnySNat (..)
+  , (:<)
   ) where
 
-import Prelude hiding (reverse, uncurry, curry, head, null)
+import Prelude hiding (reverse, uncurry, curry, head, null, (!!), length, tail)
 
 -- | Heterogeneous vector
 data HVect (ts :: [*]) where
   HNil :: HVect '[]
-  (:&:) :: t -> HVect ts -> HVect (t ': ts)
+  (:&:) :: !t -> !(HVect ts) -> HVect (t ': ts)
 
 instance Eq (HVect '[]) where
     _ == _ =
@@ -82,8 +89,59 @@
 head :: HVect (t ': ts) -> t
 head (a :&: as) = a
 
+tail :: HVect (t ': ts) -> HVect ts
+tail (a :&: as) = as
+
+length :: HVect as -> SNat (HVectLen as)
+length HNil = SZero
+length (a :&: as) = SSucc (length as)
+
+sNatToInt :: SNat n -> Int
+sNatToInt SZero = 0
+sNatToInt (SSucc n) = 1 + (sNatToInt n)
+
+intToSNat :: Int -> AnySNat
+intToSNat 0 = AnySNat SZero
+intToSNat n =
+    case intToSNat (n - 1) of
+      AnySNat n -> AnySNat (SSucc n)
+
+data Nat where
+    Zero :: Nat
+    Succ :: Nat -> Nat
+
+data SNat (n :: Nat) where
+    SZero :: SNat Zero
+    SSucc :: SNat n -> SNat (Succ n)
+
+data AnySNat where
+    AnySNat :: forall n. SNat n -> AnySNat
+
+type family HVectLen (ts :: [*]) :: Nat
+type instance HVectLen '[] = Zero
+type instance HVectLen (t ': ts) = Succ (HVectLen ts)
+
+type family HVectIdx (n :: Nat) (ts :: [*]) :: *
+type instance HVectIdx Zero (a ': as) = a
+type instance HVectIdx (Succ n) (a ': as) = HVectIdx n as
+type instance HVectIdx a '[] = ()
+
+type family (m :: Nat) :< (n :: Nat) :: Bool
+type instance m :< Zero = False
+type instance Zero :< (Succ n) = True
+type instance (Succ m) :< (Succ n) = m :< n
+
+type family (m :: Nat) :- (n :: Nat) :: Nat
+type instance n :- Zero = n
+type instance (Succ m) :- (Succ n) = m :- n
+
+(!!) :: ((n :< HVectLen as) ~ True) => SNat n -> HVect as -> HVectIdx n as
+SZero !! (a :&: as) = a
+(SSucc s) !! (a :&: as) = s !! as
+
 infixr 5 :&:
 infixr 5 <++>
+infixl 9 !!
 
 (<++>) :: HVect as -> HVect bs -> HVect (Append as bs)
 (<++>) HNil bs = bs
diff --git a/test/Data/HVectTest.hs b/test/Data/HVectTest.hs
--- a/test/Data/HVectTest.hs
+++ b/test/Data/HVectTest.hs
@@ -35,6 +35,11 @@
     do assertEqual 1 (HV.head $ 1 :&: empty)
        assertEqual 1 (HV.head $ 1 :&: 2 :&: empty)
 
+test_tail :: IO ()
+test_tail =
+    do assertEqual empty (HV.tail $ 1 :&: empty)
+       assertEqual (2 :&: empty) (HV.tail $ 1 :&: 2 :&: empty)
+
 test_null :: IO ()
 test_null =
     do assertBool (HV.null empty)
@@ -45,12 +50,25 @@
     do assertEqual (1 :&: 2 :&: "foo" :&: "bar" :&: empty) ((1 :&: 2 :&: empty) <++> ("foo" :&: "bar" :&: empty))
        assertEqual (1 :&: 2 :&: empty) ((1 :&: 2 :&: empty) <++> empty)
 
+
 test_curryUncurry :: IO ()
 test_curryUncurry =
     do assertEqual "12" (fun (1 :&: 2 :&: empty))
        assertEqual "12" (HV.curry fun 1 2)
        assertEqual "12" (HV.uncurry (HV.curry fun) (1 :&: 2 :&: empty))
     where
-      fun :: HVect '[Int, Int] -> String
+      fun :: HVect [Int, Int] -> String
       fun (a :&: b  :&: HNil) = show a ++ show b
       fun _ = "OOPS!"
+
+test_length :: IO ()
+test_length =
+    do assertEqual 0 (sNatToInt $ HV.length empty)
+       assertEqual 2 (sNatToInt $ HV.length ("foo" :&: "bar" :&: empty))
+       assertEqual 5 (sNatToInt $ HV.length ("aaa" :&: False :&: True :&: "foo" :&: "bar" :&: empty))
+
+test_idxAccess :: IO ()
+test_idxAccess =
+    do assertEqual "foo" (SZero HV.!! ("foo" :&: "bar" :&: empty))
+       assertEqual "bar" (SSucc SZero HV.!! ("foo" :&: "bar" :&: empty))
+       assertEqual "bar" (SSucc (SSucc SZero) HV.!! (True :&: "foo" :&: "bar" :&: empty))