3cca261 · type-level-sets

git.iko.soy/type-level-sets

on master help sign in

added EQ instances

3cca261dominic10 years ago

src/Data/Type/Map.hs+7−1

compare with master

unifiedsplit

@@ -98,6 +98,12 @@ instance Show' (Map '[]) where

98instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s)) where

99 show' (Ext k v s) = ", " ++ show k ++ " :-> " ++ show v ++ (show' s)

100

101+instance Eq (Map '[]) where

102+ Empty == Empty = True

103+

104+instance (KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where

105+ (Ext k v m) == (Ext k' v' m') = k == k' && v == v' && m == m'

106+

101{-| Union of two finite maps -}

107{-| Union of two finite maps -}

102union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)

108union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)

103union s t = nub (quicksort (append s t))

109union s t = nub (quicksort (append s t))

@@ -151,7 +157,7 @@ instance Nubable '[] where

151instance Nubable '[e] where

157instance Nubable '[e] where

152 nub (Ext k v Empty) = Ext k v Empty

158 nub (Ext k v Empty) = Ext k v Empty

153

159

154−instance {-# OVERLAPABLE #-}

160+instance {-# OVERLAPPABLE #-}

155 (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),

161 (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),

156 Nubable (f ': s)) => Nubable (e ': f ': s) where

162 Nubable (f ': s)) => Nubable (e ': f ': s) where

157 nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))

163 nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))

src/Data/Type/Set.hs+4

@@ -34,6 +34,10 @@ instance Show' (Set '[]) where

34instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where

35 show' (Ext e s) = ", " ++ show e ++ (show' s)

37+instance (Eq e, Eq (Set s)) => Eq (Set (e ': s)) where

38+ (Ext e m) == (Ext e' m') = e == e' && m == m'

39+

40+

37{-| At the type level, normalise the list form to the set form -}

41{-| At the type level, normalise the list form to the set form -}

38type AsSet s = Nub (Sort s)

42type AsSet s = Nub (Sort s)

stack.yaml+1−1

@@ -1,7 +1,7 @@

1# For more information, see: https://github.com/commercialhaskell/stack/wiki/stack.yaml

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: nightly-2016-07-18

6# Local packages, usually specified by relative directory name

7packages:

type-level-sets.cabal+21−16

@@ -1,5 +1,5 @@

1name: type-level-sets

2−version: 0.7

2+version: 0.8.0.0

3synopsis: Type-level sets and finite maps (with value-level counterparts)

4description:

5 This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level

@@ -8,32 +8,37 @@ description:

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.

10 .

11− Here is a brief example for finite maps.:

11+ Here is a brief example for finite maps:

12 .

13 >

14 > import Data.Type.Map

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

@@ -64,9 +69,9 @@ maintainer: 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.10.3

72+tested-with: GHC >= 8.0.1

69−extra-source-files: example.hs

74+extra-source-files: example.hs, example2.hs

72source-repository head

77source-repository head