git.iko.soy/type-level-sets
on master help sign in
swap
e36892722 ahead, 0 behind
README+42−21
since splitsnapshots
unifiedsplit
@@ -1,35 +1,56 @@
1−This library provides type-level sets to Haskell, with a value level counterpart, and operations for taking the union, computing
1+This library provides type-level sets and finite maps to Haskell, with a value level counterpart, and operations for taking the union, computing
2−subsets, and split sets. Also included is a "mapping" type constructor that pairs symbols with types. This can be used to represent
2+subsets/submaps, and splitting sets/maps. This library was originally built based on
3−sets of variable-type pairs, which is used in the paper "Embedding effect systems in Haskell" (Dominic Orchard,
3+"Embedding effect systems in Haskell" (Dominic Orchard,
4Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.
4Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.
5
5
6The following shows an example:
6The following shows an example:
7
7
8− {-# LANGUAGE DataKinds, TypeOperators #-}
8+ {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}
9+ import Data.Type.Map
10+
11+ -- Specifies how to combine duplicate key-value pairs for Int values
12+ type instance Combine Int Int = Int
13+ instance Combinable Int Int where
14+ combine x y = x + y
15+
16+ foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
17+ foo = Ext (Var :: (Var "x")) 2
18+ $ Ext (Var :: (Var "z")) True
19+ $ Ext (Var :: (Var "w")) 5
20+ Empty
21+
22+ bar :: Map '["y" :-> Int, "w" :-> Int]
23+ bar = Ext (Var :: (Var "y")) 3
24+ $ Ext (Var :: (Var "w")) 1
25+ $ Empty
26+
27+ -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
28+ foobar = foo `union` bar
29+
30+The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
31+The type signatures is commented out as it can be infered. Running the example we get:
9
32
10− import Data.Type.Set
33+ *Main> foobar
34+ {w :-> 6, x :-> 2, y :-> 3, z :-> True}
11
35
12− foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
36+Thus, we see that values for 'w' are added.
13− foo = Ext ((Var :: (Var "x")) :-> 2) $
14− Ext ((Var :: (Var "z")) :-> 4) $
15− Ext ((Var :: (Var "w")) :-> 5) $
16− Empty
17
37
18− bar :: Set '["y" :-> Int, "w" :-> Int]
38+ import GHC.TypeLits
19− bar = Ext ((Var :: (Var "y")) :-> 3) $
39+ import Data.Type.Set
20− Ext ((Var :: (Var "w")) :-> 1) $
40+ type instance Cmp (Natural n) (Natural m) = CmpNat n m
21− Empty
22
41
23− -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
42+ data Natural (a :: Nat) where
24− foobar = foo `union` bar
43+ Z :: Natural 0
44+ S :: Natural n -> Natural (n + 1)
25
45
26−The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
46+ -- foo :: Set '[Natural 0, Natural 1, Natural 3]
27−The type signatures is commented out as it can be infered. Running the example we get:
47+ foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
28
48
29− *Main> foobar
49+ -- bar :: Set '[Natural 1, Natural 2]
30− {(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)}
50+ bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
31
51
32−Thus, we see that the first value paired with the "w" variable is dropped.
52+ -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
53+ foobar = foo `union` bar
33
54
34
55
35
56
TySet.hsdeleted−355
@@ -1,355 +0,0 @@
1−-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
2−{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators, FlexibleInstances, ScopedTypeVariables, ImplicitParams, MultiParamTypeClasses #-}
3−
4−module TySet(plugin, Set, Union, dropPrefix, ppr) where
5−
6−import TypeRep
7−import Type
8−import Kind
9−import TcEvidence
10−import CoAxiom
11−import Name
12−import OccName
13−import Var
14−import TyCon
15−import BasicTypes
16−
17−-- friends:
18−import Var
19−import VarEnv
20−import VarSet
21−import Name
22−import BasicTypes
23−import TyCon
24−import Class
25−import CoAxiom
26−
27−-- others
28−import PrelNames
29−import Outputable
30−import FastString
31−import Util
32−import DynFlags
33−
34−import TcPluginM ( TcPluginM, tcPluginIO, tcPluginTrace )
35−import TcRnMonad ( TcPlugin(..), TcPluginResult(..)
36− , Ct(..), CtEvidence(..), CtLoc, ctLoc, ctPred
37− , mkNonCanonical, isTouchableTcM, unsafeTcPluginTcM)
38−import Plugins ( CommandLineOption, defaultPlugin, Plugin(..) )
39−import GHC.TcPluginM.Extra
40−
41−import Debug.Trace
42−import Outputable
43−import DynFlags
44−
45−import Control.Monad
46−import Control.Monad.Trans.Maybe
47−import Control.Applicative
48−import qualified Data.Typeable as DT
49−import Data.List
50−
51−import Test.QuickCheck
52−import Test.QuickCheck.Property
53−
54−{- Set constructor -}
55−data Set (a :: [k])
56−{- Union operation -}
57−type family Union (a :: [k]) (b :: [k]) :: [k]
58−
59−type family Member (a :: k) (b :: [k]) :: Bool where
60− Member x '[] = False
61− Member x (x ': xs) = True
62− Member x (y ': xs) = Member x xs
63−
64−{- Plugin setup -}
65−plugin :: Plugin
66−plugin = defaultPlugin { tcPlugin = Just . thePlugin }
67−
68−thePlugin :: [CommandLineOption] -> TcPlugin
69−thePlugin opts = TcPlugin
70− { tcPluginInit = pluginInit opts
71− , tcPluginSolve = pluginSolve
72− , tcPluginStop = pluginStop
73− }
74−
75−class Debug t m where
76− debug :: (?ifDebug :: Bool) => t -> m ()
77−instance Debug SDoc TcPluginM where
78− debug x = tcPluginTrace "TySet" x
79−instance Debug String IO where
80− debug x = putStrLn x
81−
82−pluginInit :: [CommandLineOption] -> TcPluginM ()
83−pluginInit _ = return ()
84−
85−printerS = let ?ifDebug = True in tcPluginIO . debug . showSDocUnsafe . ppCts
86−printer = let ?ifDebug = True in tcPluginIO . debug
87−
88−pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
89−pluginSolve () given derived wanted =
90− let ?ifDebug = True in
91−
92− do tcPluginIO $ debug "*****************************"
93− tcPluginIO $ debug "Running TySet equality plugin"
94− --debug $ ppCts wanted
95− tcPluginIO $ debug $ showSDocUnsafe $ ppCts wanted
96− tcPluginIO $ debug "Givens"
97− --debug $ ppCts given
98− tcPluginIO $ debug $ showSDocUnsafe $ ppCts given
99− tcPluginIO $ debug "Derived"
100− -- debug $ ppCts derived
101− tcPluginIO $ debug $ showSDocUnsafe $ ppCts derived
102− -- debug $ ppr $ head $ wanted
103−
104− --solved <- findEmptySetEquality wanted
105− (solved, generated) <- findSetEquality wanted
106− printer "Done - solved"
107− printerS (map snd solved)
108− printer "DOne - generated"
109− printerS generated
110−
111− return $ TcPluginOk solved generated
112−
113−pluginStop :: () -> TcPluginM ()
114−pluginStop _ = return ()
115−
116−-- Pretty print constraints
117−ppCts [] = text "(empty)"
118−ppCts cs = vcat (map ppr cs)
119−
120−{- Some debugging Show instances to help me understand what is coming in and out of GHC -}
121−deriving instance Show TyLit
122−deriving instance Show Type
123−instance Show Var where
124− show v = showSDocUnsafe $ ppr v
125−instance Show TyCon where
126− show tycon = showSDocUnsafe $ ppr tycon
127−instance Show Ct where
128− show ct = showSDocUnsafe $ ppr ct
129−
130−{-
131−-- Prediacate one whether a type is = Set '[]
132−isEmptySetType t = do (x, tcs) <- splitTyConApp_maybe t
133− guard $ length tcs == 2
134− guard $ getOccString (tyConName x) == "Set"
135− case tcs of [TyVarTy k, TyConApp con [TyVarTy k']] ->
136− do guard $ k == k'
137− guard $ (getOccString . tyConName $ con) == "[]"
138− _ -> Nothing
139−-}
140−
141−getNameStr = getOccString . tyConName
142−
143−liftTc :: Maybe a -> MaybeT TcPluginM a
144−liftTc = MaybeT . return
145−
146−liftMt :: TcPluginM a -> MaybeT TcPluginM a
147−liftMt x = MaybeT (fmap Just x)
148−
149−findSetEquality :: [Ct] -> TcPluginM ([(EvTerm, Ct)], [Ct])
150−findSetEquality [] = return ([], [])
151−findSetEquality (ct : xs) =
152− do x <- runMaybeT $
153− do (Nominal, t1, t2) <- liftTc $ getEqPredTys_maybe (ctPred ct)
154− a <- liftTc $ listTypeToTerm t1
155− b <- "sofar sogood" `trace` liftTc $ listTypeToTerm t2
156− (show (t1, a, t2, b)) `trace`
157− if (a == b) then
158− "are equal" `trace` return $ Left (EvCoercion $ TcRefl Nominal t1, ct)
159− else -- not equal, try to find an mgu and generate conditions on that
160− let ?ctLoc = ctLoc ct in
161− do unifiers <- "not equal" `trace` mgu a b
162− case unifiers of
163− Left unifiers -> ("L unifiers: \n" ++ show unifiers) `trace` return $ Right []
164− Right (dataUnifiers, unsolvedExtra) -> ("data unifiers:" ++ (show $ dataUnifiers)) `trace` return $ Right $ (EvCoercion $ TcRefl Nominal t1, ct) : map (\c -> (EvCoercion $ TcRefl Nominal undefined, c)) dataUnifiers
165−
166− (solved, generated) <- findSetEquality xs
167− case x of
168− Just y -> case y of
169− Left (ev, ct) -> return $ ((ev, ct) : solved, generated)
170− Right cts -> return $ (solved ++ cts, generated)
171− Nothing -> return (solved, generated)
172−
173−listTypeToTerm :: Type -> Maybe (TermTree Type)
174−listTypeToTerm t = case (splitTyConApp_maybe t) of
175− Just (tcon, args) ->
176− case getNameStr tcon of
177− "Union" -> do guard $ (length args) >= 3
178− (_ : (t1 : (t2 : ts))) <- return args
179− t1' <- listTypeToTerm t1
180− t2' <- listTypeToTerm t2
181− return $ Union t1' t2'
182− -- this case is probably temporary [see SessionListE.hs]
183− ":++" -> do guard $ (length args) >= 3
184− (_ : (t1 : (t2 : ts))) <- return args
185− t1' <- listTypeToTerm t1
186− t2' <- listTypeToTerm t2
187− return $ Union t1' t2'
188− ":" -> do guard $ (length args >= 2)
189− (t1 : (t2 : ts)) <- return args
190− (kind, args) <- splitTyConApp_maybe $ t1
191− ts' <- listTypeToTerm $ head ts -- possible bug here
192− return $ Union (Data [t2]) ts'
193− "[]" -> do guard $ (length args == 1)
194− [t] <- return args
195− (kind, args) <- splitTyConApp_maybe $ t
196− return $ Empty
197−
198− _ -> return $ Empty -- Data [t]
199− _ -> case t of
200− TyVarTy v -> return $ Var $ v
201−
202−-- Representation for solving equalities on terms comprising union, data, and variables
203−
204−data TermTree a = Union (TermTree a) (TermTree a) | Empty | Var Var | Data [a] deriving Show
205−
206−-- if the second argument is a prefix of the first argument, then return Just of the suffix, else Nothing
207−dropPrefix :: Eq a => [a] -> [a] -> Maybe [a]
208−dropPrefix [] xs = Just []
209−dropPrefix xs [] = Just xs
210−dropPrefix (x:xs) (y:ys) | x == y = dropPrefix xs ys
211− | otherwise = Nothing
212−
213−mguDataVars :: [a] -> [Var] -> Maybe [(Var, TermTree a)]
214−mguDataVars suffix [] = Nothing -- No variables to unify with
215−mguDataVars suffix (v:vs) = Just $ [(v, Data suffix)] ++ map (\v' -> (v', Var v)) vs
216−
217−mgu :: (?ctLoc :: CtLoc) => TermTree Type -> TermTree Type -> MaybeT TcPluginM (Either [(Var, TermTree Type)] ([Ct], ([Type], [Type]))) -- last component should be some equalities
218−mgu t1 t2 = let (vs1, ds1) = normalisedRep t1
219− (vs2, ds2) = normalisedRep t2
220− in ("----> " ++ show (ds1, ds2)) `trace`
221− (show $ dropPrefix ds1 ds2) `trace`
222− case (dropPrefix ds1 ds2) of
223− Nothing -> case (dropPrefix ds2 ds1) of
224− Nothing -> "el zilcho primo" `trace` do x <- liftMt (zipMatch ds1 ds2)
225− return $ Right x -- ([], ([], []))
226− Just suffix_ds2 -> "suffix_ds2" `trace`
227− do x <- liftTc $ mguDataVars suffix_ds2 vs1
228− return $ Left x
229− Just suffix_ds1 -> ("suffix_ds1 " ++ (show suffix_ds1))
230− `trace`
231− if (suffix_ds1 == []) then
232− do x <- liftMt (zipMatch ds1 ds2)
233− ("zipm: ds1 = " ++ (show ds1) ++ " ds2 = " ++ (show ds2) ++ ": " ++ (show x)) `trace` return $ Right x -- ([], ([], []))
234− else
235− do x <- liftTc $ mguDataVars suffix_ds1 vs2
236− return $ Left x
237−
238−mkEqualities :: (?ctLoc :: CtLoc) => [(Type, Type)] -> TcPluginM [Ct]
239−mkEqualities xs = (mapM (\(x, y) -> mkCt x y) xs) -- >>= (return . concat)
240−
241−mkCt t t' = fmap mkNonCanonical (newDerived ?ctLoc (uncurry mkPrimEqPred (t,t')))
242−
243−mkEqualities' (AppTy t1 t2) (AppTy t1' t2') = do ct <- mkCt t1 t1'
244− ct' <- mkCt t2 t2'
245− return [ct, ct']
246−mkEqualities' (TyConApp con kt) (TyConApp con' kt') | con == con' = mapM (uncurry mkCt) (zip kt kt')
247−mkEqualities' (FunTy t1 t2) (FunTy t1' t2') = do ct <- mkCt t1 t1'
248− ct' <- mkCt t2 t2'
249− return [ct, ct']
250−mkEqualities' (ForAllTy v t) (ForAllTy v' t') | v == v' = do ct <- mkCt t t'
251− return [ct]
252−mkEqualities' t t' = do ct <- mkCt t t'
253− return [ct]
254−
255−
256−
257−
258−zipMatch :: (?ctLoc :: CtLoc) => [Type] -> [Type] -> TcPluginM ([Ct], ([Type], [Type]))
259−zipMatch xs ys = let (unifiers, restL, restR) = zipMatch' xs ys
260− in do unifiers' <- mkEqualities unifiers
261− return $ (unifiers', (restL, restR))
262−
263−zipMatch' :: [a] -> [a] -> ([(a, a)], [a], [a])
264−zipMatch' [] xs = ([], [], xs)
265−zipMatch' xs [] = ([], xs, [])
266−zipMatch' (x:xs) (y:ys) = let (zips, l, r) = zipMatch' xs ys
267− in ((x, y) : zips, l, r)
268−
269−
270−
271−
272−
273−
274−subst :: TermTree a -> [(Var, TermTree a)] -> TermTree a
275−subst (Union s t) theta = Union (subst s theta) (subst t theta)
276−subst (Var a) theta = case (lookup a theta) of
277− Just t -> t
278− Nothing -> Var a
279−subst t theta = t
280−
281−instance Eq a => Eq (TermTree a) where
282− t1 == t2 = let (vs1, ds1) = normalisedRep t1
283− (vs2, ds2) = normalisedRep t2
284− in ("vars = " ++ (show (vs1, vs2)) ++ " eq = " ++ (show (vs1 == vs2)))
285− `trace` (vs1 == vs2) && (all (flip elem $ ds2) ds1) && (all (flip elem $ ds1) ds2)
286−
287−normalisedRep :: Eq a => TermTree a -> ([Var], [a])
288−normalisedRep t = let (vs, ds) = separate t
289− in (nub . sort $ vs, nub ds)
290−
291−separate :: TermTree a -> ([Var], [a])
292−separate Empty = ([], [])
293−separate (Var s) = ([s], [])
294−separate (Data xs) = ([], xs)
295−separate (Union a b) = let (vs1, ds1) = separate a
296− (vs2, ds2) = separate b
297− in (vs1++vs2, ds1++ds2)
298−
299−{-- Unit testing of normaliser and set equality --}
300−testSetTermEquality :: IO ()
301−testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> n == m)
302−
303−mkVar :: String -> Var
304−mkVar = undefined
305−
306−instance {-# OVERLAPS #-} Arbitrary (TermTree Int, TermTree Int) where
307− arbitrary = sized $ \vars ->
308− sized $ \datums ->
309− do v0 <- (vector vars)::(Gen [String])
310− v <- return $ map mkVar v0
311− dat <- (vector datums)::(Gen [Int])
312− v' <- shuffle v
313− dat' <- shuffle dat
314− g1 <- gen v dat
315− g2 <- gen v' dat'
316−
317− -- Soundness check on generated tree
318− let (v0, dat0) = separate g1
319− (v1, dat1) = separate g2
320− norm :: (Ord a) => [a] -> [a]
321− norm = nub . sort
322−
323− if and [(norm v0) == (norm v), (norm v1) == (norm v),
324− (norm dat) == (norm dat0), (norm dat) == (norm dat1)]
325− then return ()
326− else error $ "Generated trees failed soundness check: " ++ (show g1) ++ " " ++ (show g2)
327− return (g1, g2)
328−
329−-- Arbitrarily permute a union of two generators
330−unionPerm x y = do x' <- x
331− y' <- y
332− elements [Union x' y', Union y' x']
333−
334−-- Generates arbitrary terms from a list of variables and list of Int adtums
335−gen :: [Var] -> [Int] -> Gen (TermTree Int)
336−gen [] [] = return $ Empty
337−gen vs ds = do -- Choose between 0 and 1 if 'vs' is empty, or 0-2 if 'vs' has elements
338− choose <- suchThat arbitrary (\x -> x<=(2 - if vs == [] then 1 else 0) && x>=0)
339− case choose::Int of
340− -- Union with Empty
341− 0 -> unionPerm (gen vs ds) (return $ Empty)
342−
343− -- Pick some number of elements (maybe none) and create a data leaf
344− 1 -> do i <- suchThat arbitrary (<= (length ds))
345− unionPerm (gen vs (drop i ds)) (return $ Data (take i ds))
346−
347− -- Case where vs is non-empty, create a variable node, and either remove that
348− -- variable, or keep it around as a possibility again to test idempotency
349− 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),
350− unionPerm (gen vs ds) (return $ Var (head vs))]
351− _ -> error "unpossible"
352−
353−
354−
355−
changelog.mdnew file+5
@@ -0,0 +1,5 @@
1+ # v0.8.9.0
2+
3+ - GHC 8.4 and 8.6 support.
4+ - Fixed bug in the delete operation.
5+ - Non-membership predicates
example-new.hsdeleted−61
@@ -1,61 +0,0 @@
1−{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, TypeFamilies, PolyKinds, EmptyDataDecls #-}
2−
3−{-# OPTIONS_GHC -fplugin=TyMap #-}
4−import TyMap
5−
6−import GHC.TypeLits
7−
8−
9−data Proxy (s :: Map * (Session *)) = Proxy
10−
11−data Container (a :: *) where
12− Empty :: Container (Set '[])
13− Ext :: a -> Container (Set s) -> Container (Set (Union '[a] s))
14− ExtP :: Proxy a -> Container (Set s) -> Container (Set (Union '[a] s))
15−
16−data Natural (a :: Nat) where
17− Z :: Natural 0
18− S :: Natural n -> Natural (n + 1)
19−
20−-- Should be typeable with the plugin
21−foo :: Container (Set '[Natural 1, Natural 2, Natural 3])
22−foo = Ext (S $ S Z) (Ext (S Z) (Ext (S $ S $ S Z) Empty))
23−
24−
25−
26−
27−
28−
29−
30−
31−
32−
33−
34−
35−
36−
37−
38−
39−
40−
41−
42−
43−
44−
45−
46−infixr 4 :->
47−data Map a b = a :-> b
48−
49−data X
50−data Y
51−
52−mkA :: Proxy (Y :-> A)
53−mkA = Proxy
54−
55−mkB :: Proxy (X :-> B)
56−mkB = Proxy
57−
58−data Session a = A | B | C a
59−
60−bar :: Container (Set '[Y :-> A, X :-> B])
61−bar = ExtP mkB (ExtP mkA Empty)
example-set.hsdeleted−39
@@ -1,39 +0,0 @@
1−{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, TypeFamilies, PolyKinds, EmptyDataDecls, StandaloneDeriving #-}
2−{-# OPTIONS_GHC -fplugin=TySet #-}
3−
4−import GHC.TypeLits
5−import TySet
6−
7−data Container (a :: *) where
8− Empty :: Container (Set '[])
9− Ext :: Show a => a -> Container (Set s) -> Container (Set (Union '[a] s))
10−
11−instance Show (Container a) where
12− show Empty = "Empty"
13− show (Ext x xs) = "Ext " ++ show x ++ " " ++ show xs
14−
15−data Natural (a :: Nat) where
16− Z :: Natural 0
17− S :: Natural n -> Natural (n + 1)
18−
19−instance Show (Natural a) where
20− show Z = "Z"
21− show (S n) = "S " ++ (show n)
22−
23−-- Should be typeable with the plugin
24−
25−foo :: Container (Set '[Natural 3, Natural 2, Natural 1])
26−foo = Ext (S $ S Z) (Ext (S Z) (Ext (S $ S $ S Z) Empty))
27−
28−foo2 :: Container (Set '[Natural 2, Natural 1])
29−foo2 = Ext (S $ S Z) (Ext (S Z) Empty)
30−
31−bar :: (Container (Set '[Natural 2, Natural 1])) -> Container (Set '[Natural 1])
32−bar (Ext (S (S Z)) (Ext (S Z) Empty)) = Ext (S Z) Empty
33−bar (Ext (S Z) (Ext (S (S Z)) Empty)) = Ext (S Z) Empty
34−
35−{-
36−dup :: Container (Set s) -> Container (Set (Union s s))
37−dup Empty = Empty
38−dup (Ext x xs) = Ext x (Ext x (dup xs))
39−-}
example.hs+12−11
@@ -1,7 +1,6 @@
1−{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}
1+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}
2
2
3import GHC.TypeLits
3import GHC.TypeLits
4−import Data.Type.Set (subset)
5import Data.Type.Map
4import Data.Type.Map
6
5
7-- Specify that key-value pairs on Ints combine to an Int
6-- Specify that key-value pairs on Ints combine to an Int
@@ -9,22 +8,24 @@ type instance Combine Int Int = Int
9-- Specify that Int values for matching keys should be added
8-- Specify that Int values for matching keys should be added
10instance Combinable Int Int where
9instance Combinable Int Int where
11 combine x y = x + y
10 combine x y = x + y
12−
13−foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]
14−foo = Ext (Var :: (Var "x")) 2 $
15− Ext (Var :: (Var "z")) 4 $
16− Ext (Var :: (Var "w")) 5 $
17− Empty
18
11
12+foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
13+foo = Ext (Var :: (Var "x")) 2
14+ $ Ext (Var :: (Var "z")) True
15+ $ Ext (Var :: (Var "w")) 5
16+ $ Empty
17+
18+foo' :: Map (AsMap '["z" :-> Bool, "x" :-> Int, "w" :-> Int])
19+foo' = asMap foo
19
20
20bar :: Map '["y" :-> Int, "w" :-> Int]
21bar :: Map '["y" :-> Int, "w" :-> Int]
21bar = Ext (Var :: (Var "y")) 3 $
22bar = Ext (Var :: (Var "y")) 3 $
22 Ext (Var :: (Var "w")) 1 $
23 Ext (Var :: (Var "w")) 1 $
23− Empty
24+ Empty
24
25
25-- GHC can easily infer this type, so an explicit signature not necessary
26-- GHC can easily infer this type, so an explicit signature not necessary
26-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
27-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
27foobar = foo `union` bar
28foobar = foo `union` bar
28
29
29−foobarToFoo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]
30+foobarToFoo :: Map '["w" :-> Int, "x" :-> Int, "z" :-> Bool]
30−foobarToFoo = subset foobar
31+foobarToFoo = submap foobar
example2.hs+9
@@ -1,4 +1,5 @@
1{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}
1{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}
2+{-# LANGUAGE FlexibleContexts #-}
2
3
3import GHC.TypeLits
4import GHC.TypeLits
4import Data.Type.Set
5import Data.Type.Set
@@ -19,3 +20,11 @@ bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
19
20
20-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
21-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
21foobar = foo `union` bar
22foobar = foo `union` bar
23+
24+nonMemberTest :: NonMember (Natural 0) as => Set as -> ()
25+nonMemberTest set = ()
26+
27+-- nonMemberTest meep is well typed
28+meep = asSet $ Ext (S Z) (Ext (S (S Z)) Empty)
29+-- nonMemberTest morp is ill typed
30+morp = asSet $ Ext (S Z) (Ext (S (S Z)) (Ext Z Empty))
src/Data/Type/Map.hs+139−35
@@ -2,18 +2,23 @@
2The implementation is similar to that shown in the paper.
2The implementation is similar to that shown in the paper.
3 "Embedding effect systems in Haskell" Orchard, Petricek 2014 -}
3 "Embedding effect systems in Haskell" Orchard, Petricek 2014 -}
4
4
5−{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,
5+{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,
6− TypeFamilies, UndecidableInstances, MultiParamTypeClasses,
6+ TypeFamilies, UndecidableInstances, MultiParamTypeClasses,
7− FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables, ConstraintKinds #-}
7+ FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables,
8−
8+ ConstraintKinds, IncoherentInstances #-}
9+
9−module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
10+module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
10− Combine, Combinable(..), Cmp,
11+ Combine, Combinable(..), Cmp,
12+ Nubable, nub,
11− Lookup, Member, (:\)) where
13+ Lookup, Member, (:\), Split, split,
14+ IsMember, lookp, Updatable, update,
15+ IsMap, AsMap, asMap,
16+ Submap, submap) where
12
17
13import GHC.TypeLits
18import GHC.TypeLits
14import Data.Type.Bool
19import Data.Type.Bool
15import Data.Type.Equality
20import Data.Type.Equality
16−import Data.Type.Set hiding (Set(..), Nub,Union,Nubable,Sortable,Unionable,append,union,quicksort,nub)
21+import Data.Type.Set (Cmp, Proxy(..), Flag(..), Sort, Filter, (:++))
17
22
18{- Throughout, type variables
23{- Throughout, type variables
19 'k' ranges over "keys"
24 'k' ranges over "keys"
@@ -22,7 +27,7 @@ import Data.Type.Set hiding (Set(..), Nub,Union,Nubable,Sortable,Unionable,appen
22 'm', 'n' range over "maps" -}
27 'm', 'n' range over "maps" -}
23
28
24-- Mappings
29-- Mappings
25−infixr 4 :->
30+infixr 4 :->
26{-| A key-value pair -}
31{-| A key-value pair -}
27data Mapping k v = k :-> v
32data Mapping k v = k :-> v
28
33
@@ -41,17 +46,17 @@ type family Combine (a :: v) (b :: v) :: v
41
46
42{-| Delete elements from a map by key -}
47{-| Delete elements from a map by key -}
43type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
48type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
44− '[] :\ k = '[]
49+ '[] :\ k = '[]
45− ((k :-> v) ': m) :\ k = m :\ k
50+ ((k :-> v) ': m) :\ k = m :\ k
46− (kvp ': m) :\ k = kvp ': (m :\ k)
51+ (kvp ': m) :\ k = kvp ': (m :\ k)
47
52
48−{-| Lookup elements from a map -}
53+{-| Type-level lookup of elements from a map -}
49type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
54type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
50 Lookup '[] k = Nothing
55 Lookup '[] k = Nothing
51 Lookup ((k :-> v) ': m) k = Just v
56 Lookup ((k :-> v) ': m) k = Just v
52 Lookup (kvp ': m) k = Lookup m k
57 Lookup (kvp ': m) k = Lookup m k
53
58
54−{-| Membership test -}
59+{-| Membership test as type function -}
55type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
60type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
56 Member k '[] = False
61 Member k '[] = False
57 Member k ((k :-> v) ': m) = True
62 Member k ((k :-> v) ': m) = True
@@ -61,7 +66,7 @@ type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
61-- Value-level map with a type-level representation
66-- Value-level map with a type-level representation
62
67
63{-| Pair a symbol (representing a variable) with a type -}
68{-| Pair a symbol (representing a variable) with a type -}
64−data Var (k :: Symbol) = Var
69+data Var (k :: Symbol) = Var
65
70
66instance KnownSymbol k => Show (Var k) where
71instance KnownSymbol k => Show (Var k) where
67 show = symbolVal
72 show = symbolVal
@@ -71,11 +76,52 @@ data Map (n :: [Mapping Symbol *]) where
71 Empty :: Map '[]
76 Empty :: Map '[]
72 Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
77 Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
73
78
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+
110+{-| Predicate to check if in normalised map form -}
111+type IsMap s = (s ~ Nub (Sort s))
112+
113+{-| At the type level, normalise the list form to the map form -}
114+type AsMap s = Nub (Sort s)
115+
116+{-| At the value level, noramlise the list form to the map form -}
117+asMap :: (Sortable s, Nubable (Sort s)) => Map s -> Map (AsMap s)
118+asMap x = nub (quicksort x)
119+
74instance Show (Map '[]) where
120instance Show (Map '[]) where
75 show Empty = "{}"
121 show Empty = "{}"
76
122
77instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where
123instance (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) ++ "}"
124+ show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ show' s ++ "}"
79
125
80class Show' t where
126class Show' t where
81 show' :: t -> String
127 show' :: t -> String
@@ -84,18 +130,31 @@ instance Show' (Map '[]) where
84instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s)) where
130instance (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)
131 show' (Ext k v s) = ", " ++ show k ++ " :-> " ++ show v ++ (show' s)
86
132
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+
87−{-| Union of two finite maps -}
145+{-| Union of two finite maps (normalising) -}
88union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
146union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
89union s t = nub (quicksort (append s t))
147union s t = nub (quicksort (append s t))
90
148
91type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
149type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
92
150
151+{-| Append of two finite maps (non normalising) -}
93append :: Map s -> Map t -> Map (s :++ t)
152append :: Map s -> Map t -> Map (s :++ t)
94append Empty x = x
153append Empty x = x
95append (Ext k v xs) ys = Ext k v (append xs ys)
154append (Ext k v xs) ys = Ext k v (append xs ys)
96
155
97type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'
156type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'
98−type instance Cmp (k :-> v) (k' :-> v) = CmpSymbol k k'
157+type instance Cmp (k :-> v) (k' :-> v') = CmpSymbol k k'
99
158
100{-| Value-level quick sort that respects the type-level ordering -}
159{-| Value-level quick sort that respects the type-level ordering -}
101class Sortable xs where
160class Sortable xs where
@@ -104,11 +163,15 @@ class Sortable xs where
104instance Sortable '[] where
163instance Sortable '[] where
105 quicksort Empty = Empty
164 quicksort Empty = Empty
106
165
107−instance (Sortable (Filter FMin (k :-> v) xs),
166+instance (Sortable (Filter FMin (k :-> v) xs)
167+ , Sortable (Filter FMax (k :-> v) xs)
168+ , FilterV 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
169+ , FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
170+ quicksort (Ext k v xs) =
109− quicksort (Ext k v xs) = ((quicksort (less k v xs)) `append` (Ext k v Empty)) `append` (quicksort (more k v xs))
171+ quicksort (less k v xs) `append` Ext k v Empty `append` quicksort (more k v xs)
172+ where
110− where less = filterV (Proxy::(Proxy FMin))
173+ less = filterV (Proxy::(Proxy FMin))
111− more = filterV (Proxy::(Proxy FMax))
174+ more = filterV (Proxy::(Proxy FMax))
112
175
113{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
176{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
114class FilterV (f::Flag) k v xs where
177class FilterV (f::Flag) k v xs where
@@ -117,13 +180,19 @@ class FilterV (f::Flag) k v xs where
117instance FilterV f k v '[] where
180instance FilterV f k v '[] where
118 filterV _ k v Empty = Empty
181 filterV _ k v Empty = Empty
119
182
120−instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
183+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)))
184+ filterV f@Proxy k v (Ext k' v' xs) =
185+ cond (Proxy::(Proxy (Cmp x (k :-> v) == LT)))
122− (Ext k' v' (filterV f k v xs)) (filterV f k v xs)
186+ (Ext k' v' (filterV f k v xs))
187+ (filterV f k v xs)
123
188
189+instance
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
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) =
125− filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ))))
193+ 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)
194+ (Ext k' v' (filterV f k v xs))
195+ (filterV f k v xs)
127
196
128class Combinable t t' where
197class Combinable t t' where
129 combine :: t -> t' -> Combine t t'
198 combine :: t -> t' -> Combine t t'
@@ -137,15 +206,17 @@ instance Nubable '[] where
137instance Nubable '[e] where
206instance Nubable '[e] where
138 nub (Ext k v Empty) = Ext k v Empty
207 nub (Ext k v Empty) = Ext k v Empty
139
208
140−instance {-# OVERLAPPING #-}
209+instance {-# OVERLAPPABLE #-}
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)),
210+ (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
146 Nubable (f ': s)) => Nubable (e ': f ': s) where
211 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))
212 nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
148
213
214+instance {-# OVERLAPS #-}
215+ (Combinable v v', Nubable ((k :-> Combine v v') ': s))
216+ => Nubable ((k :-> v) ': (k :-> v') ': s) where
217+ nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)
218+
219+
149class Conder g where
220class Conder g where
150 cond :: Proxy g -> Map s -> Map t -> Map (If g s t)
221 cond :: Proxy g -> Map s -> Map t -> Map (If g s t)
151
222
@@ -155,3 +226,36 @@ instance Conder True where
155instance Conder False where
226instance Conder False where
156 cond _ s t = t
227 cond _ s t = t
157
228
229+
230+{-| Splitting a union of maps, given the maps we want to split it into -}
231+class Split s t st where
232+ -- where st ~ Union s t
233+ split :: Map st -> (Map s, Map t)
234+
235+instance Split '[] '[] '[] where
236+ split Empty = (Empty, Empty)
237+
238+instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where
239+ split (Ext k v st) = let (s, t) = split st
240+ in (Ext k v s, Ext k v t)
241+
242+instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where
243+ split (Ext k v st) = let (s, t) = split st
244+ in (Ext k v s, t)
245+
246+instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
247+ split (Ext k v st) = let (s, t) = split st
248+ in (s, Ext k v t)
249+
250+{-| Construct a submap 's' from a supermap 't' -}
251+class Submap s t where
252+ submap :: Map t -> Map s
253+
254+instance Submap '[] '[] where
255+ submap xs = Empty
256+
257+instance {-# OVERLAPPABLE #-} Submap s t => Submap s (x ': t) where
258+ submap (Ext _ _ xs) = submap xs
259+
260+instance {-# OVERLAPS #-} Submap s t => Submap (x ': s) (x ': t) where
261+ submap (Ext k v xs) = Ext k v (submap xs)
src/Data/Type/Set.hs+70−29
@@ -1,10 +1,13 @@
1−{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
1+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
2− MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
2+ MultiParamTypeClasses, FlexibleInstances, PolyKinds,
3− UndecidableInstances, ConstraintKinds, ScopedTypeVariables #-}
3+ FlexibleContexts, UndecidableInstances, ConstraintKinds,
4+ ScopedTypeVariables, TypeInType #-}
4
5
5−module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
6+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
6− Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
7+ Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
7− Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..), Delete(..), Proxy(..)) where
8+ Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9+ Delete(..), Proxy(..), remove, Remove, (:\),
10+ Member(..), NonMember, MemberP(..)) where
8
11
9import GHC.TypeLits
12import GHC.TypeLits
10import Data.Type.Bool
13import Data.Type.Bool
@@ -12,10 +15,10 @@ import Data.Type.Equality
12
15
13data Proxy (p :: k) = Proxy
16data Proxy (p :: k) = Proxy
14
17
15−-- Value-level 'Set' representation, essentially a list
18+-- Value-level 'Set' representation, essentially a list
16−data Set (n :: [*]) where
19+data Set (n :: [k]) where
17 {--| Construct an empty set -}
20 {--| Construct an empty set -}
18− Empty :: Set '[]
21+ Empty :: Set '[]
19 {--| Extend a set with an element -}
22 {--| Extend a set with an element -}
20 Ext :: e -> Set s -> Set (e ': s)
23 Ext :: e -> Set s -> Set (e ': s)
21
24
@@ -23,7 +26,7 @@ instance Show (Set '[]) where
23 show Empty = "{}"
26 show Empty = "{}"
24
27
25instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
28instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
26− show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
29+ show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
27
30
28class Show' t where
31class Show' t where
29 show' :: t -> String
32 show' :: t -> String
@@ -32,6 +35,10 @@ instance Show' (Set '[]) where
32instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
35instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
33 show' (Ext e s) = ", " ++ show e ++ (show' s)
36 show' (Ext e s) = ", " ++ show e ++ (show' s)
34
37
38+instance (Eq e, Eq (Set s)) => Eq (Set (e ': s)) where
39+ (Ext e m) == (Ext e' m') = e == e' && m == m'
40+
41+
35{-| At the type level, normalise the list form to the set form -}
42{-| At the type level, normalise the list form to the set form -}
36type AsSet s = Nub (Sort s)
43type AsSet s = Nub (Sort s)
37
44
@@ -43,8 +50,8 @@ asSet x = nub (quicksort x)
43type IsSet s = (s ~ Nub (Sort s))
50type IsSet s = (s ~ Nub (Sort s))
44
51
45{-| Useful properties to be able to refer to someties -}
52{-| Useful properties to be able to refer to someties -}
46−type SetProperties f = (Union f '[] ~ f, Split f '[] f,
53+type SetProperties f = (Union f '[] ~ f, Split f '[] f,
47− Union '[] f ~ f, Split '[] f f,
54+ Union '[] f ~ f, Split '[] f f,
48 Union f f ~ f, Split f f f,
55 Union f f ~ f, Split f f f,
49 Unionable f '[], Unionable '[] f)
56 Unionable f '[], Unionable '[] f)
50
57
@@ -67,27 +74,44 @@ append :: Set s -> Set t -> Set (s :++ t)
67append Empty x = x
74append Empty x = x
68append (Ext e xs) ys = Ext e (append xs ys)
75append (Ext e xs) ys = Ext e (append xs ys)
69
76
77+{-| Delete elements from a set -}
78+type family (m :: [k]) :\ (x :: k) :: [k] where
79+ '[] :\ x = '[]
80+ (x ': xs) :\ x = xs :\ x
81+ (y ': xs) :\ x = y ': (xs :\ x)
82+
83+class Remove s t where
84+ remove :: Set s -> Proxy t -> Set (s :\ t)
85+
86+instance Remove '[] t where
87+ remove Empty Proxy = Empty
88+
89+instance {-# OVERLAPS #-} Remove xs x => Remove (x ': xs) x where
90+ remove (Ext _ xs) x@Proxy = remove xs x
91+
92+instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
93+ => Remove (y ': xs) x where
94+ remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
95+
70{-| Splitting a union a set, given the sets we want to split it into -}
96{-| Splitting a union a set, given the sets we want to split it into -}
71class Split s t st where
97class Split s t st where
72 -- where st ~ Union s t
98 -- where st ~ Union s t
73− split :: Set st -> (Set s, Set t)
99+ split :: Set st -> (Set s, Set t)
74
100
75instance Split '[] '[] '[] where
101instance Split '[] '[] '[] where
76 split Empty = (Empty, Empty)
102 split Empty = (Empty, Empty)
77
103
78−instance Split s t st => Split (x ': s) (x ': t) (x ': st) where
104+instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where
79 split (Ext x st) = let (s, t) = split st
105 split (Ext x st) = let (s, t) = split st
80 in (Ext x s, Ext x t)
106 in (Ext x s, Ext x t)
81
107
82−instance Split s t st => Split (x ': s) t (x ': st) where
108+instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where
83 split (Ext x st) = let (s, t) = split st
109 split (Ext x st) = let (s, t) = split st
84− in (Ext x s, t)
110+ in (Ext x s, t)
85
111
86−instance (Split s t st) => Split s (x ': t) (x ': st) where
112+instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
87 split (Ext x st) = let (s, t) = split st
113 split (Ext x st) = let (s, t) = split st
88− in (s, Ext x t)
114+ in (s, Ext x t)
89−
90−
91
115
92{-| Remove duplicates from a sorted list -}
116{-| Remove duplicates from a sorted list -}
93type family Nub t where
117type family Nub t where
@@ -97,7 +121,7 @@ type family Nub t where
97 Nub (e ': f ': s) = e ': Nub (f ': s)
121 Nub (e ': f ': s) = e ': Nub (f ': s)
98
122
99{-| Value-level counterpart to the type-level 'Nub'
123{-| Value-level counterpart to the type-level 'Nub'
100− Note: the value-level case for equal types is not define here,
124+ Note: the value-level case for equal types is not define here,
101 but should be given per-application, e.g., custom 'merging' behaviour may be required -}
125 but should be given per-application, e.g., custom 'merging' behaviour may be required -}
102
126
103class Nubable t where
127class Nubable t where
@@ -112,7 +136,7 @@ instance Nubable '[e] where
112instance Nubable (e ': s) => Nubable (e ': e ': s) where
136instance Nubable (e ': s) => Nubable (e ': e ': s) where
113 nub (Ext _ (Ext e s)) = nub (Ext e s)
137 nub (Ext _ (Ext e s)) = nub (Ext e s)
114
138
115−instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
139+instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
116 Nubable (f ': s)) => Nubable (e ': f ': s) where
140 Nubable (f ': s)) => Nubable (e ': f ': s) where
117 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
141 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
118
142
@@ -121,13 +145,13 @@ instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
121class Subset s t where
145class Subset s t where
122 subset :: Set t -> Set s
146 subset :: Set t -> Set s
123
147
124−instance Subset '[] '[] where
148+instance Subset '[] '[] where
125 subset xs = Empty
149 subset xs = Empty
126
150
127−instance Subset s t => Subset s (x ': t) where
151+instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
128 subset (Ext _ xs) = subset xs
152 subset (Ext _ xs) = subset xs
129
153
130−instance Subset s t => Subset (x ': s) (x ': t) where
154+instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
131 subset (Ext x xs) = Ext x (subset xs)
155 subset (Ext x xs) = Ext x (subset xs)
132
156
133
157
@@ -140,8 +164,8 @@ data Flag = FMin | FMax
140
164
141type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
165type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
142 Filter f p '[] = '[]
166 Filter f p '[] = '[]
143− Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs)
167+ Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs)
144− Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs)
168+ Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs)
145
169
146type family DeleteFromList (e :: elem) (list :: [elem]) where
170type family DeleteFromList (e :: elem) (list :: [elem]) where
147 DeleteFromList elem '[] = '[]
171 DeleteFromList elem '[] = '[]
@@ -174,11 +198,11 @@ instance FilterV f p '[] where
174
198
175instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
199instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
176 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))
200 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))
177− (Ext x (filterV f p xs)) (filterV f p xs)
201+ (Ext x (filterV f p xs)) (filterV f p xs)
178
202
179instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
203instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
180 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))
204 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))
181− (Ext x (filterV f p xs)) (filterV f p xs)
205+ (Ext x (filterV f p xs)) (filterV f p xs)
182
206
183class Conder g where
207class Conder g where
184 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
208 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
@@ -193,3 +217,20 @@ instance Conder False where
193
217
194type family Cmp (a :: k) (b :: k) :: Ordering
218type family Cmp (a :: k) (b :: k) :: Ordering
195
219
220+{-| Membership of an element in a set, with an acommanying
221+ value-level function that returns a bool -}
222+class Member a s where
223+ member :: Proxy a -> Set s -> Bool
224+
225+instance {-# OVERLAPS #-} Member a (a ': s) where
226+ member _ (Ext x _) = True
227+
228+instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where
229+ member a (Ext _ xs) = member a xs
230+
231+type family MemberP a s :: Bool where
232+ MemberP a '[] = False
233+ MemberP a (a ': s) = True
234+ MemberP a (b ': s) = MemberP a s
235+
236+type NonMember a s = MemberP a s ~ False
stack.yaml+1−1
@@ -1,7 +1,7 @@
1# For more information, see: https://github.com/commercialhaskell/stack/wiki/stack.yaml
1# For more information, see: https://github.com/commercialhaskell/stack/wiki/stack.yaml
2
2
3# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
3# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
4−resolver: lts-3.5
4+resolver: lts-12.7
5
5
6# Local packages, usually specified by relative directory name
6# Local packages, usually specified by relative directory name
7packages:
7packages:
type-level-sets.cabal+31−25
@@ -1,39 +1,44 @@
1name: type-level-sets
1name: type-level-sets
2−version: 0.6.1
2+version: 0.8.9.0
3synopsis: Type-level sets and finite maps (with value-level counterparts)
3synopsis: Type-level sets and finite maps (with value-level counterparts)
4−description:
4+description:
5 This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
5 This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
6 finite maps via 'Map', with value-level counterparts.
6 finite maps via 'Map', with value-level counterparts.
7 .
7 .
8− Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard
8+ Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard
9 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.
9 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.
10 .
10 .
11− Here is a brief example for finite maps.:
11+ Here is a brief example for finite maps:
12 .
12 .
13 >
13 >
14 > import Data.Type.Map
14 > import Data.Type.Map
15 >
15 >
16+ > -- Specify how to combine duplicate key-value pairs for Int values
17+ > type instance Combine Int Int = Int
18+ > instance Combinable Int Int where
19+ > combine x y = x + y
20+ >
16− > foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]
21+ > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
17− > foo = Ext ((Var :: (Var "x")) :-> 2) $
22+ > foo = Ext (Var :: (Var "x")) 2
18− > Ext ((Var :: (Var "z")) :-> 4) $
23+ > $ Ext (Var :: (Var "z")) True
19− > Ext ((Var :: (Var "w")) :-> 5) $
24+ > $ Ext (Var :: (Var "w")) 5
20− > Empty
25+ > $ Empty
21 >
26 >
22 > bar :: Map '["y" :-> Int, "w" :-> Int]
27 > bar :: Map '["y" :-> Int, "w" :-> Int]
23− > bar = Ext ((Var :: (Var "y")) :-> 3) $
28+ > bar = Ext (Var :: (Var "y")) 3
24− > Ext ((Var :: (Var "w")) :-> 1) $
29+ > $ Ext (Var :: (Var "w")) 1
25− > Empty
30+ > $ Empty
26− >
31+ >
27− > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
32+ > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
28 > foobar = foo `union` bar
33 > foobar = foo `union` bar
29 .
34 .
30− The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
35+ The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
31 The type signatures is commented out as it can be infered. Running the example we get:
36 The type signatures is commented out as it can be infered. Running the example we get:
32 .
37 .
33− > >>> foobar
38+ > >>> foobar
34− > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]
39+ > {w :-> 6, x :-> 2, y :-> 3, z :-> True}
35 .
40 .
36− Thus, we see that the first value paired with the \"w\" variable is dropped.
41+ Thus, we see that the values for \"w\" are added together.
37 For sets, here is an example:
42 For sets, here is an example:
38 .
43 .
39 > import GHC.TypeLits
44 > import GHC.TypeLits
@@ -43,7 +48,7 @@ description:
43 > data Natural (a :: Nat) where
48 > data Natural (a :: Nat) where
44 > Z :: Natural 0
49 > Z :: Natural 0
45 > S :: Natural n -> Natural (n + 1)
50 > S :: Natural n -> Natural (n + 1)
46− >
51+ >
47 > -- foo :: Set '[Natural 0, Natural 1, Natural 3]
52 > -- foo :: Set '[Natural 0, Natural 1, Natural 3]
48 > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
53 > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
49 >
54 >
@@ -58,15 +63,15 @@ description:
58license: BSD3
63license: BSD3
59license-file: LICENSE
64license-file: LICENSE
60category: Type System, Data Structures
65category: Type System, Data Structures
61−copyright: 2013-16 University of Cambridge
66+copyright: 2013-18 University of Kent
62author: Dominic Orchard
67author: Dominic Orchard
63maintainer: Dominic Orchard
68maintainer: Dominic Orchard
64stability: experimental
69stability: experimental
65build-type: Simple
70build-type: Simple
66cabal-version: >= 1.6
71cabal-version: >= 1.6
67−tested-with: GHC == 7.8.2
72+tested-with: GHC >= 8.2.2
68
73
69−extra-source-files: example.hs
74+extra-source-files: example.hs, example2.hs, changelog.md
70
75
71
76
72source-repository head
77source-repository head
@@ -75,10 +80,11 @@ source-repository head
75
80
76library
81library
77 hs-source-dirs: src
82 hs-source-dirs: src
83+ other-extensions: TypeInType
78
84
79
85
80 exposed-modules: Data.Type.Set
86 exposed-modules: Data.Type.Set
81 Data.Type.Map
87 Data.Type.Map
82−
88+
83− build-depends: base >= 4.7.0.0 && < 5,
89+ build-depends: base < 5,
84− ghc-prim
90+ ghc-prim