@@ -0,0 +1,157 @@
1+{- This module provides type-level finite maps.
2+The implementation is similar to that shown in the paper.
3+ "Embedding effect systems in Haskell" Orchard, Petricek 2014 -}
4+
5+{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,
6+ TypeFamilies, UndecidableInstances, MultiParamTypeClasses,
7+ FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables, ConstraintKinds #-}
8+
9+module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
10+ Combine, Combinable(..), Cmp,
11+ Lookup, Member, (:\)) where
12+
13+import GHC.TypeLits
14+import Data.Type.Bool
15+import Data.Type.Equality
16+import Data.Type.Set hiding (Set(..), Nub,Union,Nubable,Sortable,Unionable,append,union,quicksort,nub)
17+
18+{- Throughout, type variables
19+ 'k' ranges over "keys"
20+ 'v' ranges over "values"
21+ 'kvp' ranges over "key-value-pairs"
22+ 'm', 'n' range over "maps" -}
23+
24+-- Mappings
25+infixr 4 :->
26+{-| A key-value pair -}
27+data Mapping k v = k :-> v
28+
29+{-| Union of two finite maps -}
30+type Union m n = Nub (Sort (m :++ n))
31+
32+{-| Apply 'Combine' to values with matching key (removes duplicate keys) -}
33+type family Nub t where
34+ Nub '[] = '[]
35+ Nub '[kvp] = '[kvp]
36+ Nub ((k :-> v1) ': (k :-> v2) ': m) = Nub ((k :-> Combine v1 v2) ': m)
37+ Nub (kvp1 ': kvp2 ': s) = kvp1 ': Nub (kvp2 ': s)
38+
39+{-| Open type family for combining values in a map (that have the same key) -}
40+type family Combine (a :: v) (b :: v) :: v
41+
42+{-| Delete elements from a map by key -}
43+type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
44+ '[] :\ k = '[]
45+ ((k :-> v) ': m) :\ k = m :\ k
46+ (kvp ': m) :\ k = kvp ': (m :\ k)
47+
48+{-| Lookup elements from a map -}
49+type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
50+ Lookup '[] k = Nothing
51+ Lookup ((k :-> v) ': m) k = Just v
52+ Lookup (kvp ': m) k = Lookup m k
53+
54+{-| Membership test -}
55+type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
56+ Member k '[] = False
57+ Member k ((k :-> v) ': m) = True
58+ Member k (kvp ': m) = Member k m
59+
60+-----------------------------------------------------------------
61+-- Value-level map with a type-level representation
62+
63+{-| Pair a symbol (representing a variable) with a type -}
64+data Var (k :: Symbol) = Var
65+
66+instance KnownSymbol k => Show (Var k) where
67+ show = symbolVal
68+
69+{-| A value-level heterogenously-typed Map (with type-level representation in terms of lists) -}
70+data Map (n :: [Mapping Symbol *]) where
71+ Empty :: Map '[]
72+ Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
73+
74+instance Show (Map '[]) where
75+ show Empty = "{}"
76+
77+instance (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) ++ "}"
79+
80+class Show' t where
81+ show' :: t -> String
82+instance Show' (Map '[]) where
83+ show' Empty = ""
84+instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s)) where
85+ show' (Ext k v s) = ", " ++ show k ++ " :-> " ++ show v ++ (show' s)
86+
87+{-| Union of two finite maps -}
88+union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
89+union s t = nub (quicksort (append s t))
90+
91+type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
92+
93+append :: Map s -> Map t -> Map (s :++ t)
94+append Empty x = x
95+append (Ext k v xs) ys = Ext k v (append xs ys)
96+
97+type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'
98+type instance Cmp (k :-> v) (k' :-> v) = CmpSymbol k k'
99+
100+{-| Value-level quick sort that respects the type-level ordering -}
101+class Sortable xs where
102+ quicksort :: Map xs -> Map (Sort xs)
103+
104+instance Sortable '[] where
105+ quicksort Empty = Empty
106+
107+instance (Sortable (Filter FMin (k :-> v) xs),
108+ Sortable (Filter FMax (k :-> v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
109+ quicksort (Ext k v xs) = ((quicksort (less k v xs)) `append` (Ext k v Empty)) `append` (quicksort (more k v xs))
110+ where less = filterV (Proxy::(Proxy FMin))
111+ more = filterV (Proxy::(Proxy FMax))
112+
113+{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
114+class FilterV (f::Flag) k v xs where
115+ filterV :: Proxy f -> Var k -> v -> Map xs -> Map (Filter f (k :-> v) xs)
116+
117+instance FilterV f k v '[] where
118+ filterV _ k v Empty = Empty
119+
120+instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
121+ 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)
123+
124+instance (Conder (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ)), FilterV FMax k v xs) => FilterV FMax k v (x ': xs) where
125+ 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)
127+
128+class Combinable t t' where
129+ combine :: t -> t' -> Combine t t'
130+
131+class Nubable t where
132+ nub :: Map t -> Map (Nub t)
133+
134+instance Nubable '[] where
135+ nub Empty = Empty
136+
137+instance Nubable '[e] where
138+ nub (Ext k v Empty) = Ext k v Empty
139+
140+instance {-# OVERLAPPING #-}
141+ (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where
142+ nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)
143+
144+instance {-# OVERLAPPING #-}
145+ (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
146+ Nubable (f ': s)) => Nubable (e ': f ': s) where
147+ nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
148+
149+class Conder g where
150+ cond :: Proxy g -> Map s -> Map t -> Map (If g s t)
151+
152+instance Conder True where
153+ cond _ s t = s
154+
155+instance Conder False where
156+ cond _ s t = t
157+