type-level-sets 0.8.0.0 → 0.8.5.0

raw patch · 2 files changed

+121/−83 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• src/Data/Type/Map.hs +61/−21
• type-level-sets.cabal +60/−62

@@ -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)  

@@ -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 <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (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 <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (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