type-level-sets 0.5 → 0.6
raw patch · 4 files changed
+207/−58 lines, 4 filesdep ~base
Dependency ranges changed: base
Files
- example.hs +17/−9
- src/Data/Type/Map.hs +157/−0
- src/Data/Type/Set.hs +24/−43
- type-level-sets.cabal +9/−6
example.hs view
@@ -1,16 +1,24 @@-{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-} -import Data.Type.Set+import GHC.TypeLits+import Data.Type.Map -foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]-foo = Ext ((Var :: (Var "x")) :-> 2) $- Ext ((Var :: (Var "z")) :-> 4) $- Ext ((Var :: (Var "w")) :-> 5) $+-- Specify that key-value pairs on Ints combine to an Int+type instance Combine Int Int = Int+-- Specify that Int values for matching keys should be added+instance Combinable Int Int where+ combine x y = x + y+ +foo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]+foo = Ext (Var :: (Var "x")) 2 $+ Ext (Var :: (Var "z")) 4 $+ Ext (Var :: (Var "w")) 5 $ Empty -bar :: Set '["y" :-> Int, "w" :-> Int]-bar = Ext ((Var :: (Var "y")) :-> 3) $- Ext ((Var :: (Var "w")) :-> 1) $++bar :: Map '["y" :-> Int, "w" :-> Int]+bar = Ext (Var :: (Var "y")) 3 $+ Ext (Var :: (Var "w")) 1 $ Empty -- GHC can easily infer this type, so an explicit signature not necessary
+ src/Data/Type/Map.hs view
@@ -0,0 +1,157 @@+{- This module provides type-level finite maps.+The implementation is similar to that shown in the paper.+ "Embedding effect systems in Haskell" Orchard, Petricek 2014 -}++{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures, + TypeFamilies, UndecidableInstances, MultiParamTypeClasses, + FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables, ConstraintKinds #-}++module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..), + Combine, Combinable(..), Cmp, + Lookup, Member, (:\)) where++import GHC.TypeLits+import Data.Type.Bool+import Data.Type.Equality+import Data.Type.Set hiding (Set(..), Nub,Union,Nubable,Sortable,Unionable,append,union,quicksort,nub)++{- Throughout, type variables+ 'k' ranges over "keys"+ 'v' ranges over "values"+ 'kvp' ranges over "key-value-pairs"+ 'm', 'n' range over "maps" -}++-- Mappings+infixr 4 :-> +{-| A key-value pair -}+data Mapping k v = k :-> v++{-| Union of two finite maps -}+type Union m n = Nub (Sort (m :++ n))++{-| Apply 'Combine' to values with matching key (removes duplicate keys) -}+type family Nub t where+ Nub '[] = '[]+ Nub '[kvp] = '[kvp]+ Nub ((k :-> v1) ': (k :-> v2) ': m) = Nub ((k :-> Combine v1 v2) ': m)+ Nub (kvp1 ': kvp2 ': s) = kvp1 ': Nub (kvp2 ': s)++{-| Open type family for combining values in a map (that have the same key) -}+type family Combine (a :: v) (b :: v) :: v++{-| Delete elements from a map by key -}+type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where+ '[] :\ k = '[]+ ((k :-> v) ': m) :\ k = m :\ k+ (kvp ': m) :\ k = kvp ': (m :\ k)++{-| Lookup elements from a map -}+type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where+ Lookup '[] k = Nothing+ Lookup ((k :-> v) ': m) k = Just v+ Lookup (kvp ': m) k = Lookup m k++{-| Membership test -}+type family Member (c :: k) (m :: [Mapping k v]) :: Bool where+ Member k '[] = False+ Member k ((k :-> v) ': m) = True+ Member k (kvp ': m) = Member k m++-----------------------------------------------------------------+-- Value-level map with a type-level representation++{-| Pair a symbol (representing a variable) with a type -}+data Var (k :: Symbol) = Var ++instance KnownSymbol k => Show (Var k) where+ show = symbolVal++{-| A value-level heterogenously-typed Map (with type-level representation in terms of lists) -}+data Map (n :: [Mapping Symbol *]) where+ Empty :: Map '[]+ Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)++instance Show (Map '[]) where+ show Empty = "{}"++instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where+ show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ (show' s) ++ "}" ++class Show' t where+ show' :: t -> String+instance Show' (Map '[]) where+ show' Empty = ""+instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s)) where+ show' (Ext k v s) = ", " ++ show k ++ " :-> " ++ show v ++ (show' s)++{-| Union of two finite maps -}+union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)+union s t = nub (quicksort (append s t))++type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))++append :: Map s -> Map t -> Map (s :++ t)+append Empty x = x+append (Ext k v xs) ys = Ext k v (append xs ys)++type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'+type instance Cmp (k :-> v) (k' :-> v) = CmpSymbol k k'++{-| Value-level quick sort that respects the type-level ordering -}+class Sortable xs where+ quicksort :: Map xs -> Map (Sort xs)++instance Sortable '[] where+ quicksort Empty = Empty++instance (Sortable (Filter FMin (k :-> v) xs),+ Sortable (Filter FMax (k :-> v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where+ quicksort (Ext k v xs) = ((quicksort (less k v xs)) `append` (Ext k v Empty)) `append` (quicksort (more k v xs))+ where less = filterV (Proxy::(Proxy FMin))+ more = filterV (Proxy::(Proxy FMax))++{- Filter out the elements less-than or greater-than-or-equal to the pivot -}+class FilterV (f::Flag) k v xs where+ filterV :: Proxy f -> Var k -> v -> Map xs -> Map (Filter f (k :-> v) xs)++instance FilterV f k v '[] where+ filterV _ k v Empty = Empty++instance (Conder ((Cmp x (k :-> v)) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where+ filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy ((Cmp x (k :-> v)) == LT)))+ (Ext k' v' (filterV f k v xs)) (filterV f k v xs) ++instance (Conder (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ)), FilterV FMax k v xs) => FilterV FMax k v (x ': xs) where+ filterV f@Proxy k v (Ext k' v' xs) = cond (Proxy::(Proxy (((Cmp x (k :-> v)) == GT) || ((Cmp x (k :-> v)) == EQ))))+ (Ext k' v' (filterV f k v xs)) (filterV f k v xs) ++class Combinable t t' where+ combine :: t -> t' -> Combine t t'++class Nubable t where+ nub :: Map t -> Map (Nub t)++instance Nubable '[] where+ nub Empty = Empty++instance Nubable '[e] where+ nub (Ext k v Empty) = Ext k v Empty++instance {-# OVERLAPPING #-}+ (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where+ nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)++instance {-# OVERLAPPING #-}+ (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), + Nubable (f ': s)) => Nubable (e ': f ': s) where+ nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))++class Conder g where+ cond :: Proxy g -> Map s -> Map t -> Map (If g s t)++instance Conder True where+ cond _ s t = s++instance Conder False where+ cond _ s t = t+
src/Data/Type/Set.hs view
@@ -1,20 +1,22 @@ {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,- UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}+ UndecidableInstances, ConstraintKinds, ScopedTypeVariables #-} module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, - Sort, Sortable, Append(..), Split(..), Cmp, - Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),- (:->)(..), Var(..)) where+ Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..), + Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..), Delete(..), Proxy(..)) where import GHC.TypeLits import Data.Type.Bool import Data.Type.Equality-import Data.Proxy -{-| Core Set definition, in terms of lists -}+data Proxy (p :: k) = Proxy++-- Value-level 'Set' representation, essentially a list data Set (n :: [*]) where- Empty :: Set '[]+ {--| Construct an empty set -}+ Empty :: Set '[] + {--| Extend a set with an element -} Ext :: e -> Set s -> Set (e ': s) instance Show (Set '[]) where@@ -49,25 +51,22 @@ {-- Union --} {-| Union of sets -}-type Union s t = Nub (Sort (Append s t))+type Union s t = Nub (Sort (s :++ t)) union :: (Unionable s t) => Set s -> Set t -> Set (Union s t) union s t = nub (quicksort (append s t)) -type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)))+type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t))) {-| List append (essentially set disjoint union) -}-type family Append (s :: [k]) (t :: [k]) :: [k] where- Append '[] t = t- Append (x ': xs) ys = x ': (Append xs ys)+type family (:++) (x :: [k]) (y :: [k]) :: [k] where+ '[] :++ xs = xs+ (x ': xs) :++ ys = x ': (xs :++ ys) -append :: Set s -> Set t -> Set (Append s t)+append :: Set s -> Set t -> Set (s :++ t) append Empty x = x append (Ext e xs) ys = Ext e (append xs ys) -{-| Useful alias for append -}-type (s :: [k]) :++ (t :: [k]) = Append s t- {-| Splitting a union a set, given the sets we want to split it into -} class Split s t st where -- where st ~ Union s t@@ -144,6 +143,15 @@ Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs) Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs) +type family DeleteFromList (e :: elem) (list :: [elem]) where+ DeleteFromList elem '[] = '[]+ DeleteFromList elem (x ': xs) = If (Cmp elem x == EQ)+ xs+ (x ': DeleteFromList elem xs)++type family Delete elem set where+ Delete elem (Set xs) = Set (DeleteFromList elem xs)+ {-| Value-level quick sort that respects the type-level ordering -} class Sortable xs where quicksort :: Set xs -> Set (Sort xs)@@ -185,30 +193,3 @@ type family Cmp (a :: k) (b :: k) :: Ordering -{-| Pair a symbol (represetning a variable) with a type -}-infixl 2 :->-data (k :: Symbol) :-> (v :: *) = (Var k) :-> v--data Var (k :: Symbol) where Var :: Var k - {-| Some special defaults for some common names -}- X :: Var "x"- Y :: Var "y"- Z :: Var "z"---instance (Show (Var k), Show v) => Show (k :-> v) where- show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"-instance Show (Var "x") where- show X = "x"- show Var = "Var"-instance Show (Var "y") where- show Y = "y"- show Var = "Var"-instance Show (Var "z") where- show Z = "z"- show Var = "Var"-instance Show (Var v) where- show _ = "Var"--{-| Symbol comparison -}-type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u
type-level-sets.cabal view
@@ -1,15 +1,17 @@ name: type-level-sets-version: 0.5-synopsis: Type-level sets (with value-level counterparts and various operations)+version: 0.6+synopsis: Type-level sets and finite maps (with value-level counterparts and various operations) description: - This package provides type-level sets (no duplicates, sorted to provide a nomral form) via 'Set', - with value-level counterparts. Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard + This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level+ maps via 'Map', with value-level counterparts.+ .+ Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014) . Here is a brief example: . >- > import Data.Type.Set+ > import Data.Type.Map > > foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int] > foo = Ext ((Var :: (Var "x")) :-> 2) $@@ -56,6 +58,7 @@ exposed-modules: Data.Type.Set+ Data.Type.Map - build-depends: base < 5,+ build-depends: base >= 4.7.0.0 && < 5, ghc-prim