diff --git a/example.hs b/example.hs
--- a/example.hs
+++ b/example.hs
@@ -1,16 +1,24 @@
-{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}
 
-import Data.Type.Set
+import GHC.TypeLits
+import Data.Type.Map
 
-foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
-foo = Ext ((Var :: (Var "x")) :-> 2) $
-       Ext ((Var :: (Var "z")) :-> 4) $
-        Ext ((Var :: (Var "w")) :-> 5) $
+-- Specify that key-value pairs on Ints combine to an Int
+type instance Combine Int Int = Int
+-- Specify that Int values for matching keys should be added
+instance Combinable Int Int where
+    combine x y = x + y
+                             
+foo :: Map '["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) $
+
+bar :: Map '["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
diff --git a/src/Data/Type/Map.hs b/src/Data/Type/Map.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Map.hs
@@ -0,0 +1,157 @@
+{- This module provides type-level finite maps.
+The implementation is similar to that shown in the paper.
+ "Embedding effect systems in Haskell" Orchard, Petricek 2014  -}
+
+{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures, 
+             TypeFamilies, UndecidableInstances, MultiParamTypeClasses, 
+             FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables, ConstraintKinds #-}
+
+module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..), 
+                      Combine, Combinable(..), Cmp, 
+                      Lookup, Member, (:\)) where
+
+import GHC.TypeLits
+import Data.Type.Bool
+import Data.Type.Equality
+import Data.Type.Set hiding (Set(..), Nub,Union,Nubable,Sortable,Unionable,append,union,quicksort,nub)
+
+{- Throughout, type variables
+   'k' ranges over "keys"
+   'v'  ranges over "values"
+   'kvp' ranges over "key-value-pairs"
+   'm', 'n' range over "maps" -}
+
+-- Mappings
+infixr 4 :-> 
+{-| A key-value pair -}
+data Mapping k v = k :-> v
+
+{-| Union of two finite maps -}
+type Union m n = Nub (Sort (m :++ n))
+
+{-| Apply 'Combine' to values with matching key (removes duplicate keys) -}
+type family Nub t where
+   Nub '[]                             = '[]
+   Nub '[kvp]                          = '[kvp]
+   Nub ((k :-> v1) ': (k :-> v2) ': m) = Nub ((k :-> Combine v1 v2) ': m)
+   Nub (kvp1 ': kvp2 ': s)             = kvp1 ': Nub (kvp2 ': s)
+
+{-| Open type family for combining values in a map (that have the same key) -}
+type family Combine (a :: v) (b :: v) :: v
+
+{-| Delete elements from a map by key -}
+type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
+     '[]               :\ k = '[]
+     ((k :-> v) ': m)  :\ k = m :\ k
+     (kvp ': m)        :\ k = kvp ': (m :\ k)
+
+{-| Lookup elements from a map -}
+type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
+            Lookup '[]              k = Nothing
+            Lookup ((k :-> v) ': m) k = Just v
+            Lookup (kvp ': m)       k = Lookup m k
+
+{-| Membership test -}
+type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
+            Member k '[]              = False
+            Member k ((k :-> v) ': m) = True
+            Member k (kvp ': m)       = Member k m
+
+-----------------------------------------------------------------
+-- Value-level map with a type-level representation
+
+{-| Pair a symbol (representing a variable) with a type -}
+data Var (k :: Symbol) = Var 
+
+instance KnownSymbol k => Show (Var k) where
+    show = symbolVal
+
+{-| A value-level heterogenously-typed Map (with type-level representation in terms of lists) -}
+data Map (n :: [Mapping Symbol *]) where
+    Empty :: Map '[]
+    Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
+
+instance Show (Map '[]) where
+    show Empty = "{}"
+
+instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where
+    show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}" 
+
+class Show' t where
+    show' :: t -> String
+instance Show' (Map '[]) where
+    show' Empty = ""
+instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s)) where
+    show' (Ext k v s) = ", " ++ show k ++ " :-> " ++ show v ++ (show' s)
+
+{-| Union of two finite maps -}
+union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
+union s t = nub (quicksort (append s t))
+
+type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
+
+append :: Map s -> Map t -> Map (s :++ t)
+append Empty x = x
+append (Ext k v xs) ys = Ext k v (append xs ys)
+
+type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'
+type instance Cmp (k :-> v) (k' :-> v) = CmpSymbol k k'
+
+{-| Value-level quick sort that respects the type-level ordering -}
+class Sortable xs where
+    quicksort :: Map xs -> Map (Sort xs)
+
+instance Sortable '[] where
+    quicksort Empty = Empty
+
+instance (Sortable (Filter FMin (k :-> v) xs),
+          Sortable (Filter FMax (k :-> v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
+    quicksort (Ext k v xs) = ((quicksort (less k v xs)) `append` (Ext k v Empty)) `append` (quicksort (more k v 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) k v xs where
+    filterV :: Proxy f -> Var k -> v -> Map xs -> Map (Filter f (k :-> v) xs)
+
+instance FilterV f k v '[] where
+    filterV _ k v Empty      = Empty
+
+instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
+    filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy ((Cmp x (k :-> v)) == LT)))
+                                        (Ext k' v' (filterV f k v xs)) (filterV f k v xs) 
+
+instance (Conder (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ)), FilterV FMax k v xs) => FilterV FMax k v (x ': xs) where
+    filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ))))
+                                        (Ext k' v' (filterV f k v xs)) (filterV f k v xs)  
+
+class Combinable t t' where
+    combine :: t -> t' -> Combine t t'
+
+class Nubable t where
+    nub :: Map t -> Map (Nub t)
+
+instance Nubable '[] where
+    nub Empty = Empty
+
+instance Nubable '[e] where
+    nub (Ext k v Empty) = Ext k v Empty
+
+instance {-# OVERLAPPING #-}
+    (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where
+    nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)
+
+instance {-# OVERLAPPING #-}
+     (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), 
+              Nubable (f ': s)) => Nubable (e ': f ': s) where
+    nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
+
+class Conder g where
+    cond :: Proxy g -> Map s -> Map t -> Map (If g s t)
+
+instance Conder True where
+    cond _ s t = s
+
+instance Conder False where
+    cond _ s t = t
+
diff --git a/src/Data/Type/Set.hs b/src/Data/Type/Set.hs
--- a/src/Data/Type/Set.hs
+++ b/src/Data/Type/Set.hs
@@ -1,20 +1,22 @@
 {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, 
              MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
-             UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}
+             UndecidableInstances, ConstraintKinds, ScopedTypeVariables #-}
 
 module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, 
-                      Sort, Sortable, Append(..), Split(..), Cmp, 
-                      Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
-                      (:->)(..), Var(..)) where
+                      Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..), 
+                      Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..), Delete(..), Proxy(..)) where
 
 import GHC.TypeLits
 import Data.Type.Bool
 import Data.Type.Equality
