master..fd032fe · type-level-sets

git.iko.soy/type-level-sets

README+21−42

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

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

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

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

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

3−"Embedding effect systems in Haskell" (Dominic Orchard,

3+sets of variable-type pairs, which is used in the paper "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 #-}

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

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:

33− *Main> foobar

10+ import Data.Type.Set

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

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

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

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

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

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

16+ Empty

38− import GHC.TypeLits

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

39− import Data.Type.Set

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

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

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

21+ Empty

42− data Natural (a :: Nat) where

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

43− Z :: Natural 0

24+ foobar = foo `union` bar

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

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

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

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

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

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

29+ *Main> foobar

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

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

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

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

53− foobar = foo `union` bar

changelog.mddeleted−5

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

example.hs+5−5

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

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

1+{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, 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,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+22−78

@@ -5,14 +5,13 @@ 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, IncoherentInstances #-}

8+ ConstraintKinds #-}

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,

15− IsMap, AsMap, asMap,

14+ IsMap, AsMap, asMap,

16 Submap, submap) where

15 Submap, submap) where

18import GHC.TypeLits

17import GHC.TypeLits

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

55 Lookup '[] k = Nothing

54 Lookup '[] k = Nothing

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

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

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

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

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

58+{-| Membership test -}

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

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

61 Member k '[] = False

60 Member k '[] = False

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

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

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

76 Empty :: Map '[]

75 Empty :: Map '[]

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

76 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−

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

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

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

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

112

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

121 show Empty = "{}"

89 show Empty = "{}"

122

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

91instance (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 ++ "}"

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

125

126class Show' t where

94class Show' t where

127 show' :: t -> String

95 show' :: t -> String

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

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

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

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

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

132

100

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−

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

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

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

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

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

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

148

104

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

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

150

106

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

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

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

153append Empty x = x

108append Empty x = x

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

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

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

163instance Sortable '[] where

118instance Sortable '[] where

164 quicksort Empty = Empty

119 quicksort Empty = Empty

165

120

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

121+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

122+ 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)

123+ 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))

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

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

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

175

126

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

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

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

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

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

180instance FilterV f k v '[] where

131instance FilterV f k v '[] where

181 filterV _ k v Empty = Empty

132 filterV _ k v Empty = Empty

182

133

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

134+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) =

135+ 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))

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

187− (filterV f k v xs)

188

137

189−instance

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

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

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

139+ 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))

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

195− (filterV f k v xs)

196

141

197class Combinable t t' where

142class Combinable t t' where

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

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

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

206instance Nubable '[e] where

151instance Nubable '[e] where

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

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

208

153

209−instance {-# OVERLAPPABLE #-}

154+instance {-# OVERLAPABLE #-}

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

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

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

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

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

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

213

158

214instance {-# OVERLAPS #-}

159instance {-# OVERLAPS #-}

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

160+ (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)

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

218

162

219

163

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

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

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

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

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

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

35 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−

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

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

43type AsSet s = Nub (Sort s)

38type AsSet s = Nub (Sort s)

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

74append Empty x = x

69append Empty x = x

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

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

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

97class Split s t st where

73class Split s t st where

98 -- where st ~ Union s t

74 -- where st ~ Union s t

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

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

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

114 in (s, Ext x t)

90 in (s, Ext x t)

115

92+

93+

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

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

117type family Nub t where

95type family Nub t where

118 Nub '[] = '[]

96 Nub '[] = '[]

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

148instance Subset '[] '[] where

126instance Subset '[] '[] where

149 subset xs = Empty

127 subset xs = Empty

150

128

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

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

152 subset (Ext _ xs) = subset xs

130 subset (Ext _ xs) = subset xs

153

131

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

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

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

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

156

134

157

135

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

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

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

217

195

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

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

6# Local packages, usually specified by relative directory name

7packages:

type-level-sets.cabal+25−31

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

1name: type-level-sets

2−version: 0.8.9.0

2+version: 0.7

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

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

16+ > foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]

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

17+ > foo = Ext ((Var :: (Var "x")) :-> 2) $

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

18+ > Ext ((Var :: (Var "z")) :-> 4) $

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

19+ > Ext ((Var :: (Var "w")) :-> 5) $

25− > $ Empty

20+ > Empty

26 >

21 >

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

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

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

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

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

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

30− > $ Empty

25+ > Empty

31− >

26+ >

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

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

33 > foobar = foo `union` bar

28 > foobar = foo `union` bar

34 .

29 .

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

30+ The 'Set' 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:

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

37 .

32 .

38− > >>> foobar

33+ > >>> foobar

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

34+ > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]

40 .

35 .

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

36+ Thus, we see that the first value paired with the \"w\" variable is dropped.

42 For sets, here is an example:

37 For sets, here is an example:

43 .

38 .

44 > import GHC.TypeLits

39 > import GHC.TypeLits

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

48 > data Natural (a :: Nat) where

43 > data Natural (a :: Nat) where

49 > Z :: Natural 0

44 > Z :: Natural 0

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

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

51− >

46+ >

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

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

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

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

54 >

49 >

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

63license: BSD3

58license: BSD3

64license-file: LICENSE

59license-file: LICENSE

65category: Type System, Data Structures

60category: Type System, Data Structures

66−copyright: 2013-18 University of Kent

61+copyright: 2013-16 University of Cambridge

67author: Dominic Orchard

62author: Dominic Orchard

68maintainer: Dominic Orchard

63maintainer: Dominic Orchard

69stability: experimental

64stability: experimental

70build-type: Simple

65build-type: Simple

71cabal-version: >= 1.6

66cabal-version: >= 1.6

72−tested-with: GHC >= 8.2.2

67+tested-with: GHC == 7.10.3

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

69+extra-source-files: example.hs

77source-repository head

72source-repository head

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

81library

76library

82 hs-source-dirs: src

77 hs-source-dirs: src

83− other-extensions: TypeInType

86 exposed-modules: Data.Type.Set

80 exposed-modules: Data.Type.Set

87 Data.Type.Map

81 Data.Type.Map

88−

82+

89 build-depends: base < 5,

83 build-depends: base < 5,

90− ghc-prim

84+ ghc-prim