fd032fe...master · type-level-sets

git.iko.soy/type-level-sets

README+42−21

since splitsnapshots

@@ -1,35 +1,56 @@

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

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

2−subsets, and split sets. Also included is a "mapping" type constructor that pairs symbols with types. This can be used to represent

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

3−sets of variable-type pairs, which is used in the paper "Embedding effect systems in Haskell" (Dominic Orchard,

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 #-}

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

9+ import Data.Type.Map

10+

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

15+

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

21+

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

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

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

25+ $ Empty

26+

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

28+ foobar = foo `union` bar

29+

30+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:

10− import Data.Type.Set

33+ *Main> foobar

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

12− foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]

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

13− foo = Ext ((Var :: (Var "x")) :-> 2) $

14− Ext ((Var :: (Var "z")) :-> 4) $

15− Ext ((Var :: (Var "w")) :-> 5) $

16− Empty

18− bar :: Set '["y" :-> Int, "w" :-> Int]

38+ import GHC.TypeLits

19− bar = Ext ((Var :: (Var "y")) :-> 3) $

39+ import Data.Type.Set

20− Ext ((Var :: (Var "w")) :-> 1) $

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

21− Empty

23− -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]

42+ data Natural (a :: Nat) where

24− foobar = foo `union` bar

43+ Z :: Natural 0

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

26−The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).

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

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

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

29− *Main> foobar

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

30− {(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)}

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

32−Thus, we see that the first value paired with the "w" variable is dropped.

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

53+ foobar = foo `union` bar

changelog.mdnew file+5

@@ -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

example.hs+5−5

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

1−{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}

1+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}

3import GHC.TypeLits

4import Data.Type.Map

@@ -10,10 +10,10 @@ instance Combinable Int Int where

10 combine x y = x + y

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

13−foo = Ext (Var :: (Var "x")) 2 $

13+foo = Ext (Var :: (Var "x")) 2

14− Ext (Var :: (Var "z")) True $

14+ $ Ext (Var :: (Var "z")) True

15− Ext (Var :: (Var "w")) 5 $

15+ $ Ext (Var :: (Var "w")) 5

16− Empty

16+ $ Empty

18foo' :: Map (AsMap '["z" :-> Bool, "x" :-> Int, "w" :-> Int])

19foo' = asMap foo

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+78−22

@@ -5,13 +5,14 @@ The implementation is similar to that shown in the paper.

5{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,

6 TypeFamilies, UndecidableInstances, MultiParamTypeClasses,

7 FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables,

8− ConstraintKinds #-}

8+ ConstraintKinds, IncoherentInstances #-}

10module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),

11 Combine, Combinable(..), Cmp,

12 Nubable, nub,

13 Lookup, Member, (:\), Split, split,

14+ IsMember, lookp, Updatable, update,

14− IsMap, AsMap, asMap,

15+ IsMap, AsMap, asMap,

15 Submap, submap) where

16 Submap, submap) where

17import GHC.TypeLits

18import GHC.TypeLits

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

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

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

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

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

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

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

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

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

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

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

52−{-| Lookup elements from a map -}

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

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

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

54 Lookup '[] k = Nothing

55 Lookup '[] k = Nothing

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

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

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

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

58−{-| Membership test -}

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

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

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

60 Member k '[] = False

61 Member k '[] = False

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

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

@@ -75,6 +76,37 @@ data Map (n :: [Mapping Symbol *]) where

75 Empty :: Map '[]

76 Empty :: Map '[]

76 Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)

77 Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)

79+{-| Membership test a type class (predicate) -}

80+class IsMember v t m where

81+ {-| Value-level lookup of elements from a map, via type class predicate -}

82+ lookp :: Var v -> Map m -> t

83+

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

85+ lookp _ (Ext _ x _) = x

86+

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

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

89+

90+

91+{-| Updatability as a type class -}

92+class Updatable v t m n where

93+ {-| Update a map with `m` at variable `v` with a value of type `t`

94+ to produce a map of type `n` -}

95+ update :: Map m -> Var v -> t -> Map n

96+

