@@ -5,13 +5,14 @@ The implementation is similar to that shown in the paper.
55{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,
66 TypeFamilies, UndecidableInstances, MultiParamTypeClasses,
77 FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables,
8− ConstraintKinds #-}
8+ ConstraintKinds, IncoherentInstances #-}
99
1010module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
1111 Combine, Combinable(..), Cmp,
1212 Nubable, nub,
1313 Lookup, Member, (:\), Split, split,
14− IsMap, AsMap, asMap,
14+ IsMember, lookp, Updatable, update,
15+ IsMap, AsMap, asMap,
1516 Submap, submap) where
1617
1718import GHC.TypeLits
@@ -45,17 +46,17 @@ type family Combine (a :: v) (b :: v) :: v
4546
4647{-| Delete elements from a map by key -}
4748type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
48− '[] :\ k = '[]
49− ((k :-> v) ': m) :\ k = m :\ k
50− (kvp ': m) :\ k = kvp ': (m :\ k)
49+ '[] :\ k = '[]
50+ ((k :-> v) ': m) :\ k = m :\ k
51+ (kvp ': m) :\ k = kvp ': (m :\ k)
5152
52−{-| Lookup elements from a map -}
53+{-| Type-level lookup of elements from a map -}
5354type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
5455 Lookup '[] k = Nothing
5556 Lookup ((k :-> v) ': m) k = Just v
5657 Lookup (kvp ': m) k = Lookup m k
5758
58−{-| Membership test -}
59+{-| Membership test as type function -}
5960type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
6061 Member k '[] = False
6162 Member k ((k :-> v) ': m) = True
@@ -75,6 +76,37 @@ data Map (n :: [Mapping Symbol *]) where
7576 Empty :: Map '[]
7677 Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
7778
79+{-| Membership test a type class (predicate) -}
80+class IsMember v t m where
81+ {-| Value-level lookup of elements from a map, via type class predicate -}
82+ lookp :: Var v -> Map m -> t
83+
84+instance {-# OVERLAPS #-} IsMember v t ((v ':-> t) ': m) where
85+ lookp _ (Ext _ x _) = x
86+
87+instance {-# OVERLAPPABLE #-} IsMember v t m => IsMember v t (x ': m) where
88+ lookp v (Ext _ _ m) = lookp v m
89+
90+
91+{-| Updatability as a type class -}
92+class Updatable v t m n where
93+ {-| Update a map with `m` at variable `v` with a value of type `t`
94+ to produce a map of type `n` -}
95+ update :: Map m -> Var v -> t -> Map n
96+
97+instance {-# OVERLAPS #-} Updatable v t ((v ':-> s) ': m) ((v ':-> t) ': m) where
98+ update (Ext v _ m) _ x = Ext v x m
99+
100+instance Updatable v t m n => Updatable v t ((w ':-> y) ': m) ((w ':-> y) ': n) where
101+ update (Ext w y m) v x = Ext w y (update m v x)
102+
103+-- instance Updatable v t '[] '[v ':-> t] where
104+-- update Empty v x = Ext v x Empty
105+
106+instance Updatable v t s ((v ':-> t) ': s) where
107+ update xs v x = Ext v x xs
108+
109+
78110{-| Predicate to check if in normalised map form -}
79111type IsMap s = (s ~ Nub (Sort s))
80112
@@ -89,7 +121,7 @@ instance Show (Map '[]) where
89121 show Empty = "{}"
90122
91123instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where
92− show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}"
124+ show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ show' s ++ "}"
93125
94126class Show' t where
95127 show' :: t -> String
@@ -98,12 +130,25 @@ instance Show' (Map '[]) where
98130instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s)) where
99131 show' (Ext k v s) = ", " ++ show k ++ " :-> " ++ show v ++ (show' s)
100132
101−{-| Union of two finite maps -}
133+instance Eq (Map '[]) where
134+ Empty == Empty = True
135+
136+instance (Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
137+ (Ext Var v m) == (Ext Var v' m') = v == v' && m == m'
138+
139+instance Ord (Map '[]) where
140+ compare Empty Empty = EQ
141+
142+instance (Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) where
143+ compare (Ext Var v m) (Ext Var v' m') = compare v v' `mappend` compare m m'
144+
145+{-| Union of two finite maps (normalising) -}
102146union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
103147union s t = nub (quicksort (append s t))
104148
105149type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
106150
151+{-| Append of two finite maps (non normalising) -}
107152append :: Map s -> Map t -> Map (s :++ t)
108153append Empty x = x
109154append (Ext k v xs) ys = Ext k v (append xs ys)
@@ -118,11 +163,15 @@ class Sortable xs where
118163instance Sortable '[] where
119164 quicksort Empty = Empty
120165
121−instance (Sortable (Filter FMin (k :-> v) xs),
122− Sortable (Filter FMax (k :-> v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
123− quicksort (Ext k v xs) = ((quicksort (less k v xs)) `append` (Ext k v Empty)) `append` (quicksort (more k v xs))
124− where less = filterV (Proxy::(Proxy FMin))
125− more = filterV (Proxy::(Proxy FMax))
166+instance (Sortable (Filter FMin (k :-> v) xs)
167+ , Sortable (Filter FMax (k :-> v) xs)
168+ , FilterV FMin k v xs
169+ , FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
170+ quicksort (Ext k v xs) =
171+ quicksort (less k v xs) `append` Ext k v Empty `append` quicksort (more k v xs)
172+ where
173+ less = filterV (Proxy::(Proxy FMin))
174+ more = filterV (Proxy::(Proxy FMax))
126175
127176{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
128177class FilterV (f::Flag) k v xs where
@@ -131,13 +180,19 @@ class FilterV (f::Flag) k v xs where
131180instance FilterV f k v '[] where
132181 filterV _ k v Empty = Empty
133182
134−instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
135− filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy ((Cmp x (k :-> v)) == LT)))
136− (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
183+instance (Conder (Cmp x (k :-> v) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
184+ filterV f@Proxy k v (Ext k' v' xs) =
185+ cond (Proxy::(Proxy (Cmp x (k :-> v) == LT)))
186+ (Ext k' v' (filterV f k v xs))
187+ (filterV f k v xs)
137188
138−instance (Conder (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ)), FilterV FMax k v xs) => FilterV FMax k v (x ': xs) where
139− filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ))))
140− (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
189+instance
190+ (Conder ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ)), FilterV FMax k v xs)
191+ => FilterV FMax k v (x ': xs) where
192+ filterV f@Proxy k v (Ext k' v' xs) =
193+ cond (Proxy::(Proxy ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ))))
194+ (Ext k' v' (filterV f k v xs))
195+ (filterV f k v xs)
141196
142197class Combinable t t' where
143198 combine :: t -> t' -> Combine t t'
@@ -151,13 +206,14 @@ instance Nubable '[] where
151206instance Nubable '[e] where
152207 nub (Ext k v Empty) = Ext k v Empty
153208
154−instance {-# OVERLAPABLE #-}
209+instance {-# OVERLAPPABLE #-}
155210 (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
156211 Nubable (f ': s)) => Nubable (e ': f ': s) where
157212 nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
158213
159214instance {-# OVERLAPS #-}
160− (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where
215+ (Combinable v v', Nubable ((k :-> Combine v v') ': s))
216+ => Nubable ((k :-> v) ': (k :-> v') ': s) where
161217 nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)
162218
163219