Type-level sets for Haskell (with value-level counterparts and various operations)
Go to file
Dominic Orchard e368927a9d
Merge pull request #20 from gwils/prevent-old-ghcs
Prevent bad build plans on older GHCs by expressing dependence on TypeInType
2018-12-20 20:43:00 +00:00
src/Data/Type keep deleting elements from the set 2018-11-29 11:33:16 +00:00
.gitignore Add Delete operation to delete element from Set 2015-09-27 16:23:23 +03:00
changelog.md changelog in the cabal file 2018-11-29 11:46:23 +00:00
example2.hs non membership tests 2018-04-19 14:29:05 +01:00
example.hs readme and examples 2016-09-04 21:27:17 +01:00
LICENSE split off the set representation from the effect monad library (ixmonad) 2014-09-11 14:19:21 +01:00
README readme and examples 2016-09-04 21:27:17 +01:00
Setup.hs split off the set representation from the effect monad library (ixmonad) 2014-09-11 14:19:21 +01:00
stack.yaml Update to compatibility with 8.4 type changes 2018-08-27 10:37:14 +01:00
type-level-sets.cabal Prevent bad build plans on older GHCs by expressing dependence on TypeInType 2018-12-20 15:41:38 +10:00

This library provides type-level sets and finite maps to Haskell, with a value level counterpart, and operations for taking the union, computing
subsets/submaps, and splitting sets/maps. This library was originally built based on
"Embedding effect systems in Haskell" (Dominic Orchard, 
Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets. 

The following shows an example: 

	{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}
        import Data.Type.Map
	
        -- Specifies 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:

	*Main> foobar	
	{w :-> 6, x :-> 2, y :-> 3, z :-> True}

Thus, we see that values for 'w' are added.

 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