diff --git a/example.hs b/example.hs
--- a/example.hs
+++ b/example.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}
+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}
 
 import GHC.TypeLits
 import Data.Type.Map
@@ -8,19 +8,24 @@
 -- 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 
 
+foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
+foo = Ext (Var :: (Var "x")) 2
+    $ Ext (Var :: (Var "z")) True
+    $ Ext (Var :: (Var "w")) 5
+    $ Empty
 
+foo' :: Map (AsMap '["z" :-> Bool, "x" :-> Int, "w" :-> Int])
+foo' = asMap foo
+
 bar :: Map '["y" :-> Int, "w" :-> Int]
 bar = Ext (Var :: (Var "y")) 3 $
        Ext (Var :: (Var "w")) 1 $
-         Empty 
+         Empty
 
 -- GHC can easily infer this type, so an explicit signature not necessary
 -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
 foobar = foo `union` bar
+
+foobarToFoo :: Map '["w" :-> Int, "x" :-> Int, "z" :-> Bool]
+foobarToFoo = submap foobar
diff --git a/example2.hs b/example2.hs
new file mode 100644
--- /dev/null
+++ b/example2.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}
+
+import GHC.TypeLits
+import Data.Type.Set
+
+type instance Cmp (Natural n) (Natural m) = CmpNat n m
+
+data Natural (a :: Nat) where
+    Z :: Natural 0
+    S :: Natural n -> Natural (n + 1)
+
+deriving instance Show (Natural n)
+
+-- foo :: Set '[Natural 0, Natural 1, Natural 3]
+foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
+
+-- bar :: Set '[Natural 1, Natural 2]
+bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
+
+-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
+foobar = foo `union` bar
diff --git a/src/Data/Type/Map.hs b/src/Data/Type/Map.hs
--- a/src/Data/Type/Map.hs
+++ b/src/Data/Type/Map.hs
@@ -2,18 +2,22 @@
 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 #-}
+{-# 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
+module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
+                      Combine, Combinable(..), Cmp,
+                      Nubable, nub,
+                      Lookup, Member, (:\), Split, split,
+                      IsMap, AsMap, asMap, 
+                      Submap, submap) 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)
+import Data.Type.Set (Cmp, Proxy(..), Flag(..), Sort, Filter, (:++))
 
 {- Throughout, type variables
    'k' ranges over "keys"
@@ -22,7 +26,7 @@
    'm', 'n' range over "maps" -}
 
 -- Mappings
-infixr 4 :-> 
+infixr 4 :->
 {-| A key-value pair -}
 data Mapping k v = k :-> v
 
@@ -61,7 +65,7 @@
 -- Value-level map with a type-level representation
 
 {-| Pair a symbol (representing a variable) with a type -}
-data Var (k :: Symbol) = Var 
+data Var (k :: Symbol) = Var
 
 instance KnownSymbol k => Show (Var k) where
     show = symbolVal
@@ -71,11 +75,21 @@
     Empty :: Map '[]
     Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
 
+{-| Predicate to check if in normalised map form -}
+type IsMap s = (s ~ Nub (Sort s))
+
+{-| At the type level, normalise the list form to the map form -}
+type AsMap s = Nub (Sort s)
+
+{-| At the value level, noramlise the list form to the map form -}
+asMap :: (Sortable s, Nubable (Sort s)) => Map s -> Map (AsMap s)
+asMap x = nub (quicksort x)
+
 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) ++ "}" 
+    show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}"
 
 class Show' t where
     show' :: t -> String
@@ -95,7 +109,7 @@
 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'
+type instance Cmp (k :-> v) (k' :-> v') = CmpSymbol k k'
 
 {-| Value-level quick sort that respects the type-level ordering -}
 class Sortable xs where
@@ -119,11 +133,11 @@
 
 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) 
