@@ -2,18 +2,21 @@
22The implementation is similar to that shown in the paper.
33 "Embedding effect systems in Haskell" Orchard, Petricek 2014 -}
44
5−{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,
6− TypeFamilies, UndecidableInstances, MultiParamTypeClasses,
7− FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables, ConstraintKinds #-}
5+{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,
6+ TypeFamilies, UndecidableInstances, MultiParamTypeClasses,
7+ FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables,
8+ ConstraintKinds #-}
89
9−module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
10− Combine, Combinable(..), Cmp,
11− Lookup, Member, (:\)) where
10+module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
11+ Combine, Combinable(..), Cmp,
12+ Nubable, nub,
13+ Lookup, Member, (:\), Split, split, IsMap,
14+ Submap, submap) where
1215
1316import GHC.TypeLits
1417import Data.Type.Bool
1518import Data.Type.Equality
16−import Data.Type.Set hiding (Set(..), Nub,Union,Nubable,Sortable,Unionable,append,union,quicksort,nub)
19+import Data.Type.Set (Cmp, Proxy(..), Flag(..), Sort, Filter, (:++))
1720
1821{- Throughout, type variables
1922 'k' ranges over "keys"
@@ -22,7 +25,7 @@ import Data.Type.Set hiding (Set(..), Nub,Union,Nubable,Sortable,Unionable,appen
2225 'm', 'n' range over "maps" -}
2326
2427-- Mappings
25−infixr 4 :->
28+infixr 4 :->
2629{-| A key-value pair -}
2730data Mapping k v = k :-> v
2831
@@ -61,7 +64,7 @@ type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
6164-- Value-level map with a type-level representation
6265
6366{-| Pair a symbol (representing a variable) with a type -}
64−data Var (k :: Symbol) = Var
67+data Var (k :: Symbol) = Var
6568
6669instance KnownSymbol k => Show (Var k) where
6770 show = symbolVal
@@ -71,11 +74,21 @@ data Map (n :: [Mapping Symbol *]) where
7174 Empty :: Map '[]
7275 Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
7376
77+{-| Predicate to check if in normalised map form -}
78+type IsMap s = (s ~ Nub (Sort s))
79+
80+{-| At the type level, normalise the list form to the map form -}
81+type AsMap s = Nub (Sort s)
82+
83+{-| At the value level, noramlise the list form to the map form -}
84+asMap :: (Sortable s, Nubable (Sort s)) => Map s -> Map (AsMap s)
85+asMap x = nub (quicksort x)
86+
7487instance Show (Map '[]) where
7588 show Empty = "{}"
7689
7790instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where
78− show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}"
91+ show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}"
7992
8093class Show' t where
8194 show' :: t -> String
@@ -95,7 +108,7 @@ append Empty x = x
95108append (Ext k v xs) ys = Ext k v (append xs ys)
96109
97110type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'
98−type instance Cmp (k :-> v) (k' :-> v) = CmpSymbol k k'
111+type instance Cmp (k :-> v) (k' :-> v') = CmpSymbol k k'
99112
100113{-| Value-level quick sort that respects the type-level ordering -}
101114class Sortable xs where
@@ -119,11 +132,11 @@ instance FilterV f k v '[] where
119132
120133instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
121134 filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy ((Cmp x (k :-> v)) == LT)))
122− (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
135+ (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
123136
124137instance (Conder (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ)), FilterV FMax k v xs) => FilterV FMax k v (x ': xs) where
125138 filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ))))
126− (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
139+ (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
127140
128141class Combinable t t' where
129142 combine :: t -> t' -> Combine t t'
@@ -142,10 +155,11 @@ instance {-# OVERLAPPING #-}
142155 nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)
143156
144157instance {-# OVERLAPPING #-}
145− (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
158+ (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
146159 Nubable (f ': s)) => Nubable (e ': f ': s) where
147160 nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
148161
162+
149163class Conder g where
150164 cond :: Proxy g -> Map s -> Map t -> Map (If g s t)
151165
@@ -155,3 +169,36 @@ instance Conder True where
155169instance Conder False where
156170 cond _ s t = t
157171
172+
173+{-| Splitting a union of maps, given the maps we want to split it into -}
174+class Split s t st where
175+ -- where st ~ Union s t
176+ split :: Map st -> (Map s, Map t)
177+
178+instance Split '[] '[] '[] where
179+ split Empty = (Empty, Empty)
180+
181+instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where
182+ split (Ext k v st) = let (s, t) = split st
183+ in (Ext k v s, Ext k v t)
184+
185+instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where
186+ split (Ext k v st) = let (s, t) = split st
187+ in (Ext k v s, t)
188+
189+instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
190+ split (Ext k v st) = let (s, t) = split st
191+ in (s, Ext k v t)
192+
193+{-| Construct a submap 's' from a supermap 't' -}
194+class Submap s t where
195+ submap :: Map t -> Map s
196+
197+instance Submap '[] '[] where
198+ submap xs = Empty
199+
200+instance {-# OVERLAPPABLE #-} Submap s t => Submap s (x ': t) where
201+ submap (Ext _ _ xs) = submap xs
202+
203+instance {-# OVERLAPS #-} Submap s t => Submap (x ': s) (x ': t) where
204+ submap (Ext k v xs) = Ext k v (submap xs)