diff --git a/Data/List/Indexed.hs b/Data/List/Indexed.hs
new file mode 100644
--- /dev/null
+++ b/Data/List/Indexed.hs
@@ -0,0 +1,36 @@
+{- |
+Module      :  Data.List.Indexed
+Description :  A library providing length-indexed and element-indexed lists which sit somewhere between homogeneous and fully heterogeneous lists.
+Copyright   :  Copyright (c) 2014 Kenneth Foner
+
+Maintainer  :  kenneth.foner@gmail.com
+Stability   :  experimental
+Portability :  non-portable
+
+This module re-exports the 'ConicList' and 'CountedList' types and functions to work with them.
+-}
+
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE GADTs      #-}
+{-# LANGUAGE PolyKinds  #-}
+
+module Data.List.Indexed
+   ( heterogenize , homogenize
+   , module Data.List.Indexed.Counted
+   , module Data.List.Indexed.Conic
+   ) where
+
+import Data.List.Indexed.Counted
+import Data.List.Indexed.Conic
+
+-- We can convert between them using cones and co-cones
+
+-- | Turn a 'CountedList' into a 'ConicList' by means of a function from some @a@ to an @(f t)@.
+heterogenize :: (a -> f t) -> CountedList n a -> ConicList f (Replicate n t)
+heterogenize _ CountedNil = ConicNil
+heterogenize f (x ::: xs) = f x :-: heterogenize f xs
+
+-- | Given a function to collapse any @(f t)@ into an @a@, turn a 'ConicList' into a 'CountedList'.
+homogenize :: (forall t. f t -> a) -> ConicList f ts -> CountedList (Length ts) a
+homogenize _ ConicNil   = CountedNil
+homogenize f (x :-: xs) = f x ::: homogenize f xs
diff --git a/Data/List/Indexed/Conic.hs b/Data/List/Indexed/Conic.hs
new file mode 100644
--- /dev/null
+++ b/Data/List/Indexed/Conic.hs
@@ -0,0 +1,54 @@
+{- |
+Module      :  Data.List.Indexed.Conic
+Description :  A library providing length-indexed and element-indexed lists which sit somewhere between homogeneous and fully heterogeneous lists.
+Copyright   :  Copyright (c) 2014 Kenneth Foner
+
+Maintainer  :  kenneth.foner@gmail.com
+Stability   :  experimental
+Portability :  non-portable
+
+This module implements conic lists, which are lists where every element is of type @(f a)@ for /some/ @a@, but the @a@ 
+index may vary. This sits between homogeneous and fully heterogeneous lists in terms of expressivity and also the ease
+to manipulate.
+-}
+
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-} 
+
+module Data.List.Indexed.Conic where
+
+import Data.Numeric.Witness.Peano
+
+infixr 5 :-:
+data x :-: y
+data Nil
+
+-- | Conic lists are lists where each element is an (f a) for some a, but the a may be different for each element. Types of elements are kept track of in the type of the list.
+data ConicList f ts where
+   (:-:) :: f a -> ConicList f rest -> ConicList f (a :-: rest)
+   ConicNil  :: ConicList f Nil
+
+type family Replicate n x where
+   Replicate Zero     x = Nil
+   Replicate (Succ n) x = x :-: Replicate n x
+
+type family Length ts where
+   Length Nil        = Zero
+   Length (x :-: xs) = Succ (Length xs)
+
+type family Tack x xs where
+   Tack a Nil        = a :-: Nil
+   Tack a (x :-: xs) = x :-: Tack a xs
+
+tack :: f t -> ConicList f ts -> ConicList f (Tack t ts)
+tack a ConicNil   = a :-: ConicNil
+tack a (x :-: xs) = x :-: tack a xs
diff --git a/Data/List/Indexed/Counted.hs b/Data/List/Indexed/Counted.hs
new file mode 100644
--- /dev/null
+++ b/Data/List/Indexed/Counted.hs
@@ -0,0 +1,90 @@
+{- |
+Module      :  Data.List.Indexed.Counted
+Description :  A library providing length-indexed and element-indexed lists which sit somewhere between homogeneous and fully heterogeneous lists.
+Copyright   :  Copyright (c) 2014 Kenneth Foner
+
+Maintainer  :  kenneth.foner@gmail.com
+Stability   :  experimental
+Portability :  non-portable
+
+This module implements homogeneous counted lists, which are type-indexed by length.
+-}
+
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-} 
+
+module Data.List.Indexed.Counted where
+
+import Data.Numeric.Witness.Peano
+
+import Control.Applicative
+import Data.List hiding ( replicate , zip )
+import Prelude   hiding ( replicate , zip )
+
+infixr 5 :::
+
+-- | Counted lists are indexed by length in the type.
+data CountedList n a where
+   (:::) :: a -> CountedList n a -> CountedList (Succ n) a
+   CountedNil :: CountedList Zero a
+
+instance (Show x) => Show (CountedList n x) where
+   showsPrec p xs = showParen (p > 10) $
+      (showString $ ( intercalate " ::: "
+                    $ map show
+                    $ unCount xs ) ++ " ::: CountedNil")
+
+-- | The 'count' of a list is the natural number corresponding to its length.
+count :: CountedList n a -> Natural n
+count CountedNil = Zero
+count (x ::: xs) = Succ (count xs)
+
+-- | Convert a counted list to a regular Haskell list.
+unCount :: CountedList n a -> [a]
+unCount CountedNil       = []
+unCount (x ::: xs) = x : unCount xs
+
+-- | Replicate some element a certain number of times.
+replicate :: Natural n -> x -> CountedList n x
+replicate Zero     _ = CountedNil
+replicate (Succ n) x = x ::: replicate n x
+
+-- | Appending two counted lists yields one of length equal to the sum of the lengths of the two initial lists.
+append :: CountedList n a -> CountedList m a -> CountedList (m + n) a
+append CountedNil       ys = ys
+append (x ::: xs) ys = x ::: append xs ys
+
+-- | Take the nth element of a list. We statically prevent taking the nth element of a list of length less than n.
+nth :: (n < m) => Natural n -> CountedList m a -> a
+nth Zero     (a ::: _)  = a
+nth (Succ n) (_ ::: as) = nth n as
+nth _ _ = error "nth: the impossible occurred" -- like in minus, GHC can't prove this is unreachable
+
+-- | Pad the length of a list to a given length. If the number specified is less than the length of the list given,
+--   it won't pass the type-checker.
+padTo :: (m <= n) => Natural n -> x -> CountedList m x -> CountedList ((n - m) + m) x
+padTo n x list =
+   list `append` replicate (n `minus` count list) x
+
+-- | Zip two equal-length lists together.
+zip :: CountedList n a -> CountedList n b -> CountedList n (a,b)
+zip (a ::: as) (b ::: bs) = (a,b) ::: zip as bs
+zip CountedNil _ = CountedNil
+zip _ CountedNil = CountedNil
+
+instance Functor (CountedList n) where
+   fmap f CountedNil = CountedNil
+   fmap f (a ::: as) = f a ::: fmap f as
+
+instance (ReifyNatural n) => Applicative (CountedList n) where
+   pure x    = replicate (reifyNatural :: Natural n) x
+   fs <*> xs = uncurry id <$> zip fs xs
diff --git a/IndexedList.cabal b/IndexedList.cabal
new file mode 100644
--- /dev/null
+++ b/IndexedList.cabal
@@ -0,0 +1,25 @@
+-- Initial IndexedList.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                IndexedList
+version:             0.1.0.0
+synopsis:            Length-indexed and element-indexed lists which sit somewhere between homogeneous and fully heterogeneous lists.
+description:         This library implements /counted lists/ linked to type-level naturals indexing length, compatible with the Peano natural numbers found in "Data.Numeric.Witness.Peano", as well as so-called /conic lists/, which are linked to a type index listing the type indices of partially-heterogeneous values contained within.
+license:             BSD3
+license-file:        LICENSE
+author:              Kenneth Foner
+maintainer:          kenneth.foner@gmail.com
+copyright:           Copyright (c) 2014 Kenneth Foner
+homepage:            https://github.com/kwf/IndexedList
+category:            Data
+build-type:          Simple
+-- extra-source-files:  
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Data.List.Indexed, Data.List.Indexed.Conic, Data.List.Indexed.Counted
+  -- other-modules:       
+  other-extensions:    RankNTypes, GADTs, PolyKinds, ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, TypeOperators
+  build-depends:       base >=4.7 && <4.8, PeanoWitnesses >= 0.1
+  -- hs-source-dirs:      
+  default-language:    Haskell2010
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Kenneth Foner
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Kenneth Foner nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain