type-level-sets 0.7 → 0.8.0.0
raw patch · 3 files changed
+73/−61 lines, 3 files
Files
- src/Data/Type/Map.hs +6/−0
- src/Data/Type/Set.hs +4/−0
- type-level-sets.cabal +63/−61
src/Data/Type/Map.hs view
@@ -98,6 +98,12 @@ 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) +instance Eq (Map '[]) where+ Empty == Empty = True++instance (KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where+ (Ext k v m) == (Ext k' v' m') = k == k' && v == v' && m == m'+ {-| Union of two finite maps -} union :: (Unionable s t) => Map s -> Map t -> Map (Union s t) union s t = nub (quicksort (append s t))
src/Data/Type/Set.hs view
@@ -34,6 +34,10 @@ instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where show' (Ext e s) = ", " ++ show e ++ (show' s) +instance (Eq e, Eq (Set s)) => Eq (Set (e ': s)) where+ (Ext e m) == (Ext e' m') = e == e' && m == m'++ {-| At the type level, normalise the list form to the set form -} type AsSet s = Nub (Sort s)
type-level-sets.cabal view
@@ -1,65 +1,67 @@ name: type-level-sets-version: 0.7+version: 0.8.0.0 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. - .- Here is a brief example for finite maps: - .- >- > import Data.Type.Map- >- > -- 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- > - > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]- > foobar = foo `union` bar- .- 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 - > {w :-> 6, x :-> 2, y :-> 3, z :-> True}- .- Thus, we see that the values for \"w\" are added together. - For sets, here is an example:- .- > 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)- > - > -- 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- .- Note the types here are all inferred.- .+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.+ .+ Here is a brief example for finite maps: + .+ @+ import Data.Type.Map+ .+ -- 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+ . + -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]+ foobar = foo `union` bar+ .+ @+ .+ 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 + > {w :-> 6, x :-> 2, y :-> 3, z :-> True}+ @+ .+ Thus, we see that the values for \"w\" are added together.+ .+ For sets, here is an example:+ .+ @+ 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)+ .+ -- 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+ .+ @+ Note the types here are all inferred. license: BSD3 license-file: LICENSE category: Type System, Data Structures@@ -69,7 +71,7 @@ stability: experimental build-type: Simple cabal-version: >= 1.6-tested-with: GHC == 7.10.3+tested-with: GHC >= 8.0.1 extra-source-files: example.hs, example2.hs