diff --git a/src/Data/Type/Map.hs b/src/Data/Type/Map.hs --- a/src/Data/Type/Map.hs +++ b/src/Data/Type/Map.hs @@ -5,13 +5,14 @@ {-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures, TypeFamilies, UndecidableInstances, MultiParamTypeClasses, FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables, - ConstraintKinds #-} + ConstraintKinds, IncoherentInstances #-} module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..), Combine, Combinable(..), Cmp, Nubable, nub, Lookup, Member, (:\), Split, split, - IsMap, AsMap, asMap, + IsMember, lookp, Updatable, update, + IsMap, AsMap, asMap, Submap, submap) where import GHC.TypeLits @@ -45,17 +46,17 @@ {-| 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) + '[] :\ k = '[] + ((k :-> v) ': m) :\ k = m :\ k + (kvp ': m) :\ k = kvp ': (m :\ k) -{-| Lookup elements from a map -} +{-| Type-level lookup of 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 -} +{-| Membership test as type function -} type family Member (c :: k) (m :: [Mapping k v]) :: Bool where Member k '[] = False Member k ((k :-> v) ': m) = True @@ -75,6 +76,33 @@ Empty :: Map '[] Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m) +{-| Membership test a type class (predicate) -} +class IsMember v t m where + {-| Value-level lookup of elements from a map, via type class predicate -} + lookp :: Var v -> Map m -> t + +instance {-# OVERLAPS #-} IsMember v t ((v ':-> t) ': m) where + lookp _ (Ext _ x _) = x + +instance IsMember v t m => IsMember v t (x ': m) where + lookp v (Ext _ _ m) = lookp v m + + +{-| Updatability as a type class -} +class Updatable v t m n where + {-| Update a map with `m` at variable `v` with a value of type `t` + to produce a map of type `n` -} + update :: Map m -> Var v -> t -> Map n + +instance {-# OVERLAPS #-} Updatable v t ((v ':-> s) ': m) ((v ':-> t) ': m) where + update (Ext v _ m) _ x = Ext v x m + +instance Updatable v t m n => Updatable v t ((w ':-> y) ': m) ((w ':-> y) ': n) where + update (Ext w y m) v x = Ext w y (update m v x) + +instance Updatable v t '[] '[v ':-> t] where + update Empty v x = Ext v x Empty + {-| Predicate to check if in normalised map form -} type IsMap s = (s ~ Nub (Sort s)) @@ -89,7 +117,7 @@ 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) ++ "}" + show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ show' s ++ "}" class Show' t where show' :: t -> String @@ -104,12 +132,13 @@ instance (KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where (Ext k v m) == (Ext k' v' m') = k == k' && v == v' && m == m' -{-| Union of two finite maps -} +{-| Union of two finite maps (normalising) -} 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 of two finite maps (non normalising) -} append :: Map s -> Map t -> Map (s :++ t) append Empty x = x append (Ext k v xs) ys = Ext k v (append xs ys) @@ -124,11 +153,15 @@ 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)) +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 @@ -137,13 +170,19 @@ 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) == 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) +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' @@ -163,7 +202,8 @@ nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s)) instance {-# OVERLAPS #-} - (Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': (k :-> v') ': s) where + (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) diff --git a/type-level-sets.cabal b/type-level-sets.cabal --- a/type-level-sets.cabal +++ b/type-level-sets.cabal @@ -1,67 +1,65 @@ name: type-level-sets -version: 0.8.0.0 +version: 0.8.5.0 synopsis: Type-level sets and finite maps (with value-level counterparts) -description: This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level finite maps via 'Map', with value-level counterparts. - . - Described in the paper "Embedding effect systems in Haskell" by Dominic Orchard and Tomas Petricek (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation. - . - Here is a brief example for finite maps: - . - @ - import Data.Type.Map - . - -- Specify how to combine duplicate key-value pairs for Int values - type instance Combine Int Int = Int - instance Combinable Int Int where - combine x y = x + y - . - foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int] - foo = Ext (Var :: (Var "x")) 2 - $ Ext (Var :: (Var "z")) True - $ Ext (Var :: (Var "w")) 5 - $ Empty - . - bar :: Map '["y" :-> Int, "w" :-> Int] - bar = Ext (Var :: (Var "y")) 3 - $ Ext (Var :: (Var "w")) 1 - $ Empty - . - -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool] - foobar = foo `union` bar - . - @ - . - The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates). The type signatures is commented out as it can be infered. Running the example we get: - . - @ - > >>> foobar - > {w :-> 6, x :-> 2, y :-> 3, z :-> True} - @ - . - Thus, we see that the values for \"w\" are added together. - . - For sets, here is an example: - . - @ - import GHC.TypeLits - import Data.Type.Set - type instance Cmp (Natural n) (Natural m) = CmpNat n m - . - data Natural (a :: Nat) where - Z :: Natural 0 - S :: Natural n -> Natural (n + 1) - . - -- foo :: Set '[Natural 0, Natural 1, Natural 3] - foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty)) - . - -- bar :: Set '[Natural 1, Natural 2] - bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty)) - . - -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3] - foobar = foo `union` bar - . - @ - Note the types here are all inferred. +description: + This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level + finite maps via 'Map', with value-level counterparts. + . + Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard + and Tomas Petricek (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation. + . + Here is a brief example for finite maps: + . + > + > import Data.Type.Map + > + > -- Specify how to combine duplicate key-value pairs for Int values + > type instance Combine Int Int = Int + > instance Combinable Int Int where + > combine x y = x + y + > + > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int] + > foo = Ext (Var :: (Var "x")) 2 + > $ Ext (Var :: (Var "z")) True + > $ Ext (Var :: (Var "w")) 5 + > $ Empty + > + > bar :: Map '["y" :-> Int, "w" :-> Int] + > bar = Ext (Var :: (Var "y")) 3 + > $ Ext (Var :: (Var "w")) 1 + > $ Empty + > + > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool] + > foobar = foo `union` bar + . + The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates). + The type signatures is commented out as it can be infered. Running the example we get: + . + > >>> foobar + > {w :-> 6, x :-> 2, y :-> 3, z :-> True} + . + Thus, we see that the values for \"w\" are added together. + For sets, here is an example: + . + > import GHC.TypeLits + > import Data.Type.Set + > type instance Cmp (Natural n) (Natural m) = CmpNat n m + > + > data Natural (a :: Nat) where + > Z :: Natural 0 + > S :: Natural n -> Natural (n + 1) + > + > -- foo :: Set '[Natural 0, Natural 1, Natural 3] + > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty)) + > + > -- bar :: Set '[Natural 1, Natural 2] + > bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty)) + > + > -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3] + > foobar = foo `union` bar + . + Note the types here are all inferred. + . license: BSD3 license-file: LICENSE category: Type System, Data Structures