type-level-sets 0.6.1 → 0.7
raw patch · 5 files changed
+151/−71 lines, 5 filesdep ~base
Dependency ranges changed: base
Files
- example.hs +13/−8
- example2.hs +21/−0
- src/Data/Type/Map.hs +66/−18
- src/Data/Type/Set.hs +28/−27
- type-level-sets.cabal +23/−18
example.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-} import GHC.TypeLits import Data.Type.Map@@ -8,19 +8,24 @@ -- Specify that Int values for matching keys should be added instance Combinable Int Int where combine x y = x + y- -foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]-foo = Ext (Var :: (Var "x")) 2 $- Ext (Var :: (Var "z")) 4 $- Ext (Var :: (Var "w")) 5 $- Empty +foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]+foo = Ext (Var :: (Var "x")) 2+ $ Ext (Var :: (Var "z")) True+ $ Ext (Var :: (Var "w")) 5+ $ Empty +foo' :: Map (AsMap '["z" :-> Bool, "x" :-> Int, "w" :-> Int])+foo' = asMap foo+ bar :: Map '["y" :-> Int, "w" :-> Int] bar = Ext (Var :: (Var "y")) 3 $ Ext (Var :: (Var "w")) 1 $- Empty + Empty -- GHC can easily infer this type, so an explicit signature not necessary -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int] foobar = foo `union` bar++foobarToFoo :: Map '["w" :-> Int, "x" :-> Int, "z" :-> Bool]+foobarToFoo = submap foobar
+ example2.hs view
@@ -0,0 +1,21 @@+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}++import GHC.TypeLits+import Data.Type.Set++type instance Cmp (Natural n) (Natural m) = CmpNat n m++data Natural (a :: Nat) where+ Z :: Natural 0+ S :: Natural n -> Natural (n + 1)++deriving instance Show (Natural n)++-- foo :: Set '[Natural 0, Natural 1, Natural 3]+foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))++-- bar :: Set '[Natural 1, Natural 2]+bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))++-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]+foobar = foo `union` bar
src/Data/Type/Map.hs view
@@ -2,18 +2,22 @@ The implementation is similar to that shown in the paper. "Embedding effect systems in Haskell" Orchard, Petricek 2014 -} -{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures, - TypeFamilies, UndecidableInstances, MultiParamTypeClasses, - FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables, ConstraintKinds #-}+{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,+ TypeFamilies, UndecidableInstances, MultiParamTypeClasses,+ FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables,+ ConstraintKinds #-} -module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..), - Combine, Combinable(..), Cmp, - Lookup, Member, (:\)) where+module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),+ Combine, Combinable(..), Cmp,+ Nubable, nub,+ Lookup, Member, (:\), Split, split,+ IsMap, AsMap, asMap, + Submap, submap) where import GHC.TypeLits import Data.Type.Bool import Data.Type.Equality-import Data.Type.Set hiding (Set(..), Nub,Union,Nubable,Sortable,Unionable,append,union,quicksort,nub)+import Data.Type.Set (Cmp, Proxy(..), Flag(..), Sort, Filter, (:++)) {- Throughout, type variables 'k' ranges over "keys"@@ -22,7 +26,7 @@ 'm', 'n' range over "maps" -} -- Mappings-infixr 4 :-> +infixr 4 :-> {-| A key-value pair -} data Mapping k v = k :-> v @@ -61,7 +65,7 @@ -- Value-level map with a type-level representation {-| Pair a symbol (representing a variable) with a type -}-data Var (k :: Symbol) = Var +data Var (k :: Symbol) = Var instance KnownSymbol k => Show (Var k) where show = symbolVal@@ -71,11 +75,21 @@ Empty :: Map '[] Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m) +{-| Predicate to check if in normalised map form -}+type IsMap s = (s ~ Nub (Sort s))++{-| At the type level, normalise the list form to the map form -}+type AsMap s = Nub (Sort s)++{-| At the value level, noramlise the list form to the map form -}+asMap :: (Sortable s, Nubable (Sort s)) => Map s -> Map (AsMap s)+asMap x = nub (quicksort x)+ instance Show (Map '[]) where show Empty = "{}" instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where- show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}" + show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}" class Show' t where show' :: t -> String@@ -95,7 +109,7 @@ append (Ext k v xs) ys = Ext k v (append xs ys) type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'-type instance Cmp (k :-> v) (k' :-> v) = CmpSymbol k k'+type instance Cmp (k :-> v) (k' :-> v') = CmpSymbol k k' {-| Value-level quick sort that respects the type-level ordering -} class Sortable xs where@@ -119,11 +133,11 @@ instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy ((Cmp x (k :-> v)) == LT)))- (Ext k' v' (filterV f k v xs)) (filterV f k v xs) + (Ext k' v' (filterV f k v xs)) (filterV f k v xs) instance (Conder (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ)), FilterV FMax k v xs) => FilterV FMax k v (x ': xs) where filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ))))- (Ext k' v' (filterV f k v xs)) (filterV f k v xs) + (Ext k' v' (filterV f k v xs)) (filterV f k v xs) class Combinable t t' where combine :: t -> t' -> Combine t t'@@ -137,14 +151,15 @@ instance Nubable '[e] where nub (Ext k v Empty) = Ext k v Empty -instance {-# OVERLAPPING #-}+instance {-# OVERLAPPABLE #-}+ (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),+ Nubable (f ': s)) => Nubable (e ': f ': s) where+ nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))++instance {-# OVERLAPS #-} (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s) -instance {-# OVERLAPPING #-}- (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), - Nubable (f ': s)) => Nubable (e ': f ': s) where- nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s)) class Conder g where cond :: Proxy g -> Map s -> Map t -> Map (If g s t)@@ -155,3 +170,36 @@ instance Conder False where cond _ s t = t ++{-| Splitting a union of maps, given the maps we want to split it into -}+class Split s t st where+ -- where st ~ Union s t+ split :: Map st -> (Map s, Map t)++instance Split '[] '[] '[] where+ split Empty = (Empty, Empty)++instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where+ split (Ext k v st) = let (s, t) = split st+ in (Ext k v s, Ext k v t)++instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where+ split (Ext k v st) = let (s, t) = split st+ in (Ext k v s, t)++instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where+ split (Ext k v st) = let (s, t) = split st+ in (s, Ext k v t)++{-| Construct a submap 's' from a supermap 't' -}+class Submap s t where+ submap :: Map t -> Map s++instance Submap '[] '[] where+ submap xs = Empty++instance {-# OVERLAPPABLE #-} Submap s t => Submap s (x ': t) where+ submap (Ext _ _ xs) = submap xs++instance {-# OVERLAPS #-} Submap s t => Submap (x ': s) (x ': t) where+ submap (Ext k v xs) = Ext k v (submap xs)
src/Data/Type/Set.hs view
@@ -1,10 +1,12 @@-{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, - MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,- UndecidableInstances, ConstraintKinds, ScopedTypeVariables #-}+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,+ MultiParamTypeClasses, FlexibleInstances, PolyKinds,+ FlexibleContexts, UndecidableInstances, ConstraintKinds,+ ScopedTypeVariables #-} -module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, - Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..), - Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..), Delete(..), Proxy(..)) where+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,+ Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),+ Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),+ Delete(..), Proxy(..)) where import GHC.TypeLits import Data.Type.Bool@@ -12,10 +14,10 @@ data Proxy (p :: k) = Proxy --- Value-level 'Set' representation, essentially a list +-- Value-level 'Set' representation, essentially a list data Set (n :: [*]) where {--| Construct an empty set -}- Empty :: Set '[] + Empty :: Set '[] {--| Extend a set with an element -} Ext :: e -> Set s -> Set (e ': s) @@ -23,7 +25,7 @@ show Empty = "{}" instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where- show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}" + show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}" class Show' t where show' :: t -> String@@ -43,8 +45,8 @@ type IsSet s = (s ~ Nub (Sort s)) {-| Useful properties to be able to refer to someties -}-type SetProperties f = (Union f '[] ~ f, Split f '[] f, - Union '[] f ~ f, Split '[] f f, +type SetProperties f = (Union f '[] ~ f, Split f '[] f,+ Union '[] f ~ f, Split '[] f f, Union f f ~ f, Split f f f, Unionable f '[], Unionable '[] f) @@ -70,22 +72,22 @@ {-| Splitting a union a set, given the sets we want to split it into -} class Split s t st where -- where st ~ Union s t- split :: Set st -> (Set s, Set t) + split :: Set st -> (Set s, Set t) instance Split '[] '[] '[] where split Empty = (Empty, Empty) -instance Split s t st => Split (x ': s) (x ': t) (x ': st) where+instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where split (Ext x st) = let (s, t) = split st in (Ext x s, Ext x t) -instance Split s t st => Split (x ': s) t (x ': st) where+instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where split (Ext x st) = let (s, t) = split st- in (Ext x s, t) + in (Ext x s, t) -instance (Split s t st) => Split s (x ': t) (x ': st) where+instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where split (Ext x st) = let (s, t) = split st- in (s, Ext x t) + in (s, Ext x t) @@ -97,7 +99,7 @@ Nub (e ': f ': s) = e ': Nub (f ': s) {-| Value-level counterpart to the type-level 'Nub'- Note: the value-level case for equal types is not define here, + Note: the value-level case for equal types is not define here, but should be given per-application, e.g., custom 'merging' behaviour may be required -} class Nubable t where@@ -112,7 +114,7 @@ instance Nubable (e ': s) => Nubable (e ': e ': s) where nub (Ext _ (Ext e s)) = nub (Ext e s) -instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), +instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), Nubable (f ': s)) => Nubable (e ': f ': s) where nub (Ext e (Ext f s)) = Ext e (nub (Ext f s)) @@ -121,11 +123,11 @@ class Subset s t where subset :: Set t -> Set s -instance Subset '[] '[] where +instance Subset '[] '[] where subset xs = Empty -instance Subset '[] (x ': t) where - subset xs = Empty+instance Subset s t => Subset s (x ': t) where+ subset (Ext _ xs) = subset xs instance Subset s t => Subset (x ': s) (x ': t) where subset (Ext x xs) = Ext x (subset xs)@@ -140,8 +142,8 @@ type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where Filter f p '[] = '[]- Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs) - Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs) + Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs)+ Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs) type family DeleteFromList (e :: elem) (list :: [elem]) where DeleteFromList elem '[] = '[]@@ -174,11 +176,11 @@ instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))- (Ext x (filterV f p xs)) (filterV f p xs) + (Ext x (filterV f p xs)) (filterV f p xs) instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))- (Ext x (filterV f p xs)) (filterV f p xs) + (Ext x (filterV f p xs)) (filterV f p xs) class Conder g where cond :: Proxy g -> Set s -> Set t -> Set (If g s t)@@ -192,4 +194,3 @@ {-| Open-family for the ordering operation in the sort -} type family Cmp (a :: k) (b :: k) :: Ordering-
type-level-sets.cabal view
@@ -1,39 +1,44 @@ name: type-level-sets-version: 0.6.1+version: 0.7 synopsis: Type-level sets and finite maps (with value-level counterparts) description: This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level finite maps via 'Map', with value-level counterparts. . Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard - 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.+ 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. .- Here is a brief example for finite maps.: + Here is a brief example for finite maps: . > > import Data.Type.Map >- > foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]- > foo = Ext ((Var :: (Var "x")) :-> 2) $- > Ext ((Var :: (Var "z")) :-> 4) $- > Ext ((Var :: (Var "w")) :-> 5) $- > Empty + > -- Specify how to combine duplicate key-value pairs for Int values+ > type instance Combine Int Int = Int+ > instance Combinable Int Int where+ > combine x y = x + y >+ > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]+ > foo = Ext (Var :: (Var "x")) 2 + > $ Ext (Var :: (Var "z")) True + > $ Ext (Var :: (Var "w")) 5 + > $ Empty + > > bar :: Map '["y" :-> Int, "w" :-> Int]- > bar = Ext ((Var :: (Var "y")) :-> 3) $- > Ext ((Var :: (Var "w")) :-> 1) $- > Empty+ > bar = Ext (Var :: (Var "y")) 3+ > $ Ext (Var :: (Var "w")) 1+ > $ Empty > - > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]+ > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool] > foobar = foo `union` bar .- The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).+ The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates). The type signatures is commented out as it can be infered. Running the example we get: . > >>> foobar - > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]+ > {w :-> 6, x :-> 2, y :-> 3, z :-> True} .- Thus, we see that the first value paired with the \"w\" variable is dropped.+ Thus, we see that the values for \"w\" are added together. For sets, here is an example: . > import GHC.TypeLits@@ -64,9 +69,9 @@ stability: experimental build-type: Simple cabal-version: >= 1.6-tested-with: GHC == 7.8.2+tested-with: GHC == 7.10.3 -extra-source-files: example.hs+extra-source-files: example.hs, example2.hs source-repository head@@ -80,5 +85,5 @@ exposed-modules: Data.Type.Set Data.Type.Map - build-depends: base >= 4.7.0.0 && < 5,+ build-depends: base < 5, ghc-prim