diff --git a/Data/Vinyl.hs b/Data/Vinyl.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl.hs
@@ -0,0 +1,14 @@
+module Data.Vinyl
+  ( module Data.Vinyl.Lens
+  , module Data.Vinyl.Witnesses
+  , module Data.Vinyl.Field
+  , module Data.Vinyl.Rec
+  , module Data.Vinyl.Relation
+  ) where
+
+import Data.Vinyl.Lens
+import Data.Vinyl.Witnesses
+import Data.Vinyl.Field
+import Data.Vinyl.Rec
+import Data.Vinyl.Relation
+
diff --git a/Data/Vinyl/Field.hs b/Data/Vinyl/Field.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Field.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+
+module Data.Vinyl.Field where
+
+import GHC.TypeLits
+
+-- A field is a symbol key and a type for its value.
+data (:::) :: Symbol -> * -> * where
+  Field :: sy ::: t
+
+instance (SingI sy, Show t) => Show (sy ::: t) where
+  show Field = fromSing (sing :: Sing sy)
diff --git a/Data/Vinyl/Lens.hs b/Data/Vinyl/Lens.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Lens.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE GADTs #-}
+
+module Data.Vinyl.Lens
+  ( module Control.Lens
+  , RLens
+  , rLens
+  , rGet
+  , rPut
+  , rMod
+  ) where
+
+import Data.Vinyl.Rec
+import Data.Vinyl.Field
+import Data.Vinyl.Witnesses
+
+import Control.Lens
+
+type RLens sy t = IElem (sy ::: t) fs => SimpleLens (Rec fs) t
+
+rLens :: (sy ::: t) -> RLens sy t
+rLens f = rLens' f implicitly
+
+rGet = view . rLens
+
+rPut = set . rLens
+rMod = over . rLens
+
+-- Records have lenses
+rLens' :: (f ~ (sy ::: t)) => f -> Elem f fs -> SimpleLens (Rec fs) t
+rLens' _ Here = lens (\((_,x) :& xs) -> x) (\((k,_) :& xs) x -> (k,x) :& xs)
+rLens' f (There p) = rLensPrepend $ rLens' f p
+
+rLensPrepend :: SimpleLens (Rec fs) t -> SimpleLens (Rec (f ': fs)) t
+rLensPrepend l = lens (\(_ :& xs) -> view l xs) (\(a :& xs) x -> a :& (set l x xs))
+
diff --git a/Data/Vinyl/Rec.hs b/Data/Vinyl/Rec.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Rec.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Data.Vinyl.Rec
+  ( Rec(..)
+  , (=:)
+  , (<+>)
+  ) where
+
+import Data.Vinyl.Field
+import GHC.TypeLits
+
+-- A record is parameterized by a list of fields.
+data Rec :: [*] -> * where
+  RNil :: Rec '[]
+  (:&) :: (f ~ (sy ::: t)) => (f, t) -> Rec fs -> Rec (f ': fs)
+infixr :&
+
+-- Appends records
+(<+>) :: Rec as -> Rec bs -> Rec (as ++ bs)
+RNil      <+> xs = xs
+(x :& xs) <+> ys =  x :& (xs <+> ys)
+infixl 8 <+>
+
+-- Shorthand for a record with a single field
+(=:) :: sy ::: t -> t -> Rec '[sy ::: t]
+a =: b = (a, b) :& RNil
+
+-- Type level list append
+type family (as :: [*]) ++ (bs :: [*]) :: [*]
+type instance '[] ++ bs = bs
+type instance (a ': as) ++ bs  = a ': (as ++ bs)
+
+
+instance Show (Rec '[]) where
+  show RNil = "{}"
+instance (SingI sy, Show t, Show (Rec fs)) => Show (Rec ((sy ::: t) ': fs)) where
+  show ((k,x) :& xs) = show k ++ " :=: " ++ show x ++ ", " ++ show xs
+
+
+instance Eq (Rec '[]) where
+  _ == _ = True
+instance (Eq t, Eq (Rec fs)) => Eq (Rec ((s ::: t) ': fs)) where
+  ((_,x) :& xs) == ((_,y) :& ys) = (x == y) && (xs == ys)
+
diff --git a/Data/Vinyl/Relation.hs b/Data/Vinyl/Relation.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Relation.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+
+module Data.Vinyl.Relation
+  ( (<:)(..)
+  , (:~:)
+  , (~=)
+  , rIso
+  ) where
+
+import Data.Vinyl.Witnesses
+import Data.Vinyl.Field
+import Data.Vinyl.Rec
+import Data.Vinyl.Lens
+
+import GHC.Prim (Constraint)
+
+-- A subtyping relation
+class (IsSubtype r1 r2) => r1 <: r2 where
+  cast :: r1 -> r2
+
+-- On record is a subtype of another if the fields of the latter are a
+-- subset of the fields of the former.
+type family IsSubtype r1 r2 :: Constraint
+type instance IsSubtype (Rec ss) (Rec ts) = ISubset ts ss
+
+-- If two records types are subtypes of each other, that means that they
+-- differ only in order of fields.
+type r1 :~: r2 = (r1 <: r2, r2 <: r1)
+
+-- Term-level record congruence
+(~=) :: (Eq a, a :~: b) => a -> b -> Bool
+x ~= y = x == (cast y)
+
+instance Rec xs <: (Rec '[]) where
+  cast _ = RNil
+
+instance (y ~ (sy ::: t), IElem y xs, Rec xs <: Rec ys) => Rec xs <: Rec (y ': ys) where
+  cast r = (field, rGet field r) :& cast r
+    where field = lookupField implicitly r
+
+lookupField :: Elem x xs -> Rec xs -> x
+lookupField Here ((k,_) :& _) = k
+lookupField (There p) (_ :& xs) = lookupField p xs
+
+rIso :: (r1 :~: r2) => SimpleIso r1 r2
+rIso = iso cast cast
+
diff --git a/Data/Vinyl/Unicode.hs b/Data/Vinyl/Unicode.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Unicode.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module Data.Vinyl.Unicode where
+
+import Data.Vinyl.Rec
+import Data.Vinyl.Relation
+import Data.Vinyl.Witnesses
+
+type x ∈ xs = IElem x xs
+type xs ⊆ ys = ISubset xs ys
+type r1 ≅ r2 = r1 :~: r2
+
+(≅) = (~=)
diff --git a/Data/Vinyl/Witnesses.hs b/Data/Vinyl/Witnesses.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Witnesses.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+
+module Data.Vinyl.Witnesses where
+
+class Implicit p where
+  implicitly :: p
+
+type IElem x xs = Implicit (Elem x xs)
+data Elem :: k -> [k] -> * where
+  Here  :: Elem x (x ': xs)
+  There :: Elem x xs -> Elem x (y ': xs)
+
+type ISubset xs ys = Implicit (Subset xs ys)
+data Subset :: [k] -> [k] -> * where
+  SubsetNil  :: Subset '[] xs
+  SubsetCons ::
+    Elem x ys ->
+    Subset xs ys ->
+    Subset (x ': xs) ys
+
+instance Implicit (Elem x (x ': xs)) where
+  implicitly = Here
+instance Implicit (Elem x xs) => Implicit (Elem x (y ': xs)) where
+  implicitly = There implicitly
+
+instance Implicit (Subset '[] xs) where
+  implicitly = SubsetNil
+instance (IElem x ys, ISubset xs ys) => Implicit (Subset (x ': xs) ys) where
+  implicitly = SubsetCons implicitly implicitly
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (C) 2012 Jonathan Sterling
+
+Permission is hereby granted, free of charge, to any person obtaining a
+copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
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
diff --git a/vinyl.cabal b/vinyl.cabal
new file mode 100644
--- /dev/null
+++ b/vinyl.cabal
@@ -0,0 +1,28 @@
+-- Initial vinyl.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                vinyl
+version:             0.1.0.0
+synopsis:            Extensible Records
+-- description:
+license:             MIT
+license-file:        LICENSE
+author:              Jonathan Sterling
+maintainer:          jonsterling@me.com
+-- copyright:
+category:            Data
+build-type:          Simple
+cabal-version:       >=1.8
+
+description: Extensible records for Haskell with lenses using modern GHC features.
+
+
+source-repository head
+  type:     git
+  location: https://github.com/jonsterling/Vinyl/
+
+
+library
+  exposed-modules:     Data.Vinyl, Data.Vinyl.Field, Data.Vinyl.Lens, Data.Vinyl.Witnesses, Data.Vinyl.Rec, Data.Vinyl.Relation, Data.Vinyl.Unicode
+  -- other-modules:
+  build-depends:       base ==4.6.*, lens >=3.0, ghc-prim