git.iko.soy/type-level-sets
on master help sign in
swap
e36892726 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−344
@@ -1,344 +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) 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−pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
86−pluginSolve () given derived wanted =
87− let ?ifDebug = True in
88−
89− do
90− tcPluginIO $ debug "Running TySet equality plugin"
91− debug $ ppCts wanted
92− -- debug $ ppr $ head $ wanted
93−
94− --solved <- findEmptySetEquality wanted
95− (solved, generated) <- findSetEquality wanted
96− return $ TcPluginOk solved generated
97−
98−pluginStop :: () -> TcPluginM ()
99−pluginStop _ = return ()
100−
101−-- Pretty print constraints
102−ppCts [] = text "(empty)"
103−ppCts cs = vcat (map ppr cs)
104−
105−{- Some debugging Show instances to help me understand what is coming in and out of GHC -}
106−deriving instance Show TyLit
107−deriving instance Show Type
108−instance Show Var where
109− show v = showSDocUnsafe $ ppr v
110−instance Show TyCon where
111− show tycon = showSDocUnsafe $ ppr tycon
112−instance Show Ct where
113− show ct = showSDocUnsafe $ ppr ct
114−
115−{-
116−-- Prediacate one whether a type is = Set '[]
117−isEmptySetType t = do (x, tcs) <- splitTyConApp_maybe t
118− guard $ length tcs == 2
119− guard $ getOccString (tyConName x) == "Set"
120− case tcs of [TyVarTy k, TyConApp con [TyVarTy k']] ->
121− do guard $ k == k'
122− guard $ (getOccString . tyConName $ con) == "[]"
123− _ -> Nothing
124−-}
125−
126−getNameStr = getOccString . tyConName
127−
128−liftTc :: Maybe a -> MaybeT TcPluginM a
129−liftTc = MaybeT . return
130−
131−liftMt :: TcPluginM a -> MaybeT TcPluginM a
132−liftMt x = MaybeT (fmap Just x)
133−
134−findSetEquality :: [Ct] -> TcPluginM ([(EvTerm, Ct)], [Ct])
135−findSetEquality [] = return ([], [])
136−findSetEquality (ct : xs) =
137− do x <- runMaybeT $
138− do (Nominal, t1, t2) <- liftTc $ getEqPredTys_maybe (ctPred ct)
139− a <- liftTc $ listTypeToTerm t1
140− b <- "sofar sogood" `trace` liftTc $ listTypeToTerm t2
141− (show (t1, a, t2, b)) `trace`
142− if (a == b) then
143− "are equal" `trace` return $ Left (EvCoercion $ TcRefl Nominal t1, ct)
144− else -- not equal, try to find an mgu and generate conditions on that
145− let ?ctLoc = ctLoc ct in
146− do unifiers <- "not equal" `trace` mgu a b
147− case unifiers of
148− Left unifiers -> ("L unifiers: \n" ++ show unifiers) `trace` return $ Right []
149− Right (dataUnifiers, unsolvedExtra) -> ("data unifiers:" ++ (show $ dataUnifiers)) `trace` return $ Right $ (EvCoercion $ TcRefl Nominal t1, ct) : map (\c -> (EvCoercion $ TcRefl Nominal undefined, c)) dataUnifiers
150−
151− (solved, generated) <- findSetEquality xs
152− case x of
153− Just y -> case y of
154− Left (ev, ct) -> return $ ((ev, ct) : solved, generated)
155− Right cts -> return $ (solved ++ cts, generated)
156− Nothing -> return (solved, generated)
157−
158−listTypeToTerm :: Type -> Maybe (TermTree Type)
159−listTypeToTerm t = case (splitTyConApp_maybe t) of
160− Just (tcon, args) ->
161− case getNameStr tcon of
162− "Union" -> do guard $ (length args) >= 3
163− (_ : (t1 : (t2 : ts))) <- return args
164− t1' <- listTypeToTerm t1
165− t2' <- listTypeToTerm t2
166− return $ Union t1' t2'
167− -- this case is probably temporary [see SessionListE.hs]
168− ":++" -> do guard $ (length args) >= 3
169− (_ : (t1 : (t2 : ts))) <- return args
170− t1' <- listTypeToTerm t1
171− t2' <- listTypeToTerm t2
172− return $ Union t1' t2'
173− ":" -> do guard $ (length args >= 2)
174− (t1 : (t2 : ts)) <- return args
175− (kind, args) <- splitTyConApp_maybe $ t1
176− ts' <- listTypeToTerm $ head ts -- possible bug here
177− return $ Union (Data [t2]) ts'
178− "[]" -> do guard $ (length args == 1)
179− [t] <- return args
180− (kind, args) <- splitTyConApp_maybe $ t
181− return $ Empty
182−
183− _ -> return $ Empty -- Data [t]
184− _ -> case t of
185− TyVarTy v -> return $ Var $ v
186−
187−-- Representation for solving equalities on terms comprising union, data, and variables
188−
189−data TermTree a = Union (TermTree a) (TermTree a) | Empty | Var Var | Data [a] deriving Show
190−
191−-- if the second argument is a prefix of the first argument, then return Just of the suffix, else Nothing
192−dropPrefix :: Eq a => [a] -> [a] -> Maybe [a]
193−dropPrefix [] xs = Just []
194−dropPrefix xs [] = Just xs
195−dropPrefix (x:xs) (y:ys) | x == y = dropPrefix xs ys
196− | otherwise = Nothing
197−
198−mguDataVars :: [a] -> [Var] -> Maybe [(Var, TermTree a)]
199−mguDataVars suffix [] = Nothing -- No variables to unify with
200−mguDataVars suffix (v:vs) = Just $ [(v, Data suffix)] ++ map (\v' -> (v', Var v)) vs
201−
202−mgu :: (?ctLoc :: CtLoc) => TermTree Type -> TermTree Type -> MaybeT TcPluginM (Either [(Var, TermTree Type)] ([Ct], ([Type], [Type]))) -- last component should be some equalities
203−mgu t1 t2 = let (vs1, ds1) = normalisedRep t1
204− (vs2, ds2) = normalisedRep t2
205− in ("----> " ++ show (ds1, ds2)) `trace`
206− (show $ dropPrefix ds1 ds2) `trace`
207− case (dropPrefix ds1 ds2) of
208− Nothing -> case (dropPrefix ds2 ds1) of
209− Nothing -> "el zilcho primo" `trace` do x <- liftMt (zipMatch ds1 ds2)
210− return $ Right x -- ([], ([], []))
211− Just suffix_ds2 -> "suffix_ds2" `trace`
212− do x <- liftTc $ mguDataVars suffix_ds2 vs1
213− return $ Left x
214− Just suffix_ds1 -> ("suffix_ds1 " ++ (show suffix_ds1))
215− `trace`
216− if (suffix_ds1 == []) then
217− do x <- liftMt (zipMatch ds1 ds2)
218− ("zipm: ds1 = " ++ (show ds1) ++ " ds2 = " ++ (show ds2) ++ ": " ++ (show x)) `trace` return $ Right x -- ([], ([], []))
219− else
220− do x <- liftTc $ mguDataVars suffix_ds1 vs2
221− return $ Left x
222−
223−mkEqualities :: (?ctLoc :: CtLoc) => [(Type, Type)] -> TcPluginM [Ct]
224−mkEqualities xs = (mapM (\(x, y) -> mkCt x y) xs) -- >>= (return . concat)
225−
226−mkCt t t' = fmap mkNonCanonical (newDerived ?ctLoc (uncurry mkPrimEqPred (t,t')))
227−
228−mkEqualities' (AppTy t1 t2) (AppTy t1' t2') = do ct <- mkCt t1 t1'
229− ct' <- mkCt t2 t2'
230− return [ct, ct']
231−mkEqualities' (TyConApp con kt) (TyConApp con' kt') | con == con' = mapM (uncurry mkCt) (zip kt kt')
232−mkEqualities' (FunTy t1 t2) (FunTy t1' t2') = do ct <- mkCt t1 t1'
233− ct' <- mkCt t2 t2'
234− return [ct, ct']
235−mkEqualities' (ForAllTy v t) (ForAllTy v' t') | v == v' = do ct <- mkCt t t'
236− return [ct]
237−mkEqualities' t t' = do ct <- mkCt t t'
238− return [ct]
239−
240−
241−
242−
243−zipMatch :: (?ctLoc :: CtLoc) => [Type] -> [Type] -> TcPluginM ([Ct], ([Type], [Type]))
244−zipMatch xs ys = let (unifiers, restL, restR) = zipMatch' xs ys
245− in do unifiers' <- mkEqualities unifiers
246− return $ (unifiers', (restL, restR))
247−
248−zipMatch' :: [a] -> [a] -> ([(a, a)], [a], [a])
249−zipMatch' [] xs = ([], [], xs)
250−zipMatch' xs [] = ([], xs, [])
251−zipMatch' (x:xs) (y:ys) = let (zips, l, r) = zipMatch' xs ys
252− in ((x, y) : zips, l, r)
253−
254−
255−
256−
257−
258−
259−subst :: TermTree a -> [(Var, TermTree a)] -> TermTree a
260−subst (Union s t) theta = Union (subst s theta) (subst t theta)
261−subst (Var a) theta = case (lookup a theta) of
262− Just t -> t
263− Nothing -> Var a
264−subst t theta = t
265−
266−instance Eq a => Eq (TermTree a) where
267− t1 == t2 = let (vs1, ds1) = normalisedRep t1
268− (vs2, ds2) = normalisedRep t2
269− in ("vars = " ++ (show (vs1, vs2)) ++ " eq = " ++ (show (vs1 == vs2)))
270− `trace` (vs1 == vs2) && (all (flip elem $ ds2) ds1) && (all (flip elem $ ds1) ds2)
271−
272−normalisedRep :: Eq a => TermTree a -> ([Var], [a])
273−normalisedRep t = let (vs, ds) = separate t
274− in (nub . sort $ vs, nub ds)
275−
276−separate :: TermTree a -> ([Var], [a])
277−separate Empty = ([], [])
278−separate (Var s) = ([s], [])
279−separate (Data xs) = ([], xs)
280−separate (Union a b) = let (vs1, ds1) = separate a
281− (vs2, ds2) = separate b
282− in (vs1++vs2, ds1++ds2)
283−
284−{-- Unit testing of normaliser and set equality --}
285−testSetTermEquality :: IO ()
286−testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> n == m)
287−
288−mkVar :: String -> Var
289−mkVar = undefined
290−
291−instance Arbitrary (TermTree Int, TermTree Int) where
292− arbitrary = sized $ \vars ->
293− sized $ \datums ->
294− do v0 <- (vector vars)::(Gen [String])
295− v <- return $ map mkVar v0
296− dat <- (vector datums)::(Gen [Int])
297− v' <- shuffle v
298− dat' <- shuffle dat
299− g1 <- gen v dat
300− g2 <- gen v' dat'
301−
302− -- Soundness check on generated tree
303− let (v0, dat0) = separate g1
304− (v1, dat1) = separate g2
305− norm :: (Ord a) => [a] -> [a]
306− norm = nub . sort
307−
308− if and [(norm v0) == (norm v), (norm v1) == (norm v),
309− (norm dat) == (norm dat0), (norm dat) == (norm dat1)]
310− then return ()
311− else error $ "Generated trees failed soundness check: " ++ (show g1) ++ " " ++ (show g2)
312− return (g1, g2)
313−
314−-- Arbitrarily permute a union of two generators
315−unionPerm x y = do x' <- x
316− y' <- y
317− elements [Union x' y', Union y' x']
318−
319−-- Generates arbitrary terms from a list of variables and list of Int adtums
320−gen :: [Var] -> [Int] -> Gen (TermTree Int)
321−gen [] [] = return $ Empty
322−gen vs ds = do -- Choose between 0 and 1 if 'vs' is empty, or 0-2 if 'vs' has elements
323− choose <- suchThat arbitrary (\x -> x<=(2 - if vs == [] then 1 else 0) && x>=0)
324− case choose::Int of
325− -- Union with Empty
326− 0 -> unionPerm (gen vs ds) (return $ Empty)
327−
328− -- Pick some number of elements (maybe none) and create a data leaf
329− 1 -> do i <- suchThat arbitrary (<= (length ds))
330− unionPerm (gen vs (drop i ds)) (return $ Data (take i ds))
331−
332− -- Case where vs is non-empty, create a variable node, and either remove that
333− -- variable, or keep it around as a possibility again to test idempotency
334− 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),
335− unionPerm (gen vs ds) (return $ Var (head vs))]
336− _ -> error "unpossible"
337−
338−
339−
340−
341−
342−
343−
344−
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−86
@@ -1,86 +0,0 @@
1−{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, TypeFamilies, PolyKinds, EmptyDataDecls #-}
2−
3−{-# OPTIONS_GHC -fplugin=TyMap #-}
4−import TyMap
5−
6−
7−
8−
9−
10−
11−
12−
13−
14−
15−
16−
17−
18−
19−
20−
21−
22−
23−
24−
25−
26−
27−
28−
29−
30−
31−import GHC.TypeLits
32−
33−
34−data Proxy (s :: Map * (Session *)) = Proxy
35−
36−data Container (a :: *) where
37− Empty :: Container (Set '[])
38− Ext :: a -> Container (Set s) -> Container (Set (Union '[a] s))
39− ExtP :: Proxy a -> Container (Set s) -> Container (Set (Union '[a] s))
40−
41−data Natural (a :: Nat) where
42− Z :: Natural 0
43− S :: Natural n -> Natural (n + 1)
44−
45−-- Should be typeable with the plugin
46−foo :: Container (Set '[Natural 1, Natural 2, Natural 3])
47−foo = Ext (S $ S Z) (Ext (S Z) (Ext (S $ S $ S Z) Empty))
48−
49−
50−
51−
52−
53−
54−
55−
56−
57−
58−
59−
60−
61−
62−
63−
64−
65−
66−
67−
68−
69−
70−
71−infixr 4 :->
72−data Map a b = a :-> b
73−
74−data X
75−data Y
76−
77−mkA :: Proxy (Y :-> A)
78−mkA = Proxy
79−
80−mkB :: Proxy (X :-> B)
81−mkB = Proxy
82−
83−data Session a = A | B | C a
84−
85−bar :: Container (Set '[Y :-> A, X :-> B])
86−bar = ExtP mkB (ExtP mkA Empty)
example.hs+13−8
@@ -1,4 +1,4 @@
1−{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}
1+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}
2
2
3import GHC.TypeLits
3import GHC.TypeLits
4import Data.Type.Map
4import Data.Type.Map
@@ -8,19 +8,24 @@ type instance Combine Int Int = Int
8-- Specify that Int values for matching keys should be added
8-- Specify that Int values for matching keys should be added
9instance Combinable Int Int where
9instance Combinable Int Int where
10 combine x y = x + y
10 combine x y = x + y
11−
12−foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]
13−foo = Ext (Var :: (Var "x")) 2 $
14− Ext (Var :: (Var "z")) 4 $
15− Ext (Var :: (Var "w")) 5 $
16− Empty
17
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
18
20
19bar :: Map '["y" :-> Int, "w" :-> Int]
21bar :: Map '["y" :-> Int, "w" :-> Int]
20bar = Ext (Var :: (Var "y")) 3 $
22bar = Ext (Var :: (Var "y")) 3 $
21 Ext (Var :: (Var "w")) 1 $
23 Ext (Var :: (Var "w")) 1 $
22− Empty
24+ Empty
23
25
24-- 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
25-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
27-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
26foobar = foo `union` bar
28foobar = foo `union` bar
29+
30+foobarToFoo :: Map '["w" :-> Int, "x" :-> Int, "z" :-> Bool]
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