git.iko.soy/type-level-sets
on master help sign in
updated set example, fixed overlapping
a86bba9dominic
example.hs+2−2
compare with master
unifiedsplit
@@ -22,5 +22,5 @@ bar = Ext (Var :: (Var "y")) 3 $
22 Empty
22 Empty
23
23
24-- GHC can easily infer this type, so an explicit signature not necessary
24-- GHC can easily infer this type, so an explicit signature not necessary
25−-- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
25+-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
26−foobar = foo `union` bar
26+foobar = foo `union` bar
example2.hsnew file+21
@@ -0,0 +1,21 @@
1+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}
2+
3+import GHC.TypeLits
4+import Data.Type.Set
5+
6+type instance Cmp (Natural n) (Natural m) = CmpNat n m
7+
8+data Natural (a :: Nat) where
9+ Z :: Natural 0
10+ S :: Natural n -> Natural (n + 1)
11+
12+deriving instance Show (Natural n)
13+
14+-- foo :: Set '[Natural 0, Natural 1, Natural 3]
15+foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
16+
17+-- bar :: Set '[Natural 1, Natural 2]
18+bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
19+
20+-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
21+foobar = foo `union` bar
src/Data/Type/Set.hs+4−4
@@ -14,9 +14,9 @@ data Proxy (p :: k) = Proxy
14
14
15-- Value-level 'Set' representation, essentially a list
15-- Value-level 'Set' representation, essentially a list
16data Set (n :: [*]) where
16data Set (n :: [*]) where
17− {-| Construct an empty set-}
17+ {--| Construct an empty set -}
18− Empty :: Set '[]
18+ Empty :: Set '[]
19− {-| Extend a set with an element -}
19+ {--| Extend a set with an element -}
20 Ext :: e -> Set s -> Set (e ': s)
20 Ext :: e -> Set s -> Set (e ': s)
21
21
22instance Show (Set '[]) where
22instance Show (Set '[]) where
@@ -112,7 +112,7 @@ instance Nubable '[e] where
112instance Nubable (e ': s) => Nubable (e ': e ': s) where
112instance Nubable (e ': s) => Nubable (e ': e ': s) where
113 nub (Ext _ (Ext e s)) = nub (Ext e s)
113 nub (Ext _ (Ext e s)) = nub (Ext e s)
114
114
115−instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
115+instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
116 Nubable (f ': s)) => Nubable (e ': f ': s) where
116 Nubable (f ': s)) => Nubable (e ': f ': s) where
117 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
117 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
118
118
type-level-sets.cabal+29−9
@@ -1,30 +1,30 @@
1name: type-level-sets
1name: type-level-sets
2−version: 0.6
2+version: 0.6.1
3−synopsis: Type-level sets and finite maps (with value-level counterparts and various operations)
3+synopsis: Type-level sets and finite maps (with value-level counterparts)
4description:
4description:
5 This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
5 This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
6− maps via 'Map', with value-level counterparts.
6+ finite maps via 'Map', with value-level counterparts.
7 .
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)
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 .
10 .
11− Here is a brief example:
11+ Here is a brief example for finite maps.:
12 .
12 .
13 >
13 >
14 > import Data.Type.Map
14 > import Data.Type.Map
15 >
15 >
16− > foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
16+ > foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]
17 > foo = Ext ((Var :: (Var "x")) :-> 2) $
17 > foo = Ext ((Var :: (Var "x")) :-> 2) $
18 > Ext ((Var :: (Var "z")) :-> 4) $
18 > Ext ((Var :: (Var "z")) :-> 4) $
19 > Ext ((Var :: (Var "w")) :-> 5) $
19 > Ext ((Var :: (Var "w")) :-> 5) $
20 > Empty
20 > Empty
21 >
21 >
22− > bar :: Set '["y" :-> Int, "w" :-> Int]
22+ > bar :: Map '["y" :-> Int, "w" :-> Int]
23 > bar = Ext ((Var :: (Var "y")) :-> 3) $
23 > bar = Ext ((Var :: (Var "y")) :-> 3) $
24 > Ext ((Var :: (Var "w")) :-> 1) $
24 > Ext ((Var :: (Var "w")) :-> 1) $
25 > Empty
25 > Empty
26 >
26 >
27− > -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
27+ > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
28 > foobar = foo `union` bar
28 > foobar = foo `union` bar
29 .
29 .
30 The 'Set' 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).
@@ -34,11 +34,31 @@ description:
34 > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]
34 > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]
35 .
35 .
36 Thus, we see that the first value paired with the \"w\" variable is dropped.
36 Thus, we see that the first value paired with the \"w\" variable is dropped.
37+ For sets, here is an example:
38+ .
39+ > import GHC.TypeLits
40+ > import Data.Type.Set
41+ > type instance Cmp (Natural n) (Natural m) = CmpNat n m
42+ >
43+ > data Natural (a :: Nat) where
44+ > Z :: Natural 0
45+ > S :: Natural n -> Natural (n + 1)
46+ >
47+ > -- foo :: Set '[Natural 0, Natural 1, Natural 3]
48+ > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
49+ >
50+ > -- bar :: Set '[Natural 1, Natural 2]
51+ > bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
52+ >
53+ > -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
54+ > foobar = foo `union` bar
55+ .
56+ Note the types here are all inferred.
37 .
57 .
38license: BSD3
58license: BSD3
39license-file: LICENSE
59license-file: LICENSE
40category: Type System, Data Structures
60category: Type System, Data Structures
41−copyright: 2013-14 University of Cambridge
61+copyright: 2013-16 University of Cambridge
42author: Dominic Orchard
62author: Dominic Orchard
43maintainer: Dominic Orchard
63maintainer: Dominic Orchard
44stability: experimental
64stability: experimental