-import Data.Proxy
 
-{-| Core Set definition, in terms of lists -}
+data Proxy (p :: k) = Proxy
+
+-- Value-level 'Set' representation,  essentially a list 
 data Set (n :: [*]) where
-    Empty :: Set '[]
+    {--| Construct an empty set -}
+    Empty :: Set '[]   
+    {--| Extend a set with an element -}
     Ext :: e -> Set s -> Set (e ': s)
 
 instance Show (Set '[]) where
@@ -49,25 +51,22 @@
 {-- Union --}
 
 {-| Union of sets -}
-type Union s t = Nub (Sort (Append s t))
+type Union s t = Nub (Sort (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)))
+type Unionable s t = (Sortable (s :++ t), Nubable (Sort (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)
+type family (:++) (x :: [k]) (y :: [k]) :: [k] where
+            '[]       :++ xs = xs
+            (x ': xs) :++ ys = x ': (xs :++ ys)
 
-append :: Set s -> Set t -> Set (Append s t)
+append :: Set s -> Set t -> Set (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
@@ -144,6 +143,15 @@
             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) 
 
+type family DeleteFromList (e :: elem) (list :: [elem]) where
+    DeleteFromList elem '[] = '[]
+    DeleteFromList elem (x ': xs) = If (Cmp elem x == EQ)
+                                       xs
+                                       (x ': DeleteFromList elem xs)
+
+type family Delete elem set where
+    Delete elem (Set xs) = Set (DeleteFromList elem xs)
+
 {-| Value-level quick sort that respects the type-level ordering -}
 class Sortable xs where
     quicksort :: Set xs -> Set (Sort xs)
@@ -185,30 +193,3 @@
 
 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
--- a/type-level-sets.cabal
+++ b/type-level-sets.cabal
@@ -1,15 +1,17 @@
 name:                   type-level-sets
-version:                0.5
-synopsis:               Type-level sets (with value-level counterparts and various operations)
+version:                0.6
+synopsis:               Type-level sets and finite maps (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 
+   This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
+   maps via 'Map', 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
+   > import Data.Type.Map
    >
    > foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
    > foo = Ext ((Var :: (Var "x")) :-> 2) $
@@ -56,6 +58,7 @@
 
 
   exposed-modules:      Data.Type.Set
+                        Data.Type.Map
                         
-  build-depends:        base < 5,
+  build-depends:        base >= 4.7.0.0 && < 5,
                         ghc-prim