README · type-level-sets

git.iko.soy/type-level-sets

56 lines 2.0 kB history raw

1This library provides type-level sets and finite maps to Haskell, with a value level counterpart, and operations for taking the union, computing

2subsets/submaps, and splitting sets/maps. This library was originally built based on

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.

6The following shows an example:

8 {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}

9 import Data.Type.Map

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

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

22 bar :: Map '["y" :-> Int, "w" :-> Int]

23 bar = Ext (Var :: (Var "y")) 3

24 $ Ext (Var :: (Var "w")) 1

25 $ Empty

27 -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]

28 foobar = foo `union` bar

30The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).

31The type signatures is commented out as it can be infered. Running the example we get:

33 *Main> foobar

34 {w :-> 6, x :-> 2, y :-> 3, z :-> True}

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

38 import GHC.TypeLits

39 import Data.Type.Set

40 type instance Cmp (Natural n) (Natural m) = CmpNat n m

42 data Natural (a :: Nat) where

43 Z :: Natural 0

44 S :: Natural n -> Natural (n + 1)

46 -- foo :: Set '[Natural 0, Natural 1, Natural 3]

47 foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))

49 -- bar :: Set '[Natural 1, Natural 2]

50 bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))

52 -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]

53 foobar = foo `union` bar