git.iko.soy/type-level-sets
on master help sign in
updated set example, fixed overlapping
commita86bba961ac9a1dc9590345fd0a7a73473b4232b authordominic <dom.orchard@gmail.com> dateTue 5 Jan 2016, 17:46 (11 years ago) parentc3543c6
4 files changed+56−15
compare with master
unifiedsplit
example.hs+2−2 example2.hs+21 src/Data/Type/Set.hs+4−4 type-level-sets.cabal+29−9
example.hs+2−2
@@ -22,5 +22,5 @@ bar = Ext (Var :: (Var "y")) 3 $
2222 Empty
2323
2424-- GHC can easily infer this type, so an explicit signature not necessary
25−-- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
26−foobar = foo `union` bar
25+-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
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
1414
1515-- Value-level 'Set' representation, essentially a list
1616data Set (n :: [*]) where
17− {-| Construct an empty set-}
18− Empty :: Set '[]
19− {-| Extend a set with an element -}
17+ {--| Construct an empty set -}
18+ Empty :: Set '[]
19+ {--| Extend a set with an element -}
2020 Ext :: e -> Set s -> Set (e ': s)
2121
2222instance Show (Set '[]) where
@@ -112,7 +112,7 @@ instance Nubable '[e] where
112112instance Nubable (e ': s) => Nubable (e ': e ': s) where
113113 nub (Ext _ (Ext e s)) = nub (Ext e s)
114114
115−instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
115+instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
116116 Nubable (f ': s)) => Nubable (e ': f ': s) where
117117 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
118118
type-level-sets.cabal+29−9
@@ -1,30 +1,30 @@
11name: type-level-sets
2−version: 0.6
3−synopsis: Type-level sets and finite maps (with value-level counterparts and various operations)
2+version: 0.6.1
3+synopsis: Type-level sets and finite maps (with value-level counterparts)
44description:
55 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.
77 .
88 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.
1010 .
11− Here is a brief example:
11+ Here is a brief example for finite maps.:
1212 .
1313 >
1414 > import Data.Type.Map
1515 >
16− > foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
16+ > foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]
1717 > foo = Ext ((Var :: (Var "x")) :-> 2) $
1818 > Ext ((Var :: (Var "z")) :-> 4) $
1919 > Ext ((Var :: (Var "w")) :-> 5) $
2020 > Empty
2121 >
22− > bar :: Set '["y" :-> Int, "w" :-> Int]
22+ > bar :: Map '["y" :-> Int, "w" :-> Int]
2323 > bar = Ext ((Var :: (Var "y")) :-> 3) $
2424 > Ext ((Var :: (Var "w")) :-> 1) $
2525 > Empty
2626 >
27− > -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
27+ > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
2828 > foobar = foo `union` bar
2929 .
3030 The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
@@ -34,11 +34,31 @@ description:
3434 > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]
3535 .
3636 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.
3757 .
3858license: BSD3
3959license-file: LICENSE
4060category: Type System, Data Structures
41−copyright: 2013-14 University of Cambridge
61+copyright: 2013-16 University of Cambridge
4262author: Dominic Orchard
4363maintainer: Dominic Orchard
4464stability: experimental