97+instance {-# OVERLAPS #-} Updatable v t ((v ':-> s) ': m) ((v ':-> t) ': m) where

98+ update (Ext v _ m) _ x = Ext v x m

99+

100+instance 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

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

108+

109+

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

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

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

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

112

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

89 show Empty = "{}"

121 show Empty = "{}"

122

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

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

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

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

125

94class Show' t where

126class Show' t where

95 show' :: t -> String

127 show' :: t -> String

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

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

130instance (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)

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

100

132

133+instance Eq (Map '[]) where

134+ Empty == Empty = True

135+

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

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'

144+

101−{-| Union of two finite maps -}

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

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

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

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

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

104

148

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

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

106

150

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

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

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

108append Empty x = x

153append Empty x = x

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

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

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

118instance Sortable '[] where

163instance Sortable '[] where

119 quicksort Empty = Empty

164 quicksort Empty = Empty

120

165

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

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

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

168+ , FilterV FMin k v xs

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

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

170+ quicksort (Ext k v xs) =

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

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

172+ where

124− where less = filterV (Proxy::(Proxy FMin))

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

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

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

126

175

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

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

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

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

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

131instance FilterV f k v '[] where

180instance FilterV f k v '[] where

132 filterV _ k v Empty = Empty

181 filterV _ k v Empty = Empty

133

182

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

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

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

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

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

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

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

187+ (filterV f k v xs)

137

188

189+instance

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

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

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

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

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

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

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

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

195+ (filterV f k v xs)

141

196

142class Combinable t t' where

197class Combinable t t' where

143 combine :: t -> t' -> Combine t t'

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

@@ -151,13 +206,14 @@ instance Nubable '[] where

151instance Nubable '[e] where

206instance Nubable '[e] where

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

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

153

208

154−instance {-# OVERLAPABLE #-}

209+instance {-# OVERLAPPABLE #-}

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

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

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

211 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))

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

158

213

159instance {-# OVERLAPS #-}

214instance {-# OVERLAPS #-}

160− (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where

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

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

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

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

162

218

163

219

src/Data/Type/Set.hs+47−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 -}

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

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

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

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

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

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

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

40+

41+

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

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

38type AsSet s = Nub (Sort s)

43type AsSet s = Nub (Sort s)

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

69append Empty x = x

74append Empty x = x

70append (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+

72{-| 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 -}

73class Split s t st where

97class Split s t st where

74 -- where st ~ Union s t

98 -- where st ~ Union s t

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

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

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

90 in (s, Ext x t)

114 in (s, Ext x t)

115

92−

93−

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

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

95type family Nub t where

117type family Nub t where

96 Nub '[] = '[]

118 Nub '[] = '[]

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

126instance Subset '[] '[] where

148instance Subset '[] '[] where

127 subset xs = Empty

149 subset xs = Empty

128

150

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

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

130 subset (Ext _ xs) = subset xs

152 subset (Ext _ xs) = subset xs

131

153

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

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

133 subset (Ext x xs) = Ext x (subset xs)

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

134

156

135

157

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

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

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

195

217

196type 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: lts-3.5

4+resolver: lts-12.7

6# Local packages, usually specified by relative directory name

7packages:

type-level-sets.cabal+31−25

@@ -1,39 +1,44 @@

1name: type-level-sets

2−version: 0.7

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

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

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

43 > data Natural (a :: Nat) where

48 > data Natural (a :: Nat) where

44 > Z :: Natural 0

49 > Z :: Natural 0

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

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

46− >

51+ >

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

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

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

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

49 >

54 >

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

58license: BSD3

63license: BSD3

59license-file: LICENSE

64license-file: LICENSE

60category: Type System, Data Structures

65category: Type System, Data Structures

61−copyright: 2013-16 University of Cambridge

66+copyright: 2013-18 University of Kent

62author: Dominic Orchard

67author: Dominic Orchard

63maintainer: Dominic Orchard

68maintainer: 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.2.2

69−extra-source-files: example.hs

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

72source-repository head

77source-repository head

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

76library

81library

77 hs-source-dirs: src

82 hs-source-dirs: src

83+ other-extensions: TypeInType

80 exposed-modules: Data.Type.Set

86 exposed-modules: Data.Type.Set

81 Data.Type.Map

87 Data.Type.Map

82−

88+

83 build-depends: base < 5,

89 build-depends: base < 5,

84− ghc-prim

90+ ghc-prim