4bfe231..master · type-level-sets

git.iko.soy/type-level-sets

on master help sign in

changelog.mdnew file+5

since splitsnapshots

unifiedsplit

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

1+ # v0.8.9.0

3+ - GHC 8.4 and 8.6 support.

4+ - Fixed bug in the delete operation.

5+ - Non-membership predicates

example2.hs+9

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

1{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}

2+{-# LANGUAGE FlexibleContexts #-}

3import GHC.TypeLits

4import GHC.TypeLits

4import Data.Type.Set

5import Data.Type.Set

@@ -19,3 +20,11 @@ bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))

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

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

21foobar = foo `union` bar

22foobar = foo `union` bar

23+

24+nonMemberTest :: NonMember (Natural 0) as => Set as -> ()

25+nonMemberTest set = ()

26+

27+-- nonMemberTest meep is well typed

28+meep = asSet $ Ext (S Z) (Ext (S (S Z)) Empty)

29+-- nonMemberTest morp is ill typed

30+morp = asSet $ Ext (S Z) (Ext (S (S Z)) (Ext Z Empty))

src/Data/Type/Map.hs+15−5

@@ -84,7 +84,7 @@ class IsMember v t m where

84instance {-# OVERLAPS #-} IsMember v t ((v ':-> t) ': m) where

85 lookp _ (Ext _ x _) = x

87−instance IsMember v t m => IsMember v t (x ': m) where

87+instance {-# OVERLAPPABLE #-} IsMember v t m => IsMember v t (x ': m) where

88 lookp v (Ext _ _ m) = lookp v m

@@ -100,8 +100,12 @@ instance {-# OVERLAPS #-} Updatable v t ((v ':-> s) ': m) ((v ':-> t) ': m) wher

100instance Updatable v t m n => Updatable v t ((w ':-> y) ': m) ((w ':-> y) ': n) where

101 update (Ext w y m) v x = Ext w y (update m v x)

102

103−instance Updatable v t '[] '[v ':-> t] where

103+-- instance Updatable v t '[] '[v ':-> t] where

104+-- update Empty v x = Ext v x Empty

105+

106+instance Updatable v t s ((v ':-> t) ': s) where

104− update Empty v x = Ext v x Empty

107+ update xs v x = Ext v x xs

108+

105

109

106{-| Predicate to check if in normalised map form -}

110{-| Predicate to check if in normalised map form -}

107type IsMap s = (s ~ Nub (Sort s))

111type IsMap s = (s ~ Nub (Sort s))

@@ -129,8 +133,14 @@ instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s))

129instance Eq (Map '[]) where

133instance Eq (Map '[]) where

130 Empty == Empty = True

134 Empty == Empty = True

131

135

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

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

133− (Ext k v m) == (Ext k' v' m') = k == k' && v == v' && m == m'

137+ (Ext Var v m) == (Ext Var v' m') = v == v' && m == m'

138+

139+instance Ord (Map '[]) where

140+ compare Empty Empty = EQ

141+

142+instance (Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) where

143+ compare (Ext Var v m) (Ext Var v' m') = compare v v' `mappend` compare m m'

134

144

135{-| Union of two finite maps (normalising) -}

145{-| Union of two finite maps (normalising) -}

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

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

src/Data/Type/Set.hs+43−7

@@ -1,12 +1,13 @@

1{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,

2 MultiParamTypeClasses, FlexibleInstances, PolyKinds,

3 FlexibleContexts, UndecidableInstances, ConstraintKinds,

4− ScopedTypeVariables #-}

4+ ScopedTypeVariables, TypeInType #-}

6module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,

7 Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),

8 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),

9− Delete(..), Proxy(..)) where

9+ Delete(..), Proxy(..), remove, Remove, (:\),

10+ Member(..), NonMember, MemberP(..)) where

11import GHC.TypeLits

12import GHC.TypeLits

12import Data.Type.Bool

13import Data.Type.Bool

@@ -15,7 +16,7 @@ import Data.Type.Equality

15data Proxy (p :: k) = Proxy

16data Proxy (p :: k) = Proxy

17-- Value-level 'Set' representation, essentially a list

18-- Value-level 'Set' representation, essentially a list

18−data Set (n :: [*]) where

19+data Set (n :: [k]) where

19 {--| Construct an empty set -}

20 {--| Construct an empty set -}

20 Empty :: Set '[]

21 Empty :: Set '[]

21 {--| Extend a set with an element -}

22 {--| Extend a set with an element -}

@@ -73,6 +74,25 @@ append :: Set s -> Set t -> Set (s :++ t)

73append Empty x = x

74append Empty x = x

74append (Ext e xs) ys = Ext e (append xs ys)

75append (Ext e xs) ys = Ext e (append xs ys)

77+{-| Delete elements from a set -}

78+type family (m :: [k]) :\ (x :: k) :: [k] where

79+ '[] :\ x = '[]

80+ (x ': xs) :\ x = xs :\ x

81+ (y ': xs) :\ x = y ': (xs :\ x)

82+

83+class Remove s t where

84+ remove :: Set s -> Proxy t -> Set (s :\ t)

85+

86+instance Remove '[] t where

87+ remove Empty Proxy = Empty

88+

89+instance {-# OVERLAPS #-} Remove xs x => Remove (x ': xs) x where

90+ remove (Ext _ xs) x@Proxy = remove xs x

91+

92+instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)

93+ => Remove (y ': xs) x where

94+ remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)

95+

76{-| Splitting a union a set, given the sets we want to split it into -}

96{-| Splitting a union a set, given the sets we want to split it into -}

77class Split s t st where

97class Split s t st where

78 -- where st ~ Union s t

98 -- where st ~ Union s t

@@ -93,8 +113,6 @@ instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where

93 split (Ext x st) = let (s, t) = split st

113 split (Ext x st) = let (s, t) = split st

94 in (s, Ext x t)

114 in (s, Ext x t)

115

96−

97−

98{-| Remove duplicates from a sorted list -}

116{-| Remove duplicates from a sorted list -}

99type family Nub t where

117type family Nub t where

100 Nub '[] = '[]

118 Nub '[] = '[]

@@ -130,10 +148,10 @@ class Subset s t where

130instance Subset '[] '[] where

148instance Subset '[] '[] where

131 subset xs = Empty

149 subset xs = Empty

132

150

133−instance Subset s t => Subset s (x ': t) where

151+instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where

134 subset (Ext _ xs) = subset xs

152 subset (Ext _ xs) = subset xs

135

153

136−instance Subset s t => Subset (x ': s) (x ': t) where

154+instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where

137 subset (Ext x xs) = Ext x (subset xs)

155 subset (Ext x xs) = Ext x (subset xs)

138

156

139

157

@@ -198,3 +216,21 @@ instance Conder False where

198{-| Open-family for the ordering operation in the sort -}

216{-| Open-family for the ordering operation in the sort -}

199

217

200type family Cmp (a :: k) (b :: k) :: Ordering

218type family Cmp (a :: k) (b :: k) :: Ordering

219+

220+{-| Membership of an element in a set, with an acommanying

221+ value-level function that returns a bool -}

222+class Member a s where

223+ member :: Proxy a -> Set s -> Bool

224+

225+instance {-# OVERLAPS #-} Member a (a ': s) where

226+ member _ (Ext x _) = True

227+

228+instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where

229+ member a (Ext _ xs) = member a xs

230+

231+type family MemberP a s :: Bool where

232+ MemberP a '[] = False

233+ MemberP a (a ': s) = True

234+ MemberP a (b ': s) = MemberP a s

235+

236+type NonMember a s = MemberP a s ~ False

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

4+resolver: lts-12.7

6# Local packages, usually specified by relative directory name

7packages:

type-level-sets.cabal+19−18

@@ -1,14 +1,14 @@

1name: type-level-sets

2−version: 0.8.0.0

2+version: 0.8.9.0

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

4−description:

4+description:

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

6 finite maps via 'Map', with value-level counterparts.

7 .

8− Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard

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.

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

@@ -19,26 +19,26 @@ description:

19 > combine x y = x + y

20 >

21 > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]

22− > foo = Ext (Var :: (Var "x")) 2

22+ > foo = Ext (Var :: (Var "x")) 2

23− > $ Ext (Var :: (Var "z")) True

23+ > $ Ext (Var :: (Var "z")) True

24− > $ Ext (Var :: (Var "w")) 5

24+ > $ Ext (Var :: (Var "w")) 5

25− > $ Empty

25+ > $ Empty

26 >

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

28 > bar = Ext (Var :: (Var "y")) 3

29 > $ Ext (Var :: (Var "w")) 1

30 > $ Empty

31− >

31+ >

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

33 > foobar = foo `union` bar

34 .

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

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

37 .

38− > >>> foobar

38+ > >>> foobar

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

40 .

41− Thus, we see that the values for \"w\" are added together.

41+ Thus, we see that the values for \"w\" are added together.

42 For sets, here is an example:

43 .

44 > import GHC.TypeLits

@@ -48,7 +48,7 @@ description:

48 > data Natural (a :: Nat) where

49 > Z :: Natural 0

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

51− >

51+ >

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

53 > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))

54 >

@@ -63,15 +63,15 @@ description:

63license: BSD3

64license-file: LICENSE

65category: Type System, Data Structures

66−copyright: 2013-16 University of Cambridge

66+copyright: 2013-18 University of Kent

67author: Dominic Orchard

68maintainer: Dominic Orchard

69stability: experimental

70build-type: Simple

71cabal-version: >= 1.6

72−tested-with: GHC >= 8.0.1

72+tested-with: GHC >= 8.2.2

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

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

77source-repository head

@@ -80,10 +80,11 @@ source-repository head

81library

82 hs-source-dirs: src

83+ other-extensions: TypeInType

85 exposed-modules: Data.Type.Set

86 exposed-modules: Data.Type.Set

86 Data.Type.Map

87 Data.Type.Map

87−

88+

88 build-depends: base < 5,

89 build-depends: base < 5,

89− ghc-prim

90+ ghc-prim