+                                        (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)  
+                                        (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
 
 class Combinable t t' where
     combine :: t -> t' -> Combine t t'
@@ -137,14 +151,15 @@
 instance Nubable '[e] where
     nub (Ext k v Empty) = Ext k v Empty
 
-instance {-# OVERLAPPING #-}
+instance {-# OVERLAPPABLE #-}
+     (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))
+
+instance {-# OVERLAPS #-}
     (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)
@@ -155,3 +170,36 @@
 instance Conder False where
     cond _ s t = t
 
+
+{-| Splitting a union of maps, given the maps we want to split it into -}
+class Split s t st where
+   -- where st ~ Union s t
+   split :: Map st -> (Map s, Map t)
+
+instance Split '[] '[] '[] where
+   split Empty = (Empty, Empty)
+
+instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where
+   split (Ext k v st) = let (s, t) = split st
+                        in (Ext k v s, Ext k v t)
+
+instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where
+   split (Ext k v st) = let (s, t) = split st
+                        in  (Ext k v s, t)
+
+instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
+   split (Ext k v st) = let (s, t) = split st
+                        in  (s, Ext k v t)
+
+{-| Construct a submap 's' from a supermap 't' -}
+class Submap s t where
+   submap :: Map t -> Map s
+
+instance Submap '[] '[] where
+   submap xs = Empty
+
+instance {-# OVERLAPPABLE #-} Submap s t => Submap s (x ': t) where
+   submap (Ext _ _ xs) = submap xs
+
+instance {-# OVERLAPS #-} Submap s t => Submap  (x ': s) (x ': t) where
+   submap (Ext k v xs) = Ext k v (submap xs)
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,10 +1,12 @@
-{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, 
-             MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
-             UndecidableInstances, ConstraintKinds, ScopedTypeVariables #-}
+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
+             MultiParamTypeClasses, FlexibleInstances, PolyKinds,
+             FlexibleContexts, UndecidableInstances, ConstraintKinds,
+             ScopedTypeVariables #-}
 
-module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, 
-                      Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..), 
-                      Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..), Delete(..), Proxy(..)) where
+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
+                      Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
+                      Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
+                      Delete(..), Proxy(..)) where
 
 import GHC.TypeLits
 import Data.Type.Bool
@@ -12,10 +14,10 @@
 
 data Proxy (p :: k) = Proxy
 
--- Value-level 'Set' representation,  essentially a list 
+-- Value-level 'Set' representation,  essentially a list
 data Set (n :: [*]) where
     {--| Construct an empty set -}
-    Empty :: Set '[]   
+    Empty :: Set '[]
     {--| Extend a set with an element -}
     Ext :: e -> Set s -> Set (e ': s)
 
@@ -23,7 +25,7 @@
     show Empty = "{}"
 
 instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
-    show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}" 
+    show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
 
 class Show' t where
     show' :: t -> String
@@ -43,8 +45,8 @@
 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, 
+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)
 
@@ -70,22 +72,22 @@
 {-| 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) 
+   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
+instance {-# OVERLAPPABLE #-} 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
+instance {-# OVERLAPS #-} 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) 
+                      in  (Ext x s, t)
 
-instance (Split s t st) => Split s (x ': t) (x ': st) where
+instance {-# OVERLAPS #-} (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) 
+                      in  (s, Ext x t)
 
 
 
@@ -97,7 +99,7 @@
     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, 
+    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
@@ -112,7 +114,7 @@
 instance Nubable (e ': s) => Nubable (e ': e ': s) where
     nub (Ext _ (Ext e s)) = nub (Ext e s)
 
-instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), 
+instance {-# OVERLAPS #-} (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))
 
@@ -121,11 +123,11 @@
 class Subset s t where
    subset :: Set t -> Set s
 
-instance Subset '[] '[] where 
+instance Subset '[] '[] where
    subset xs = Empty
 
-instance Subset '[] (x ': t) where 
-   subset xs = Empty
+instance Subset s t => Subset s (x ': t) where
+   subset (Ext _ xs) = subset xs
 
 instance Subset s t => Subset (x ': s) (x ': t) where
    subset (Ext x xs) = Ext x (subset xs)
@@ -140,8 +142,8 @@
 
 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) 
+            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 '[] = '[]
@@ -174,11 +176,11 @@
 
 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) 
+                                        (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)  
+                                        (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)
@@ -192,4 +194,3 @@
 {-| Open-family for the ordering operation in the sort -}
 
 type family Cmp (a :: k) (b :: k) :: Ordering
-
diff --git a/type-level-sets.cabal b/type-level-sets.cabal
--- a/type-level-sets.cabal
+++ b/type-level-sets.cabal
@@ -1,39 +1,44 @@
 name:                   type-level-sets
-version:                0.6.1
+version:                0.7
 synopsis:               Type-level sets and finite maps (with value-level counterparts)
 description:            
    This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
    finite 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). This version now uses Quicksort to normalise the representation.
+   and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation.	
    .
-   Here is a brief example for finite maps.: 
+   Here is a brief example for finite maps: 
    .
    >
    > import Data.Type.Map
    >
-   > 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 
+   > -- Specify how to combine duplicate key-value pairs for Int values
+   > type instance Combine Int Int = Int
+   > instance Combinable Int Int where
+   >     combine x y = x + y
    >
+   > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
+   > foo = Ext (Var :: (Var "x")) 2 
+   >     $ Ext (Var :: (Var "z")) True 
+   >     $ Ext (Var :: (Var "w")) 5 
+   >     $ Empty 
+   >
    > bar :: Map '["y" :-> Int, "w" :-> Int]
-   > bar = Ext ((Var :: (Var "y")) :-> 3) $
-   >         Ext ((Var :: (Var "w")) :-> 1) $
-   >           Empty
+   > bar = Ext (Var :: (Var "y")) 3
+   >     $ Ext (Var :: (Var "w")) 1
+   >     $ Empty
    >  
-   > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
+   > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
    > foobar = foo `union` bar
    .
-   The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
+   The 'Map' 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)]
+   > {w :-> 6, x :-> 2, y :-> 3, z :-> True}
    .
-   Thus, we see that the first value paired with the \"w\" variable is dropped.
+   Thus, we see that the values for \"w\" are added together. 
    For sets, here is an example:
    .
    > import GHC.TypeLits
@@ -64,9 +69,9 @@
 stability:              experimental
 build-type:             Simple
 cabal-version:          >= 1.6
-tested-with:            GHC == 7.8.2
+tested-with:            GHC == 7.10.3
 
-extra-source-files:     example.hs
+extra-source-files:     example.hs, example2.hs
 
 
 source-repository head
@@ -80,5 +85,5 @@
   exposed-modules:      Data.Type.Set
                         Data.Type.Map
                         
-  build-depends:        base >= 4.7.0.0 && < 5,
+  build-depends:        base < 5,
                         ghc-prim