diff --git a/src/Data/Type/Map.hs b/src/Data/Type/Map.hs index f74de7f..a5ed771 100644 --- a/src/Data/Type/Map.hs +++ b/src/Data/Type/Map.hs @@ -5,7 +5,7 @@ The implementation is similar to that shown in the paper. {-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures, TypeFamilies, UndecidableInstances, MultiParamTypeClasses, FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables, - ConstraintKinds, IncoherentInstances, FunctionalDependencies #-} + ConstraintKinds, FunctionalDependencies #-} module Data.Type.Map (Mapping(..), Union, Unionable, union, append, Var(..), Map(..), ext, empty, mapLength, @@ -21,6 +21,9 @@ import GHC.TypeLits import Data.Type.Bool import Data.Type.Equality import Data.Type.Set (Cmp, Proxy(..), Flag(..), Sort, Filter, Filter', (:++)) +import Data.Kind (Type) +import Rearrange.Rearrangeable +import Rearrange.Typeclass {- Throughout, type variables 'k' ranges over "keys" @@ -74,10 +77,15 @@ 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 +data Map (n :: [Mapping Symbol Type]) where Empty :: Map '[] Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m) +instance Rearrangeable Map where + rConsToHead (Ext x v _) = Ext x v + rTail (Ext _ _ xs) = xs + rEmpty = Empty + {-| Smart constructor which normalises the representation -} ext :: (Sortable ((k :-> v) ': m), Nubable (Sort ((k :-> v) ': m))) => Var k -> v -> Map m -> Map (AsMap ((k :-> v) ': m)) ext k v m = asMap $ Ext k v m @@ -128,7 +136,11 @@ type IsMap s = (s ~ Nub (Sort s)) {-| At the type level, normalise the list form to the map form -} type AsMap s = Nub (Sort s) -{-| At the value level, noramlise the list form to the map form -} +{-| At the value level, normalise the list form to the map form. + Note: in theory, this could be replaced with a call to rDel + mapping from a Map s to a Map (AsMap s). + However, nub must be used due to note [NubOrdering] + (in `Data.Type.Set`). -} asMap :: (Sortable s, Nubable (Sort s)) => Map s -> Map (AsMap s) asMap x = nub (quicksort x) @@ -172,57 +184,16 @@ 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 - -class FilterV' (f::Flag) k v k' v' xs (cmp :: Ordering) where - filterV' :: Proxy f -> Proxy cmp -> Var k -> v -> Var k' -> v' -> Map xs -> Map (Filter' f (k :-> v) (k' :-> v') xs cmp) - -instance FilterV' f k v k' v' xs (Cmp k' k) => FilterV f k v ((k' :-> v') ': xs) where - filterV _ _ v (Ext _ v' xs) = - filterV' (Proxy :: Proxy f) (Proxy :: Proxy (Cmp k' k)) (Var :: Var k) v (Var :: Var k') v' xs - -instance (FilterV 'FMin k v xs) => FilterV' FMin k v k' v' xs LT where - filterV' _ _ k v k' v' xs = Ext k' v' (filterV (Proxy :: Proxy FMin) k v xs) - -instance (FilterV 'FMin k v xs) => FilterV' FMin k v k' v' xs EQ where - filterV' _ _ k v k' v' xs = filterV (Proxy :: Proxy FMin) k v xs +type Sortable xs = Permute Map xs (Sort xs) -instance (FilterV 'FMin k v xs) => FilterV' FMin k v k' v' xs GT where - filterV' _ _ k v k' v' xs = filterV (Proxy :: Proxy FMin) k v xs - -instance (FilterV 'FMax k v xs) => FilterV' FMax k v k' v' xs LT where - filterV' _ _ k v k' v' xs = filterV (Proxy :: Proxy FMax) k v xs - -instance (FilterV 'FMax k v xs) => FilterV' FMax k v k' v' xs EQ where - filterV' _ _ k v k' v' xs = Ext k' v' (filterV (Proxy :: Proxy FMax) k v xs) - -instance (FilterV 'FMax k v xs) => FilterV' FMax k v k' v' xs GT where - filterV' _ _ k v k' v' xs = Ext k' v' (filterV (Proxy :: Proxy FMax) k v xs) +quicksort :: Sortable xs => Map xs -> Map (Sort xs) +quicksort = permute class Combinable t t' where combine :: t -> t' -> Combine t t' +{-| Value-level counterpart to the type-level 'Nub' + See the notes on `nub` in `Data.Type.Set`. -} class Nubable t where nub :: Map t -> Map (Nub t) @@ -242,36 +213,14 @@ instance {-# OVERLAPS #-} => Nubable ((k :-> v) ': (k :-> v') ': s) where nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s) - {-| Splitting a union of maps, given the maps we want to split it into -} -class Split s t st where - -- where st ~ Union s t - split :: Map st -> (Map s, Map t) - -instance Split '[] '[] '[] where - split Empty = (Empty, Empty) +type Split s t st = (RDel Map st s, RDel Map st t) -instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where - split (Ext k v st) = let (s, t) = split st - in (Ext k v s, Ext k v t) - -instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where - split (Ext k v st) = let (s, t) = split st - in (Ext k v s, t) - -instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where - split (Ext k v st) = let (s, t) = split st - in (s, Ext k v t) +split :: (Split s t st) => Map st -> (Map s, Map t) +split inp = (rDel inp, rDel inp) {-| Construct a submap 's' from a supermap 't' -} -class Submap s t where - submap :: Map t -> Map s - -instance Submap '[] '[] where - submap xs = Empty - -instance {-# OVERLAPPABLE #-} Submap s t => Submap s (x ': t) where - submap (Ext _ _ xs) = submap xs +type Submap s t = RDel Map t s -instance {-# OVERLAPS #-} Submap s t => Submap (x ': s) (x ': t) where - submap (Ext k v xs) = Ext k v (submap xs) +submap :: (Submap s t) => Map t -> Map s +submap = rDel \ No newline at end of file diff --git a/src/Data/Type/Set.hs b/src/Data/Type/Set.hs index 2595320..d80b114 100644 --- a/src/Data/Type/Set.hs +++ b/src/Data/Type/Set.hs @@ -1,10 +1,10 @@ {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts, UndecidableInstances, ConstraintKinds, - ScopedTypeVariables, TypeInType #-} + ScopedTypeVariables #-} module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, - Sort, Sortable, (:++), Split(..), Cmp, Filter, Filter', Flag(..), + Sort, Sortable, (:++), split, Split, Cmp, Filter, Filter', Flag(..), Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..), Delete(..), Proxy(..), remove, Remove, (:\), Elem(..), Member(..), MemberP, NonMember) where @@ -12,6 +12,8 @@ module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append, import GHC.TypeLits import Data.Type.Bool import Data.Type.Equality +import Rearrange.Rearrangeable +import Rearrange.Typeclass data Proxy (p :: k) = Proxy @@ -23,6 +25,15 @@ data Set (n :: [k]) where {--| Extend a set with an element -} Ext :: e -> Set s -> Set (e ': s) +instance Rearrangeable Set where + rConsToHead (Ext x _) = Ext x + rTail (Ext _ xs) = xs + rEmpty = Empty + +instance RearrangeableStar Set where + rCons = Ext + rHead (Ext x _) = x + instance Show (Set '[]) where show Empty = "{}" @@ -54,7 +65,10 @@ instance (Ord a, Ord (Set s)) => Ord (Set (a ': s)) where {-| At the type level, normalise the list form to the set form -} type AsSet s = Nub (Sort s) -{-| At the value level, noramlise the list form to the set form -} +{-| At the value level, normalise the list form to the set form. + Note: in theory, this could be replaced with a call to rDel + mapping from a Set s to a Set (AsSet s). + However, nub must be used due to note [NubOrdering]. -} asSet :: (Sortable s, Nubable (Sort s)) => Set s -> Set (AsSet s) asSet x = nub (quicksort x) @@ -77,8 +91,9 @@ type SetProperties (f :: [k]) = {-| Union of sets -} type Union s t = Nub (Sort (s :++ t)) +{- Note: nub must be used due to note [NubOrdering]. -} union :: (Unionable s t) => Set s -> Set t -> Set (Union s t) -union s t = nub (quicksort (append s t)) +union s t = nub $ quicksort (append s t) type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t))) @@ -113,24 +128,11 @@ instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x) remove (Ext y xs) (x@Proxy) = Ext y (remove xs x) {-| 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 - split :: Set st -> (Set s, Set t) - -instance Split '[] '[] '[] where - split Empty = (Empty, Empty) +type Split s t st = (RDel Set st s, RDel Set st t) -instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where - split (Ext x st) = let (s, t) = split st - in (Ext x s, Ext x t) - -instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where - split (Ext x st) = let (s, t) = split st - in (Ext x s, t) - -instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where - split (Ext x st) = let (s, t) = split st - in (s, Ext x t) +split :: (Split s t st) => + Set st -> (Set s, Set t) +split inp = (rDel inp, rDel inp) {-| Remove duplicates from a sorted list -} type family Nub t where @@ -141,7 +143,15 @@ type family Nub t where {-| Value-level counterpart to the type-level 'Nub' Note: the value-level case for equal types is not define here, - but should be given per-application, e.g., custom 'merging' behaviour may be required -} + but should be given per-application, e.g., custom 'merging' behaviour may be required. + Note: [NubOrdering] + rearrangements are not used here since the original behaviour of Nubable + assumes that if there are two equal elements, the later one is used. The + rearrangements library assumes the opposite, so they are incompatible. + Furthermore, a user could define a custom merging behaviour for nub which + would not be preserved by rDel. + There are some definitions which could be rewritten to use rDel if this + was not the case, such as asSet. -} class Nubable t where nub :: Set t -> Set (Nub t) @@ -159,20 +169,9 @@ instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)), Nubable (f ': s)) => Nubable (e ': f ': s) where nub (Ext e (Ext f s)) = Ext e (nub (Ext f s)) - -{-| Construct a subsetset 's' from a superset 't' -} -class Subset s t where - subset :: Set t -> Set s - -instance Subset '[] '[] where - subset xs = Empty - -instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where - subset (Ext _ xs) = subset xs - -instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where - subset (Ext x xs) = Ext x (subset xs) - +type Subset s t = RDel Set t s +subset :: (Subset s t) => Set t -> Set s +subset = rDel {-| Type-level quick sort for normalising the representation of sets -} type family Sort (xs :: [k]) :: [k] where @@ -201,48 +200,10 @@ 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) - -instance Sortable '[] where - quicksort Empty = Empty - -instance (Sortable (Filter FMin p xs), - Sortable (Filter FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable (p ': xs) where - quicksort (Ext p xs) = ((quicksort (less p xs)) `append` (Ext p Empty)) `append` (quicksort (more p 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) p xs where - filterV :: Proxy f -> p -> Set xs -> Set (Filter f p xs) - -class FilterV' (f::Flag) p x xs (cmp :: Ordering) where - filterV' :: Proxy f -> Proxy cmp -> p -> x -> Set xs -> Set (Filter' f p x xs cmp) - -instance FilterV f p '[] where - filterV _ p Empty = Empty - -instance FilterV' f p x xs (Cmp x p) => FilterV f p (x ': xs) where - filterV _ p (Ext x xs) = filterV' (Proxy :: Proxy f) (Proxy :: Proxy (Cmp x p)) p x xs - -instance (FilterV 'FMin p xs) => FilterV' FMin p x xs LT where - filterV' _ _ p x xs = Ext x (filterV (Proxy :: Proxy FMin) p xs) - -instance (FilterV 'FMin p xs) => FilterV' FMin p x xs EQ where - filterV' _ _ p x xs = filterV (Proxy :: Proxy FMin) p xs - -instance (FilterV 'FMin p xs) => FilterV' FMin p x xs GT where - filterV' _ _ p x xs = filterV (Proxy :: Proxy FMin) p xs - -instance (FilterV 'FMax p xs) => FilterV' FMax p x xs LT where - filterV' _ _ p x xs = filterV (Proxy :: Proxy FMax) p xs - -instance (FilterV 'FMax p xs) => FilterV' FMax p x xs EQ where - filterV' _ _ p x xs = Ext x (filterV (Proxy :: Proxy FMax) p xs) +type Sortable xs = Permute Set xs (Sort xs) -instance (FilterV 'FMax p xs) => FilterV' FMax p x xs GT where - filterV' _ _ p x xs = Ext x (filterV (Proxy :: Proxy FMax) p xs) +quicksort :: (Sortable xs) => Set xs -> Set (Sort xs) +quicksort = permute {-| Open-family for the ordering operation in the sort -} diff --git a/stack.yaml b/stack.yaml index b99651d..5d963fa 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,14 +1,16 @@ # For more information, see: https://github.com/commercialhaskell/stack/wiki/stack.yaml # Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2) -resolver: lts-18.10 +resolver: lts-23.10 # Local packages, usually specified by relative directory name packages: - '.' # Packages to be pulled from upstream that are not in the resolver (e.g., acme-missiles-0.3) -extra-deps: [] +extra-deps: +- git: https://github.com/finnbar/rearrangements.git + commit: 8c0767fba8522462588aa7815f4a9b4c7dd00d3e # Override default flag values for local packages and extra-deps flags: {} diff --git a/type-level-sets.cabal b/type-level-sets.cabal index 31701fe..a009b41 100644 --- a/type-level-sets.cabal +++ b/type-level-sets.cabal @@ -80,14 +80,15 @@ source-repository head library hs-source-dirs: src - other-extensions: TypeInType exposed-modules: Data.Type.Set Data.Type.Map build-depends: base < 5, - ghc-prim + ghc-prim, + rearrangements + default-language: Haskell2010 test-suite tests type: exitcode-stdio-1.0 @@ -100,7 +101,7 @@ test-suite tests MapSpec SetSpec build-tool-depends: - hspec-discover:hspec-discover >=2.7 && <2.10 + hspec-discover:hspec-discover build-depends: type-level-sets , hspec