type-level-sets 0.8.7.0 → 0.8.9.0
raw patch · 4 files changed
+52/−26 lines, 4 filesdep ~base
Dependency ranges changed: base
Files
- example2.hs +9/−0
- src/Data/Type/Map.hs +14/−4
- src/Data/Type/Set.hs +13/−6
- type-level-sets.cabal +16/−16
example2.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}+{-# LANGUAGE FlexibleContexts #-} import GHC.TypeLits import Data.Type.Set@@ -19,3 +20,11 @@ -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3] foobar = foo `union` bar++nonMemberTest :: NonMember (Natural 0) as => Set as -> ()+nonMemberTest set = ()++-- nonMemberTest meep is well typed+meep = asSet $ Ext (S Z) (Ext (S (S Z)) Empty)+-- nonMemberTest morp is ill typed+morp = asSet $ Ext (S Z) (Ext (S (S Z)) (Ext Z Empty))
src/Data/Type/Map.hs view
@@ -100,9 +100,13 @@ 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+-- instance Updatable v t '[] '[v ':-> t] where+-- update Empty v x = Ext v x Empty +instance Updatable v t s ((v ':-> t) ': s) where+ update xs v x = Ext v x xs++ {-| Predicate to check if in normalised map form -} type IsMap s = (s ~ Nub (Sort s)) @@ -129,8 +133,14 @@ instance Eq (Map '[]) where Empty == Empty = True -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'+instance (Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where+ (Ext Var v m) == (Ext Var v' m') = v == v' && m == m'++instance Ord (Map '[]) where+ compare Empty Empty = EQ++instance (Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) where+ compare (Ext Var v m) (Ext Var v' m') = compare v v' `mappend` compare m m' {-| Union of two finite maps (normalising) -} union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
src/Data/Type/Set.hs view
@@ -1,13 +1,13 @@ {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts, UndecidableInstances, ConstraintKinds,- ScopedTypeVariables #-}+ ScopedTypeVariables, TypeInType #-} module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..), Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..), Delete(..), Proxy(..), remove, Remove, (:\),- Member) where+ Member(..), NonMember, MemberP(..)) where import GHC.TypeLits import Data.Type.Bool@@ -16,7 +16,7 @@ data Proxy (p :: k) = Proxy -- Value-level 'Set' representation, essentially a list-data Set (n :: [k]) :: * where+data Set (n :: [k]) where {--| Construct an empty set -} Empty :: Set '[] {--| Extend a set with an element -}@@ -77,7 +77,7 @@ {-| Delete elements from a set -} type family (m :: [k]) :\ (x :: k) :: [k] where '[] :\ x = '[]- (x ': xs) :\ x = xs+ (x ': xs) :\ x = xs :\ x (y ': xs) :\ x = y ': (xs :\ x) class Remove s t where@@ -86,8 +86,8 @@ instance Remove '[] t where remove Empty Proxy = Empty -instance {-# OVERLAPS #-} Remove (x ': xs) x where- remove (Ext _ xs) Proxy = xs+instance {-# OVERLAPS #-} Remove xs x => Remove (x ': xs) x where+ remove (Ext _ xs) x@Proxy = remove xs x instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x) => Remove (y ': xs) x where@@ -227,3 +227,10 @@ instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where member a (Ext _ xs) = member a xs++type family MemberP a s :: Bool where+ MemberP a '[] = False+ MemberP a (a ': s) = True+ MemberP a (b ': s) = MemberP a s++type NonMember a s = MemberP a s ~ False
type-level-sets.cabal view
@@ -1,14 +1,14 @@ name: type-level-sets-version: 0.8.7.0+version: 0.8.9.0 synopsis: Type-level sets and finite maps (with value-level counterparts)-description: +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. + 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: + Here is a brief example for finite maps: . > > import Data.Type.Map@@ -19,26 +19,26 @@ > 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 + > 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 + > >>> foobar > {w :-> 6, x :-> 2, y :-> 3, z :-> True} .- Thus, we see that the values for \"w\" are added together. + Thus, we see that the values for \"w\" are added together. For sets, here is an example: . > import GHC.TypeLits@@ -48,7 +48,7 @@ > 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)) >@@ -63,13 +63,13 @@ license: BSD3 license-file: LICENSE category: Type System, Data Structures-copyright: 2013-16 University of Cambridge+copyright: 2013-18 University of Kent author: Dominic Orchard maintainer: Dominic Orchard stability: experimental build-type: Simple cabal-version: >= 1.6-tested-with: GHC >= 8.0.1+tested-with: GHC >= 8.2.2 extra-source-files: example.hs, example2.hs @@ -84,6 +84,6 @@ exposed-modules: Data.Type.Set Data.Type.Map- + build-depends: base < 5, ghc-prim