git.iko.soy/type-level-sets
on master help sign in
readme plus differen show instances
8a8bca6Dominic Orchard
READMEnew file+36
compare with master
unifiedsplit
@@ -0,0 +1,36 @@
1+This library provides type-level sets 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
3+sets of variable-type pairs, which is used in the paper "Embedding effect systems in Haskell" (Dominic Orchard,
4+Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.
5+
6+Here is some example code!
7+
8+<code>
9+ {-# LANGUAGE DataKinds, TypeOperators #-}
10+
11+ import Data.Type.Set
12+
13+ -- foo :: Set '["x" :-> Integer, "z" :-> Integer]
14+ foo = Ext ((Var :: (Var "x")) :-> 2) $
15+ Ext ((Var :: (Var "z")) :-> 4) $
16+ Empty
17+
18+ -- bar :: Set '["y" :-> Integer, "w" :-> Integer]
19+ bar = Ext ((Var :: (Var "y")) :-> 3) $
20+ Ext ((Var :: (Var "w")) :-> 1) $
21+ Empty
22+
23+ -- foobar :: Set '["w" :-> Integer, "x" :-> Integer, "y" :-> Integer, "z" :-> Integer]
24+ foobar = foo `union` bar
25+</code>
26+
27+Note, the type signatures are commented out here as they can be inferred.
28+Example execution:
29+
30+<code>
31+ *Main> foobar
32+ {(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)}
33+</code>
34+
35+
36+
src/Data/Type/Set.hs+10−4
@@ -5,7 +5,8 @@
5
5
6module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
6module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7 Sort, Sortable, Append(..), Split(..), Cmp,
7 Sort, Sortable, Append(..), Split(..), Cmp,
8− Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..)) where
8+ Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9+ (:->)(..), Var(..)) where
9
10
10import GHC.TypeLits
11import GHC.TypeLits
11import Data.Type.Bool
12import Data.Type.Bool
@@ -196,11 +197,16 @@ data Var (k :: Symbol) where Var :: Var k
196instance (Show (Var k), Show v) => Show (k :-> v) where
197instance (Show (Var k), Show v) => Show (k :-> v) where
197 show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
198 show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
198instance Show (Var "x") where
199instance Show (Var "x") where
199− show _ = "x"
200+ show X = "x"
201+ show Var = "Var"
200instance Show (Var "y") where
202instance Show (Var "y") where
201− show _ = "y"
203+ show Y = "y"
204+ show Var = "Var"
202instance Show (Var "z") where
205instance Show (Var "z") where
203− show _ = "z"
206+ show Z = "z"
207+ show Var = "Var"
208+instance Show (Var v) where
209+ show _ = "Var"
204
210
205{-| Symbol comparison -}
211{-| Symbol comparison -}
206type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u
212type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u