master..2ad8611 · type-level-sets

git.iko.soy/type-level-sets

on 2ad8611 help sign in

changelog.mddeleted−5

since splitsnapshots

unifiedsplit

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

1− # v0.8.9.0

2−

3− - GHC 8.4 and 8.6 support.

4− - Fixed bug in the delete operation.

5− - Non-membership predicates

example2.hs−9

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

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

2−{-# LANGUAGE FlexibleContexts #-}

4import GHC.TypeLits

3import GHC.TypeLits

5import Data.Type.Set

4import Data.Type.Set

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

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

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

22foobar = foo `union` bar

21foobar = 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+24−46

@@ -46,17 +46,17 @@ type family Combine (a :: v) (b :: v) :: v

47{-| Delete elements from a map by key -}

48type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where

49− '[] :\ k = '[]

49+ '[] :\ k = '[]

50− ((k :-> v) ': m) :\ k = m :\ k

50+ ((k :-> v) ': m) :\ k = m :\ k

51− (kvp ': m) :\ k = kvp ': (m :\ k)

51+ (kvp ': m) :\ k = kvp ': (m :\ k)

53−{-| Type-level lookup of elements from a map -}

53+{-| Lookup elements from a map -}

54type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where

55 Lookup '[] k = Nothing

56 Lookup ((k :-> v) ': m) k = Just v

57 Lookup (kvp ': m) k = Lookup m k

59−{-| Membership test as type function -}

59+{-| Membership test -}

60type family Member (c :: k) (m :: [Mapping k v]) :: Bool where

61 Member k '[] = False

62 Member k ((k :-> v) ': m) = True

@@ -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 {-# OVERLAPPABLE #-} IsMember v t m => IsMember v t (x ': m) where

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

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

@@ -100,12 +100,8 @@ 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

107− update xs v x = Ext v x xs

104+ update Empty v x = Ext v x Empty

108−

109

105

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

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

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

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

@@ -121,7 +117,7 @@ instance Show (Map '[]) where

121 show Empty = "{}"

117 show Empty = "{}"

122

118

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

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

124− show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ show' s ++ "}"

120+ show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}"

125

121

126class Show' t where

122class Show' t where

127 show' :: t -> String

123 show' :: t -> String

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

133instance Eq (Map '[]) where

129instance Eq (Map '[]) where

134 Empty == Empty = True

130 Empty == Empty = True

135

131

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

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

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

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

138−

139−instance Ord (Map '[]) where

140− compare Empty Empty = EQ

141

134

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'

144−

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

135+{-| Union of two finite maps -}

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

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

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

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

148

138

149type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))

139type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))

150

140

151−{-| Append of two finite maps (non normalising) -}

152append :: Map s -> Map t -> Map (s :++ t)

141append :: Map s -> Map t -> Map (s :++ t)

153append Empty x = x

142append Empty x = x

154append (Ext k v xs) ys = Ext k v (append xs ys)

143append (Ext k v xs) ys = Ext k v (append xs ys)

@@ -163,15 +152,11 @@ class Sortable xs where

163instance Sortable '[] where

152instance Sortable '[] where

164 quicksort Empty = Empty

153 quicksort Empty = Empty

165

154

166−instance (Sortable (Filter FMin (k :-> v) xs)

155+instance (Sortable (Filter FMin (k :-> v) xs),

167− , Sortable (Filter FMax (k :-> v) xs)

168− , FilterV FMin k v xs

169− , FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where

156+ Sortable (Filter FMax (k :-> v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where

170− quicksort (Ext k v xs) =

171− quicksort (less k v xs) `append` Ext k v Empty `append` quicksort (more k v xs)

157+ quicksort (Ext k v xs) = ((quicksort (less k v xs)) `append` (Ext k v Empty)) `append` (quicksort (more k v xs))

172− where

173− less = filterV (Proxy::(Proxy FMin))

158+ where less = filterV (Proxy::(Proxy FMin))

174− more = filterV (Proxy::(Proxy FMax))

159+ more = filterV (Proxy::(Proxy FMax))

175

160

176{- Filter out the elements less-than or greater-than-or-equal to the pivot -}

161{- Filter out the elements less-than or greater-than-or-equal to the pivot -}

177class FilterV (f::Flag) k v xs where

162class FilterV (f::Flag) k v xs where

@@ -180,19 +165,13 @@ class FilterV (f::Flag) k v xs where

180instance FilterV f k v '[] where

165instance FilterV f k v '[] where

181 filterV _ k v Empty = Empty

166 filterV _ k v Empty = Empty

182

167

183−instance (Conder (Cmp x (k :-> v) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where

168+instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where

184− filterV f@Proxy k v (Ext k' v' xs) =

169+ filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy ((Cmp x (k :-> v)) == LT)))

185− cond (Proxy::(Proxy (Cmp x (k :-> v) == LT)))

186− (Ext k' v' (filterV f k v xs))

170+ (Ext k' v' (filterV f k v xs)) (filterV f k v xs)

187− (filterV f k v xs)

188

171

189−instance

190− (Conder ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ)), FilterV FMax k v xs)

172+instance (Conder (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ)), FilterV FMax k v xs) => FilterV FMax k v (x ': xs) where

191− => FilterV FMax k v (x ': xs) where

192− filterV f@Proxy k v (Ext k' v' xs) =

193− cond (Proxy::(Proxy ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ))))

173+ filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ))))

194− (Ext k' v' (filterV f k v xs))

174+ (Ext k' v' (filterV f k v xs)) (filterV f k v xs)

195− (filterV f k v xs)

196

175

197class Combinable t t' where

176class Combinable t t' where

198 combine :: t -> t' -> Combine t t'

177 combine :: t -> t' -> Combine t t'

@@ -212,8 +191,7 @@ instance {-# OVERLAPPABLE #-}

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

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

213

192

214instance {-# OVERLAPS #-}

193instance {-# OVERLAPS #-}

215− (Combinable v v', Nubable ((k :-> Combine v v') ': s))

194+ (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where

216− => Nubable ((k :-> v) ': (k :-> v') ': s) where

217 nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)

195 nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)

218

196

219

197

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

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

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

2 MultiParamTypeClasses, FlexibleInstances, PolyKinds,

3 FlexibleContexts, UndecidableInstances, ConstraintKinds,

4− ScopedTypeVariables, TypeInType #-}

4+ ScopedTypeVariables #-}

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(..), remove, Remove, (:\),

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

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

12import GHC.TypeLits

11import GHC.TypeLits

13import Data.Type.Bool

12import Data.Type.Bool

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

16data Proxy (p :: k) = Proxy

15data Proxy (p :: k) = Proxy

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

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

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

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

20 {--| Construct an empty set -}

19 {--| Construct an empty set -}

21 Empty :: Set '[]

20 Empty :: Set '[]

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

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

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

74append Empty x = x

73append Empty x = x

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

74append (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−

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

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

97class Split s t st where

77class Split s t st where

98 -- where st ~ Union s t

78 -- where st ~ Union s t

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

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

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

114 in (s, Ext x t)

94 in (s, Ext x t)

115

96+

97+

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

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

117type family Nub t where

99type family Nub t where

118 Nub '[] = '[]

100 Nub '[] = '[]

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

148instance Subset '[] '[] where

130instance Subset '[] '[] where

149 subset xs = Empty

131 subset xs = Empty

150

132

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

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

152 subset (Ext _ xs) = subset xs

134 subset (Ext _ xs) = subset xs

153

135

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

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

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

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

156

138

157

139

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

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

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

217

199

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

200type 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: lts-12.7

4+resolver: nightly-2016-07-18

6# Local packages, usually specified by relative directory name

7packages:

type-level-sets.cabal+18−19

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

1name: type-level-sets

2−version: 0.8.9.0

2+version: 0.8.0.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-18 University of Kent

66+copyright: 2013-16 University of Cambridge

67author: Dominic Orchard

68maintainer: Dominic Orchard

69stability: experimental

70build-type: Simple

71cabal-version: >= 1.6

72−tested-with: GHC >= 8.2.2

72+tested-with: GHC >= 8.0.1

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

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

77source-repository head

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

81library

82 hs-source-dirs: src

83− other-extensions: TypeInType

86 exposed-modules: Data.Type.Set

85 exposed-modules: Data.Type.Set

87 Data.Type.Map

86 Data.Type.Map

88−

87+

89 build-depends: base < 5,

88 build-depends: base < 5,

90− ghc-prim

89+ ghc-prim