diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Copyright (c) 2014, Dominic Orchard
+
+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.
+
+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,6 @@
+module Main (main) where
+
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/example.hs b/example.hs
new file mode 100644
--- /dev/null
+++ b/example.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds, TypeOperators #-}
+
+import Data.Type.Set
+
+foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
+foo = Ext ((Var :: (Var "x")) :-> 2) $
+       Ext ((Var :: (Var "z")) :-> 4) $
+        Ext ((Var :: (Var "w")) :-> 5) $
+         Empty 
+
+bar :: Set '["y" :-> Int, "w" :-> Int]
+bar = Ext ((Var :: (Var "y")) :-> 3) $
+       Ext ((Var :: (Var "w")) :-> 1) $
+         Empty 
+
+-- GHC can easily infer this type, so an explicit signature not necessary
+-- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
+foobar = foo `union` bar
diff --git a/src/Data/Type/Set.hs b/src/Data/Type/Set.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Set.hs
@@ -0,0 +1,214 @@
+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, 
+             MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
+             UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}
+
+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, 
+                      Sort, Sortable, Append(..), Split(..), Cmp, 
+                      Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
+                      (:->)(..), Var(..)) where
+
+import GHC.TypeLits
+import Data.Type.Bool
+import Data.Type.Equality
+import Data.Proxy
+
+{-| Core Set definition, in terms of lists -}
+data Set (n :: [*]) where
+    Empty :: Set '[]
+    Ext :: e -> Set s -> Set (e ': s)
+
+instance Show (Set '[]) where
+    show Empty = "{}"
+
+instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
+    show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}" 
+
+class Show' t where
+    show' :: t -> String
+instance Show' (Set '[]) where
+    show' Empty = ""
+instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
+    show' (Ext e s) = ", " ++ show e ++ (show' s)
+
+{-| At the type level, normalise the list form to the set form -}
+type AsSet s = Nub (Sort s)
+
+{-| At the value level, noramlise the list form to the set form -}
+asSet :: (Sortable s, Nubable (Sort s)) => Set s -> Set (AsSet s)
+asSet x = nub (quicksort x)
+
+{-| Predicate to check if in the set form -}
+type IsSet s = (s ~ Nub (Sort s))
+
+{-| Useful properties to be able to refer to someties -}
+type SetProperties f = (Union f '[] ~ f, Split f '[] f, 
+                        Union '[] f ~ f, Split '[] f f, 
+                        Union f f ~ f, Split f f f,
+                        Unionable f '[], Unionable '[] f)
+
+{-- Union --}
+
+{-| Union of sets -}
+type Union s t = Nub (Sort (Append s t))
+
+union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
+union s t = nub (quicksort (append s t))
+
+type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)))
+
+{-| List append (essentially set disjoint union) -}
+type family Append (s :: [k]) (t :: [k]) :: [k] where
+            Append '[] t = t
+            Append (x ': xs) ys = x ': (Append xs ys)
+
+append :: Set s -> Set t -> Set (Append s t)
+append Empty x = x
+append (Ext e xs) ys = Ext e (append xs ys)
+
+{-| Useful alias for append -}
+type (s :: [k]) :++ (t :: [k]) = Append s t
+
+{-| Splitting a union a set, given the sets we want to split it into -}
+class Split s t st where
+   -- where st ~ Union s t
+   split :: Set st -> (Set s, Set t) 
+
+instance Split '[] '[] '[] where
+   split Empty = (Empty, Empty)
+
+instance Split s t st => Split (x ': s) (x ': t) (x ': st) where
+   split (Ext x st) = let (s, t) = split st
+                      in (Ext x s, Ext x t)
+
+instance Split s t st => Split (x ': s) t (x ': st) where
+   split (Ext x st) = let (s, t) = split st
+                      in  (Ext x s, t) 
+
+instance (Split s t st) => Split s (x ': t) (x ': st) where
+   split (Ext x st) = let (s, t) = split st
+                      in  (s, Ext x t) 
+
+
+
+{-| Remove duplicates from a sorted list -}
+type family Nub t where
+    Nub '[]           = '[]
+    Nub '[e]          = '[e]
+    Nub (e ': e ': s) = Nub (e ': s)
+    Nub (e ': f ': s) = e ': Nub (f ': s)
+
+{-| Value-level counterpart to the type-level 'Nub'
+    Note: the value-level case for equal types is not define here, 
+          but should be given per-application, e.g., custom 'merging' behaviour may be required -}
+
+class Nubable t where
+    nub :: Set t -> Set (Nub t)
+
+instance Nubable '[] where
+    nub Empty = Empty
+
+instance Nubable '[e] where
+    nub (Ext x Empty) = Ext x Empty
+
+instance Nubable (e ': s) => Nubable (e ': e ': s) where
+    nub (Ext _ (Ext e s)) = nub (Ext e s)
+
+instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), 
+              Nubable (f ': s)) => Nubable (e ': f ': s) where
+    nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
+
+
+{-| Construct a subsetset 's' from a superset 't' -}
+class Subset s t where
+   subset :: Set t -> Set s
+
+instance Subset '[] '[] where 
+   subset xs = Empty
+
+instance Subset '[] (x ': t) where 
+   subset xs = Empty
+
+instance Subset s t => Subset (x ': s) (x ': t) where
+   subset (Ext x xs) = Ext x (subset xs)
+
+
+{-| Type-level quick sort for normalising the representation of sets -}
+type family Sort (xs :: [k]) :: [k] where
+            Sort '[]       = '[]
+            Sort (x ': xs) = ((Sort (Filter FMin x xs)) :++ '[x]) :++ (Sort (Filter FMax x xs))
+
+data Flag = FMin | FMax
+
+type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
+            Filter f p '[]       = '[]
+            Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs) 
+            Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs) 
+
+{-| Value-level quick sort that respects the type-level ordering -}
+class Sortable xs where
+    quicksort :: Set xs -> Set (Sort xs)
+
+instance Sortable '[] where
+    quicksort Empty = Empty
+
+instance (Sortable (Filter FMin p xs),
+          Sortable (Filter FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable (p ': xs) where
+    quicksort (Ext p xs) = ((quicksort (less p xs)) `append` (Ext p Empty)) `append` (quicksort (more p xs))
+                           where less = filterV (Proxy::(Proxy FMin))
+                                 more = filterV (Proxy::(Proxy FMax))
+
+{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
+class FilterV (f::Flag) p xs where
+    filterV :: Proxy f -> p -> Set xs -> Set (Filter f p xs)
+
+instance FilterV f p '[] where
+    filterV _ p Empty      = Empty
+
+instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
+    filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))
+                                        (Ext x (filterV f p xs)) (filterV f p xs) 
+
+instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
+    filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))
+                                        (Ext x (filterV f p xs)) (filterV f p xs)  
+
+class Conder g where
+    cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
+
+instance Conder True where
+    cond _ s t = s
+
+instance Conder False where
+    cond _ s t = t
+
+{-| Open-family for the ordering operation in the sort -}
+
+type family Cmp (a :: k) (b :: k) :: Ordering
+
+{-| Pair a symbol (represetning a variable) with a type -}
+infixl 2 :->
+data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
+
+data Var (k :: Symbol) where Var :: Var k 
+                             {-| Some special defaults for some common names -}
+                             X   :: Var "x"
+                             Y   :: Var "y"
+                             Z   :: Var "z"
+
+
+instance (Show (Var k), Show v) => Show (k :-> v) where
+    show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
+instance Show (Var "x") where
+    show X   = "x"
+    show Var = "Var"
+instance Show (Var "y") where
+    show Y   = "y"
+    show Var = "Var"
+instance Show (Var "z") where
+    show Z   = "z"
+    show Var = "Var"
+instance Show (Var v) where
+    show _ = "Var"
+
+{-| Symbol comparison -}
+type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u
diff --git a/type-level-sets.cabal b/type-level-sets.cabal
new file mode 100644
--- /dev/null
+++ b/type-level-sets.cabal
@@ -0,0 +1,61 @@
+name:                   type-level-sets
+version:                0.5
+synopsis:               Type-level sets (with value-level counterparts and various operations)
+description:            
+   This package provides type-level sets (no duplicates, sorted to provide a nomral form) via 'Set', 
+   with value-level counterparts. Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard 
+   and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014)
+   .
+   Here is a brief example: 
+   .
+   >
+   > import Data.Type.Set
+   >
+   > foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
+   > foo = Ext ((Var :: (Var "x")) :-> 2) $
+   >         Ext ((Var :: (Var "z")) :-> 4) $
+   >           Ext ((Var :: (Var "w")) :-> 5) $
+   >             Empty 
+   >
+   > bar :: Set '["y" :-> Int, "w" :-> Int]
+   > bar = Ext ((Var :: (Var "y")) :-> 3) $
+   >         Ext ((Var :: (Var "w")) :-> 1) $
+   >           Empty
+   >  
+   > -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
+   > foobar = foo `union` bar
+   .
+   The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
+   The type signatures is commented out as it can be infered. Running the example we get:
+   .
+   > >>> foobar	
+   > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]
+   .
+   Thus, we see that the first value paired with the \"w\" variable is dropped.
+   .
+license:                BSD3
+license-file:           LICENSE
+category:               Type System, Data Structures
+copyright:              2013-14 University of Cambridge
+author:                 Dominic Orchard
+maintainer:             Dominic Orchard
+stability:              experimental
+build-type:             Simple
+cabal-version:          >= 1.6
+tested-with:            GHC == 7.8.2
+
+extra-source-files:     example.hs
+
+
+source-repository head
+  type: git
+  location: https://github.com/dorchard/type-level-sets
+
+library
+  hs-source-dirs:       src
+
+
+  exposed-modules:      Data.Type.Set
+                        
+  build-depends:        base < 5,
+                        ghc-prim