Update to GHC 9.8.4 and use rearrangements to simplify value-level implementations

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

src/Data/Type/Set.hs

@@ -1,17 +1,19 @@
 {-# 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
 
 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 -}
 

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: {}

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