diff --git a/ons-hs.cabal b/ons-hs.cabal index 32b07f8..bd7c3f8 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -17,9 +17,9 @@ library hs-source-dirs: src exposed-modules: EquivariantMap , EquivariantSet - , Orbit - , Orbit.Class - , Orbit.Products + , Nominal + , Nominal.Class + , Nominal.Products , OrbitList , Support , Support.Rat diff --git a/src/EquivariantMap.hs b/src/EquivariantMap.hs index 99fc06e..19db4ea 100644 --- a/src/EquivariantMap.hs +++ b/src/EquivariantMap.hs @@ -6,14 +6,12 @@ module EquivariantMap where -import Data.Set (Set) -import qualified Data.Set as Set import Data.Semigroup (Semigroup) import Data.Map (Map) import qualified Data.Map as Map import EquivariantSet (EquivariantSet(EqSet)) -import Orbit +import Nominal import Support -- TODO: foldable / traversable @@ -27,31 +25,31 @@ import Support -- thing is that we have to store which values are preserved under a map. This -- is done with the list of bit vector. Otherwise, it is an orbit-wise -- representation, just like sets. -newtype EquivariantMap k v = EqMap { unEqMap :: Map (Orb k) (Orb v, [Bool]) } +newtype EquivariantMap k v = EqMap { unEqMap :: Map (Orbit k) (Orbit v, [Bool]) } -- Need undecidableIntances for this -deriving instance (Eq (Orb k), Eq (Orb v)) => Eq (EquivariantMap k v) -deriving instance (Ord (Orb k), Ord (Orb v)) => Ord (EquivariantMap k v) -deriving instance (Show (Orb k), Show (Orb v)) => Show (EquivariantMap k v) +deriving instance (Eq (Orbit k), Eq (Orbit v)) => Eq (EquivariantMap k v) +deriving instance (Ord (Orbit k), Ord (Orbit v)) => Ord (EquivariantMap k v) +deriving instance (Show (Orbit k), Show (Orbit v)) => Show (EquivariantMap k v) -- Left biased... -deriving instance Ord (Orb k) => Monoid (EquivariantMap k v) -deriving instance Ord (Orb k) => Semigroup (EquivariantMap k v) +deriving instance Ord (Orbit k) => Monoid (EquivariantMap k v) +deriving instance Ord (Orbit k) => Semigroup (EquivariantMap k v) -- Helper functions -mapel :: (Orbit k, Orbit v) => k -> v -> (Orb v, [Bool]) +mapel :: (Nominal k, Nominal v) => k -> v -> (Orbit v, [Bool]) mapel k v = (toOrbit v, bv (Support.toList (support k)) (Support.toList (support v))) bv :: [Rat] -> [Rat] -> [Bool] bv l [] = replicate (length l) False -bv [] l = error "Non-equivariant function" +bv [] _ = error "Non-equivariant function" bv (x:xs) (y:ys) = case compare x y of LT -> False : bv xs (y:ys) EQ -> True : bv xs ys GT -> error "Non-equivariant function" -mapelInv :: (Orbit k, Orbit v) => k -> (Orb v, [Bool]) -> v +mapelInv :: (Nominal k, Nominal v) => k -> (Orbit v, [Bool]) -> v mapelInv x (oy, bv) = getElement oy (Support.fromDistinctAscList . fmap fst . Prelude.filter snd $ zip (Support.toList (support x)) bv) @@ -60,10 +58,10 @@ mapelInv x (oy, bv) = getElement oy (Support.fromDistinctAscList . fmap fst . Pr null :: EquivariantMap k v -> Bool null (EqMap m) = Map.null m -member :: (Orbit k, Ord (Orb k)) => k -> EquivariantMap k v -> Bool +member :: (Nominal k, Ord (Orbit k)) => k -> EquivariantMap k v -> Bool member x (EqMap m) = Map.member (toOrbit x) m -lookup :: (Orbit k, Ord (Orb k), Orbit v) => k -> EquivariantMap k v -> Maybe v +lookup :: (Nominal k, Ord (Orbit k), Nominal v) => k -> EquivariantMap k v -> Maybe v lookup x (EqMap m) = mapelInv x <$> Map.lookup (toOrbit x) m @@ -72,13 +70,13 @@ lookup x (EqMap m) = mapelInv x <$> Map.lookup (toOrbit x) m empty :: EquivariantMap k v empty = EqMap Map.empty -singleton :: (Orbit k, Orbit v) => k -> v -> EquivariantMap k v +singleton :: (Nominal k, Nominal v) => k -> v -> EquivariantMap k v singleton k v = EqMap (Map.singleton (toOrbit k) (mapel k v)) -insert :: (Orbit k, Orbit v, Ord (Orb k)) => k -> v -> EquivariantMap k v -> EquivariantMap k v +insert :: (Nominal k, Nominal v, Ord (Orbit k)) => k -> v -> EquivariantMap k v -> EquivariantMap k v insert k v (EqMap m) = EqMap (Map.insert (toOrbit k) (mapel k v) m) -delete :: (Orbit k, Ord (Orb k)) => k -> EquivariantMap k v -> EquivariantMap k v +delete :: (Nominal k, Ord (Orbit k)) => k -> EquivariantMap k v -> EquivariantMap k v delete k (EqMap m) = EqMap (Map.delete (toOrbit k) m) @@ -87,22 +85,22 @@ delete k (EqMap m) = EqMap (Map.delete (toOrbit k) m) -- Can be done with just Map.unionWith and without getElementE but is a bit -- harder (probably easier). Also true for related functions -- op should be equivariant! -unionWith :: forall k v. (Orbit k, Orbit v, Ord (Orb k)) => (v -> v -> v) -> EquivariantMap k v -> EquivariantMap k v -> EquivariantMap k v +unionWith :: forall k v. (Nominal k, Nominal v, Ord (Orbit k)) => (v -> v -> v) -> EquivariantMap k v -> EquivariantMap k v -> EquivariantMap k v unionWith op (EqMap m1) (EqMap m2) = EqMap (Map.unionWithKey opl m1 m2) where opl ko p1 p2 = let k = getElementE ko :: k in mapel k (mapelInv k p1 `op` mapelInv k p2) -intersectionWith :: forall k v1 v2 v3. (Orbit k, Orbit v1, Orbit v2, Orbit v3, Ord (Orb k)) => (v1 -> v2 -> v3) -> EquivariantMap k v1 -> EquivariantMap k v2 -> EquivariantMap k v3 +intersectionWith :: forall k v1 v2 v3. (Nominal k, Nominal v1, Nominal v2, Nominal v3, Ord (Orbit k)) => (v1 -> v2 -> v3) -> EquivariantMap k v1 -> EquivariantMap k v2 -> EquivariantMap k v3 intersectionWith op (EqMap m1) (EqMap m2) = EqMap (Map.intersectionWithKey opl m1 m2) where opl ko p1 p2 = let k = getElementE ko :: k in mapel k (mapelInv k p1 `op` mapelInv k p2) -- Traversal -- f should be equivariant -map :: forall k v1 v2. (Orbit k, Orbit v1, Orbit v2) => (v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2 +map :: forall k v1 v2. (Nominal k, Nominal v1, Nominal v2) => (v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2 map f (EqMap m) = EqMap (Map.mapWithKey f2 m) where f2 ko p1 = let k = getElementE ko :: k in mapel k (f $ mapelInv k p1) -mapWithKey :: (Orbit k, Orbit v1, Orbit v2) => (k -> v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2 +mapWithKey :: (Nominal k, Nominal v1, Nominal v2) => (k -> v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2 mapWithKey f (EqMap m) = EqMap (Map.mapWithKey f2 m) where f2 ko p1 = let k = getElementE ko in mapel k (f k $ mapelInv k p1) @@ -111,13 +109,13 @@ mapWithKey f (EqMap m) = EqMap (Map.mapWithKey f2 m) keysSet :: EquivariantMap k v -> EquivariantSet k keysSet (EqMap m) = EqSet (Map.keysSet m) -fromSet :: (Orbit k, Orbit v) => (k -> v) -> EquivariantSet k -> EquivariantMap k v +fromSet :: (Nominal k, Nominal v) => (k -> v) -> EquivariantSet k -> EquivariantMap k v fromSet f (EqSet s) = EqMap (Map.fromSet f2 s) where f2 ko = let k = getElementE ko in mapel k (f k) -- Filter -filter :: forall k v. (Orbit k, Orbit v) => (v -> Bool) -> EquivariantMap k v -> EquivariantMap k v +filter :: forall k v. (Nominal k, Nominal v) => (v -> Bool) -> EquivariantMap k v -> EquivariantMap k v filter p (EqMap m) = EqMap (Map.filterWithKey p2 m) where p2 ko pr = let k = getElementE ko :: k in p $ mapelInv k pr diff --git a/src/EquivariantSet.hs b/src/EquivariantSet.hs index c9120d7..489f89c 100644 --- a/src/EquivariantSet.hs +++ b/src/EquivariantSet.hs @@ -13,7 +13,8 @@ import Data.Set (Set) import qualified Data.Set as Set import Prelude hiding (map, product) -import Orbit +import Nominal +import OrbitList (OrbitList(..)) -- Given a nominal type, we can construct equivariant sets. These simply use a @@ -22,20 +23,20 @@ import Orbit -- will always work directly with elements. This way we model infinite sets. -- Note that functions such as toList do not return an ordered list since the -- representatives are chosen arbitrarily. -newtype EquivariantSet a = EqSet { unEqSet :: Set (Orb a) } +newtype EquivariantSet a = EqSet { unEqSet :: Set (Orbit a) } -- Need undecidableIntances for this -deriving instance Eq (Orb a) => Eq (EquivariantSet a) -deriving instance Ord (Orb a) => Ord (EquivariantSet a) -deriving instance Show (Orb a) => Show (EquivariantSet a) +deriving instance Eq (Orbit a) => Eq (EquivariantSet a) +deriving instance Ord (Orbit a) => Ord (EquivariantSet a) +deriving instance Show (Orbit a) => Show (EquivariantSet a) -- For these we rely on the instances of Set -- It defines the join semi-lattice structure -deriving instance Ord (Orb a) => Monoid (EquivariantSet a) -deriving instance Ord (Orb a) => Semigroup (EquivariantSet a) +deriving instance Ord (Orbit a) => Monoid (EquivariantSet a) +deriving instance Ord (Orbit a) => Semigroup (EquivariantSet a) -- This action is trivial, since equivariant sets are equivariant -deriving via (Trivial (EquivariantSet a)) instance Orbit (EquivariantSet a) +deriving via (Trivial (EquivariantSet a)) instance Nominal (EquivariantSet a) -- Query @@ -46,10 +47,10 @@ null = Set.null . unEqSet orbits :: EquivariantSet a -> Int orbits = Set.size . unEqSet -member :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> Bool +member :: (Nominal a, Ord (Orbit a)) => a -> EquivariantSet a -> Bool member a = Set.member (toOrbit a) . unEqSet -isSubsetOf :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> Bool +isSubsetOf :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> Bool isSubsetOf (EqSet s1) (EqSet s2) = Set.isSubsetOf s1 s2 @@ -58,86 +59,86 @@ isSubsetOf (EqSet s1) (EqSet s2) = Set.isSubsetOf s1 s2 empty :: EquivariantSet a empty = EqSet Set.empty -singleOrbit :: Orbit a => a -> EquivariantSet a +singleOrbit :: Nominal a => a -> EquivariantSet a singleOrbit = EqSet . Set.singleton . toOrbit -- Insert whole orbit of a -insert :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> EquivariantSet a +insert :: (Nominal a, Ord (Orbit a)) => a -> EquivariantSet a -> EquivariantSet a insert a = EqSet . Set.insert (toOrbit a) . unEqSet -- Deletes whole orbit of a -delete :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> EquivariantSet a +delete :: (Nominal a, Ord (Orbit a)) => a -> EquivariantSet a -> EquivariantSet a delete a = EqSet . Set.delete (toOrbit a) . unEqSet -- Combine -union :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a +union :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a union a b = EqSet $ Set.union (unEqSet a) (unEqSet b) -- Not symmetric, but A \ B -difference :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a +difference :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a difference a b = EqSet $ Set.difference (unEqSet a) (unEqSet b) -intersection :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a +intersection :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a intersection a b = EqSet $ Set.intersection (unEqSet a) (unEqSet b) -- Cartesian product. This is a non trivial thing and relies on the -- ordering of Orbit.product. -product :: forall a b. (Orbit a, Orbit b) => EquivariantSet a -> EquivariantSet b -> EquivariantSet (a, b) +product :: forall a b. (Nominal a, Nominal b) => EquivariantSet a -> EquivariantSet b -> EquivariantSet (a, b) product (EqSet sa) (EqSet sb) = EqSet . Set.fromDistinctAscList . concat - $ Orbit.product (Proxy @a) (Proxy @b) <$> Set.toAscList sa <*> Set.toAscList sb + $ Nominal.product (Proxy @a) (Proxy @b) <$> Set.toAscList sa <*> Set.toAscList sb -- Cartesian product followed by a function (f should be equivariant) -productWith :: (Orbit a, Orbit b, Orbit c, Ord (Orb c)) => (a -> b -> c) -> EquivariantSet a -> EquivariantSet b -> EquivariantSet c +productWith :: (Nominal a, Nominal b, Nominal c, Ord (Orbit c)) => (a -> b -> c) -> EquivariantSet a -> EquivariantSet b -> EquivariantSet c productWith f as bs = map (uncurry f) $ EquivariantSet.product as bs -- Filter -- f should be equivariant -filter :: Orbit a => (a -> Bool) -> EquivariantSet a -> EquivariantSet a +filter :: Nominal a => (a -> Bool) -> EquivariantSet a -> EquivariantSet a filter f (EqSet s) = EqSet . Set.filter (f . getElementE) $ s -- f should be equivariant -partition :: Orbit a => (a -> Bool) -> EquivariantSet a -> (EquivariantSet a, EquivariantSet a) +partition :: Nominal a => (a -> Bool) -> EquivariantSet a -> (EquivariantSet a, EquivariantSet a) partition f (EqSet s) = both EqSet . Set.partition (f . getElementE) $ s - where both f (a, b) = (f a, f b) + where both g (a, b) = (g a, g b) -- Map -- precondition: f is equivariant -- Note that f may change the ordering -map :: (Orbit a, Orbit b, Ord (Orb b)) => (a -> b) -> EquivariantSet a -> EquivariantSet b +map :: (Nominal a, Nominal b, Ord (Orbit b)) => (a -> b) -> EquivariantSet a -> EquivariantSet b map f = EqSet . Set.map (omap f) . unEqSet -- precondition: f quivariant and preserves order on the orbits. -- This means you should know the representation to use it well -mapMonotonic :: (Orbit a, Orbit b) => (a -> b) -> EquivariantSet a -> EquivariantSet b +mapMonotonic :: (Nominal a, Nominal b) => (a -> b) -> EquivariantSet a -> EquivariantSet b mapMonotonic f = EqSet . Set.mapMonotonic (omap f) . unEqSet -- Folds -- I am not sure about the preconditions for folds -foldr :: Orbit a => (a -> b -> b) -> b -> EquivariantSet a -> b +foldr :: Nominal a => (a -> b -> b) -> b -> EquivariantSet a -> b foldr f b = Set.foldr (f . getElementE) b . unEqSet -foldl :: Orbit a => (b -> a -> b) -> b -> EquivariantSet a -> b -foldl f b = Set.foldl (\b -> f b . getElementE) b . unEqSet +foldl :: Nominal a => (b -> a -> b) -> b -> EquivariantSet a -> b +foldl f b = Set.foldl (\acc -> f acc . getElementE) b . unEqSet -- Conversion -toList :: Orbit a => EquivariantSet a -> [a] +toList :: Nominal a => EquivariantSet a -> [a] toList = fmap getElementE . Set.toList . unEqSet -fromList :: (Orbit a, Ord (Orb a)) => [a] -> EquivariantSet a +fromList :: (Nominal a, Ord (Orbit a)) => [a] -> EquivariantSet a fromList = EqSet . Set.fromList . fmap toOrbit -toOrbitList :: EquivariantSet a -> [Orb a] -toOrbitList = Set.toList . unEqSet +toOrbitList :: EquivariantSet a -> OrbitList a +toOrbitList = OrbitList . Set.toList . unEqSet -fromOrbitList :: Ord (Orb a) => [Orb a] -> EquivariantSet a -fromOrbitList = EqSet . Set.fromList +fromOrbitList :: Ord (Orbit a) => OrbitList a -> EquivariantSet a +fromOrbitList = EqSet . Set.fromList . unOrbitList diff --git a/src/Nominal.hs b/src/Nominal.hs new file mode 100644 index 0000000..45e0b27 --- /dev/null +++ b/src/Nominal.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Nominal + ( module Nominal + , module Nominal.Class + ) where + +import Data.Proxy + +import Nominal.Products +import Nominal.Class +import Support (def) + + +-- We can get 'default' values, if we don't care about the support. +getElementE :: forall a. Nominal a => Orbit a -> a +getElementE orb = getElement orb (def (index (Proxy :: Proxy a) orb)) + +-- We can `map` orbits to orbits for equivariant functions +omap :: (Nominal a, Nominal b) => (a -> b) -> Orbit a -> Orbit b +omap f = toOrbit . f . getElementE + +-- Enumerate all orbits in a product A x B. In lexicographical order! +product :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] +product pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> prodStrings (index pa oa) (index pb ob) + +-- Separated product: A * B = { (a,b) | Exist C1, C2 disjoint supporting a, b resp.} +separatedProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] +separatedProduct pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> sepProdStrings (index pa oa) (index pb ob) + +-- "Left product": A |x B = { (a,b) | C supports a => C supports b } +leftProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a,b)] +leftProduct pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> rincProdStrings (index pa oa) (index pb ob) + +{-# INLINABLE product #-} +{-# INLINABLE separatedProduct #-} +{-# INLINABLE leftProduct #-} + diff --git a/src/Nominal/Class.hs b/src/Nominal/Class.hs new file mode 100644 index 0000000..de5f5a6 --- /dev/null +++ b/src/Nominal/Class.hs @@ -0,0 +1,223 @@ +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Nominal.Class + ( Nominal(..) -- typeclass + , Trivial(..) -- newtype wrapper for deriving instances + , Generic(..) -- newtype wrapper for deriving instances + , OrbPair(..) -- need to export? + , OrbRec(..) -- need to export? + ) where + +import Data.Void +import Data.Proxy (Proxy(..)) +import GHC.Generics hiding (Generic) +import qualified GHC.Generics as GHC (Generic) + +import Support + + +-- This is the main meat of the package. The Orbit typeclass, it gives us ways +-- to manipulate nominal elements in sets and maps. The type class has +-- associated data to represent an orbit of type a. This is often much easier +-- than the type a itself. For example, all orbits of Rat are equal. +-- Furthermore, we provide means to go back and forth between elements and +-- orbits, and we get to know their support size. For many manipulations we +-- need an Ord instance on the associated data type, this can often be +-- implemented, even when the type 'a' does not have an Ord instance. +-- +-- Laws / conditions: +-- * index . toOrbit == size . support +-- * getElement o s is defined if index o == Set.size s +class Nominal a where + type Orbit a :: * + toOrbit :: a -> Orbit a + support :: a -> Support + getElement :: Orbit a -> Support -> a + index :: Proxy a -> Orbit a -> Int + + +-- We can construct orbits from rational numbers. There is exactly one orbit, +-- so this can be represented by the unit type. +instance Nominal Rat where + type Orbit Rat = () + toOrbit _ = () + support r = Support.singleton r + getElement _ s = Support.min s + index _ _ = 1 + + +-- Supports themselves are nominal. Note that this is a very important instance +-- as all other instances can reduce to this one (and perhaps the one for +-- products). 'Abstract types' in the original ONS library can be represented +-- directly as T = (Trivial Int, Support). The orbit of a given support is +-- completely specified by an integer. +instance Nominal Support where + type Orbit Support = Int + toOrbit s = Support.size s + support s = s + getElement _ s = s + index _ n = n + + +-- Two general ways for deriving instances are provided: +-- 1. A trivial instance, where the group action is trivial. This means that +-- each value is its own orbit and is supported by the empty set. +-- 2. A generic instance, this uses the GHC.Generis machinery. This will +-- derive ``the right'' instance based on the algebraic data type. +-- Neither of them is a default, so they should be derived using DerivingVia. +-- (Available from GHC 8.6.1.) Example of both: +-- deriving via (Trivial Bool) instance Orbit Bool +-- deriving via (Generic (a, b)) instance (Orbit a, Orbit b) => Orbit (a, b) + +-- For the trivial action, each element is its own orbit and is supported +-- by the empty set. +newtype Trivial a = Trivial { unTrivial :: a } +instance Nominal (Trivial a) where + type Orbit (Trivial a) = a + toOrbit (Trivial a) = a + support _ = Support.empty + getElement a _ = Trivial a + index _ _ = 0 + + +-- We can now define trivial instances for some basic types. (Some of these +-- could equivalently be derived with generics.) +deriving via (Trivial Void) instance Nominal Void +deriving via (Trivial ()) instance Nominal () +deriving via (Trivial Bool) instance Nominal Bool +deriving via (Trivial Char) instance Nominal Char +deriving via (Trivial Ordering) instance Nominal Ordering + + +-- The generic instance unfolds the algebraic data type in sums and products, +-- these have their own instances defined below. +newtype Generic a = Generic { unGeneric :: a } +instance (GHC.Generic a, GNominal (Rep a)) => Nominal (Generic a) where + type Orbit (Generic a) = GOrbit (Rep a) + toOrbit = gtoOrbit . from . unGeneric + support = gsupport . from . unGeneric + getElement o s = Generic (to (ggetElement o s)) + index _ = gindex (Proxy :: Proxy (Rep a)) + + +-- Some instances we can derive via generics +deriving via (Generic (a, b)) instance (Nominal a, Nominal b) => Nominal (a, b) +deriving via (Generic (a, b, c)) instance (Nominal a, Nominal b, Nominal c) => Nominal (a, b, c) +deriving via (Generic (a, b, c, d)) instance (Nominal a, Nominal b, Nominal c, Nominal d) => Nominal (a, b, c, d) + +deriving via (Generic (Either a b)) instance (Nominal a, Nominal b) => Nominal (Either a b) + +deriving via (Generic [a]) instance Nominal a => Nominal [a] +deriving via (Generic (Maybe a)) instance Nominal a => Nominal (Maybe a) + + +-- Generic class, so that custom data types can be derived +class GNominal f where + type GOrbit f :: * + gtoOrbit :: f a -> GOrbit f + gsupport :: f a -> Support + ggetElement :: GOrbit f -> Support -> f a + gindex :: Proxy f -> GOrbit f -> Int + + +-- Instance for the Void type +instance GNominal V1 where + type GOrbit V1 = Void + gtoOrbit _ = undefined + gsupport _ = empty + ggetElement _ _ = undefined + gindex _ _ = 0 + + +-- Instance for the Uni type +instance GNominal U1 where + type GOrbit U1 = () + gtoOrbit _ = () + gsupport _ = empty + ggetElement _ _ = U1 + gindex _ _ = 0 + + +-- Disjoint unions are easy: just work on either side. +instance (GNominal f, GNominal g) => GNominal (f :+: g) where + type GOrbit (f :+: g) = Either (GOrbit f) (GOrbit g) + gtoOrbit (L1 a) = Left (gtoOrbit a) + gtoOrbit (R1 b) = Right (gtoOrbit b) + gsupport (L1 a) = gsupport a + gsupport (R1 b) = gsupport b + ggetElement (Left oa) s = L1 (ggetElement oa s) + ggetElement (Right ob) s = R1 (ggetElement ob s) + gindex proxy (Left oa) = gindex (left proxy) oa where + left :: proxy (f :+: g) -> Proxy f + left _ = Proxy + gindex proxy (Right ob) = gindex (right proxy) ob where + right :: proxy (f :+: g) -> Proxy g + right _ = Proxy + + +-- The cartesian product is a non-trivial instance. We represent orbits in a +-- product as described inthe paper: with two orbits, and how the match. The +-- matchings can be given as strings, which can be easily enumerated, in order +-- to enumerate the whole product. +instance (GNominal f, GNominal g) => GNominal (f :*: g) where + type GOrbit (f :*: g) = OrbPair (GOrbit f) (GOrbit g) + gtoOrbit ~(a :*: b) = OrbPair (gtoOrbit a) (gtoOrbit b) (bla sa sb) + where + sa = toList $ gsupport a + sb = toList $ gsupport b + bla [] ys = fmap (const GT) ys + bla xs [] = fmap (const LT) xs + bla (x:xs) (y:ys) = case compare x y of + LT -> LT : (bla xs (y:ys)) + EQ -> EQ : (bla xs ys) + GT -> GT : (bla (x:xs) ys) + gsupport ~(a :*: b) = (gsupport a) `union` (gsupport b) + ggetElement (OrbPair oa ob l) s = (ggetElement oa $ toSet ls) :*: (ggetElement ob $ toSet rs) + where + ~(ls, rs) = partitionOrd fst . zip l . toList $ s + toSet = fromDistinctAscList . fmap snd + gindex _ (OrbPair _ _ l) = length l + +data OrbPair a b = OrbPair !a !b ![Ordering] + deriving (Eq, Ord, Show, GHC.Generic) + +-- Could be in prelude or some other general purpose lib +partitionOrd :: (a -> Ordering) -> [a] -> ([a], [a]) +partitionOrd p xs = foldr (selectOrd p) ([], []) xs + +selectOrd :: (a -> Ordering) -> a -> ([a], [a]) -> ([a], [a]) +selectOrd f x ~(ls, rs) = case f x of + LT -> (x : ls, rs) + EQ -> (x : ls, x : rs) + GT -> (ls, x : rs) + + +instance Nominal a => GNominal (K1 c a) where + -- Cannot use (Orb a) here, that may lead to a recursive type + -- So we use the type OrbRec a instead (which uses Orb a one step later). + type GOrbit (K1 c a) = OrbRec a + gtoOrbit (K1 x) = OrbRec (toOrbit x) + gsupport (K1 x) = support x + ggetElement (OrbRec x) s = K1 $ getElement x s + gindex _ (OrbRec o) = index (Proxy :: Proxy a) o + +newtype OrbRec a = OrbRec (Orbit a) + deriving GHC.Generic +deriving instance Eq (Orbit a) => Eq (OrbRec a) +deriving instance Ord (Orbit a) => Ord (OrbRec a) +deriving instance Show (Orbit a) => Show (OrbRec a) + + +instance GNominal f => GNominal (M1 i c f) where + type GOrbit (M1 i c f) = GOrbit f + gtoOrbit (M1 x) = gtoOrbit x + gsupport (M1 x) = gsupport x + ggetElement x s = M1 $ ggetElement x s + gindex _ o = gindex (Proxy :: Proxy f) o diff --git a/src/Orbit/Products.hs b/src/Nominal/Products.hs similarity index 97% rename from src/Orbit/Products.hs rename to src/Nominal/Products.hs index f0be39f..35a0566 100644 --- a/src/Orbit/Products.hs +++ b/src/Nominal/Products.hs @@ -1,4 +1,4 @@ -module Orbit.Products where +module Nominal.Products where import Control.Applicative import Data.MemoTrie diff --git a/src/Orbit.hs b/src/Orbit.hs deleted file mode 100644 index bddb502..0000000 --- a/src/Orbit.hs +++ /dev/null @@ -1,78 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} - -module Orbit - ( module Orbit - , module Orbit.Class - ) where - -import Data.Proxy - -import Support (Support, Rat(..)) -import qualified Support - -import Orbit.Products -import Orbit.Class - - --- We can get 'default' values, if we don't care about the support. -getElementE :: forall a. Orbit a => Orb a -> a -getElementE orb = getElement orb (Support.def (index (Proxy :: Proxy a) orb)) - --- We can `map` orbits to orbits for equivariant functions -omap :: (Orbit a, Orbit b) => (a -> b) -> Orb a -> Orb b -omap f = toOrbit . f . getElementE - --- We can construct orbits from rational numbers. There is exactly one orbit, --- so this can be represented by the unit type. -instance Orbit Rat where - type Orb Rat = () - toOrbit _ = () - support r = Support.singleton r - getElement _ s = Support.min s - index _ _ = 1 - - --- Supports themselves are nominal. Note that this is a very important instance --- as all other instances can reduce to this one (and perhaps the one for --- products). 'Abstract types' in the original ONS library can be represented --- directly as T = (Trivial Int, Support). The orbit of a given support is --- completely specified by an integer. -instance Orbit Support where - type Orb Support = Int - toOrbit s = Support.size s - support s = s - getElement _ s = s - index _ n = n - - --- Some instances we can derive via generics -deriving instance (Orbit a, Orbit b) => Orbit (Either a b) - -deriving instance Orbit () -deriving instance (Orbit a, Orbit b) => Orbit (a, b) -deriving instance (Orbit a, Orbit b, Orbit c) => Orbit (a, b, c) -deriving instance (Orbit a, Orbit b, Orbit c, Orbit d) => Orbit (a, b, c, d) - -deriving instance Orbit a => Orbit [a] -deriving instance Orbit a => Orbit (Maybe a) - - --- Enumerate all orbits in a product A x B. In lexicographical order! -product :: (Orbit a, Orbit b) => Proxy a -> Proxy b -> Orb a -> Orb b -> [Orb (a,b)] -product pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> prodStrings (index pa oa) (index pb ob) - --- Separated product: A * B = { (a,b) | Exist C1, C2 disjoint supporting a, b resp.} -separatedProduct :: (Orbit a, Orbit b) => Proxy a -> Proxy b -> Orb a -> Orb b -> [Orb (a,b)] -separatedProduct pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> sepProdStrings (index pa oa) (index pb ob) - --- "Left product": A |x B = { (a,b) | C supports a => C supports b } -leftProduct :: (Orbit a, Orbit b) => Proxy a -> Proxy b -> Orb a -> Orb b -> [Orb (a,b)] -leftProduct pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> rincProdStrings (index pa oa) (index pb ob) - -{-# INLINABLE product #-} -{-# INLINABLE separatedProduct #-} -{-# INLINABLE leftProduct #-} - diff --git a/src/Orbit/Class.hs b/src/Orbit/Class.hs deleted file mode 100644 index b806154..0000000 --- a/src/Orbit/Class.hs +++ /dev/null @@ -1,183 +0,0 @@ -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -module Orbit.Class where - -import Data.Void -import Data.Proxy (Proxy(..)) -import GHC.Generics - -import Support - --- This is the main meat of the package. The Orbit typeclass, it gives us ways --- to manipulate nominal elements in sets and maps. The type class has --- associated data to represent an orbit of type a. This is often much easier --- than the type a itself. For example, all orbits of Rat are equal. --- Furthermore, we provide means to go back and forth between elements and --- orbits, and we get to know their support size. For many manipulations we --- need an Ord instance on the associated data type, this can often be --- implemented, even when the type 'a' does not have an Ord instance. --- --- Laws / conditions: --- * index . toOrbit == size . support --- * getElement o s is defined if index o == Set.size s -class Orbit a where - type Orb a :: * - toOrbit :: a -> Orb a - support :: a -> Support - getElement :: Orb a -> Support -> a - index :: Proxy a -> Orb a -> Int - - -- We provide default implementations for generic types - -- This enables us to derive Orbit instances by the Haskell compiler - -- default Orb a :: (Generic a, GOrbit (Rep a)) => * - type Orb a = GOrb (Rep a) - - default toOrbit :: (Generic a, GOrbit (Rep a), Orb a ~ GOrb (Rep a)) => a -> Orb a - toOrbit = gtoOrbit . from - - default support :: (Generic a, GOrbit (Rep a), Orb a ~ GOrb (Rep a)) => a -> Support - support = gsupport . from - - default getElement :: (Generic a, GOrbit (Rep a), Orb a ~ GOrb (Rep a)) => Orb a -> Support -> a - getElement o s = to (ggetElement o s) - - default index :: (Generic a, GOrbit (Rep a), Orb a ~ GOrb (Rep a)) => Proxy a -> Orb a -> Int - index _ = gindex (Proxy :: Proxy (Rep a)) - - {-# INLINABLE toOrbit #-} - {-# INLINABLE support #-} - {-# INLINABLE getElement #-} - {-# INLINABLE index #-} - - --- Data structure for the discrete nominal sets with a trivial action. -newtype Trivial a = Trivial { unTrivial :: a } - deriving (Eq, Ord, Show) - --- For the trivial action, each element is its own orbit and is supported --- by the empty set. -instance Orbit (Trivial a) where - type Orb (Trivial a) = a - toOrbit (Trivial a) = a - support _ = Support.empty - getElement a _ = Trivial a - index _ _ = 0 - - --- We can now define trivial instances for some basic types. --- This uses a new Haskell extension (ghc 8.6.1) -deriving via (Trivial Bool) instance Orbit Bool - - - --- Generic class, so that custom data types can be derived -class GOrbit f where - type GOrb f :: * - gtoOrbit :: f a -> GOrb f - gsupport :: f a -> Support - ggetElement :: GOrb f -> Support -> f a - gindex :: Proxy f -> GOrb f -> Int - - --- Instance for the Void type -instance GOrbit V1 where - type GOrb V1 = Void - gtoOrbit v = undefined - gsupport _ = empty - ggetElement v _ = undefined - gindex _ _ = 0 - - --- Instance for the Uni type -instance GOrbit U1 where - type GOrb U1 = () - gtoOrbit _ = () - gsupport _ = empty - ggetElement _ _ = U1 - gindex _ _ = 0 - - --- Disjoint unions are easy: just work on either side. -instance (GOrbit f, GOrbit g) => GOrbit (f :+: g) where - type GOrb (f :+: g) = Either (GOrb f) (GOrb g) - gtoOrbit (L1 a) = Left (gtoOrbit a) - gtoOrbit (R1 b) = Right (gtoOrbit b) - gsupport (L1 a) = gsupport a - gsupport (R1 b) = gsupport b - ggetElement (Left oa) s = L1 (ggetElement oa s) - ggetElement (Right ob) s = R1 (ggetElement ob s) - gindex proxy (Left oa) = gindex (left proxy) oa where - left :: proxy (f :+: g) -> Proxy f - left _ = Proxy - gindex proxy (Right ob) = gindex (right proxy) ob where - right :: proxy (f :+: g) -> Proxy g - right _ = Proxy - - --- The cartesian product is a non-trivial instance. We represent orbits in a --- product as described inthe paper: with two orbits, and how the match. The --- matchings can be given as strings, which can be easily enumerated, in order --- to enumerate the whole product. -instance (GOrbit f, GOrbit g) => GOrbit (f :*: g) where - type GOrb (f :*: g) = OrbPair (GOrb f) (GOrb g) - gtoOrbit ~(a :*: b) = OrbPair (gtoOrbit a) (gtoOrbit b) (bla sa sb) - where - sa = toList $ gsupport a - sb = toList $ gsupport b - bla [] ys = fmap (const GT) ys - bla xs [] = fmap (const LT) xs - bla (x:xs) (y:ys) = case compare x y of - LT -> LT : (bla xs (y:ys)) - EQ -> EQ : (bla xs ys) - GT -> GT : (bla (x:xs) ys) - gsupport ~(a :*: b) = (gsupport a) `union` (gsupport b) - ggetElement (OrbPair oa ob l) s = (ggetElement oa $ toSet ls) :*: (ggetElement ob $ toSet rs) - where - ~(ls, rs) = partitionOrd fst . zip l . toList $ s - toSet = fromDistinctAscList . fmap snd - gindex _ (OrbPair _ _ l) = length l - -data OrbPair a b = OrbPair !a !b ![Ordering] - deriving (Show, Eq, Ord, Generic) - --- Could be in prelude or some other general purpose lib -partitionOrd :: (a -> Ordering) -> [a] -> ([a], [a]) -partitionOrd p xs = foldr (selectOrd p) ([], []) xs - -selectOrd :: (a -> Ordering) -> a -> ([a], [a]) -> ([a], [a]) -selectOrd f x ~(ls, rs) = case f x of - LT -> (x : ls, rs) - EQ -> (x : ls, x : rs) - GT -> (ls, x : rs) - - -instance Orbit a => GOrbit (K1 c a) where - -- Cannot use (Orb a) here, that may lead to a recursive type - -- So we use the type OrbRec a instead (which uses Orb a one step later). - type GOrb (K1 c a) = OrbRec a - gtoOrbit (K1 x) = OrbRec (toOrbit x) - gsupport (K1 x) = support x - ggetElement (OrbRec x) s = K1 $ getElement x s - gindex p (OrbRec o) = index (Proxy :: Proxy a) o - -newtype OrbRec a = OrbRec (Orb a) - deriving (Generic) -deriving instance Show (Orb a) => Show (OrbRec a) -deriving instance Ord (Orb a) => Ord (OrbRec a) -deriving instance Eq (Orb a) => Eq (OrbRec a) - - -instance GOrbit f => GOrbit (M1 i c f) where - type GOrb (M1 i c f) = GOrb f - gtoOrbit (M1 x) = gtoOrbit x - gsupport (M1 x) = gsupport x - ggetElement x s = M1 $ ggetElement x s - gindex p o = gindex (Proxy :: Proxy f) o diff --git a/src/OrbitList.hs b/src/OrbitList.hs index 41ed185..211932c 100644 --- a/src/OrbitList.hs +++ b/src/OrbitList.hs @@ -10,15 +10,15 @@ import qualified Data.List.Ordered as LO import Data.Proxy import Prelude hiding (map, product) -import Orbit +import Nominal import Support -newtype OrbitList a = OrbitList { unOrbitList :: [Orb a] } +newtype OrbitList a = OrbitList { unOrbitList :: [Orbit a] } -deriving instance Eq (Orb a) => Eq (OrbitList a) -deriving instance Ord (Orb a) => Ord (OrbitList a) -deriving instance Show (Orb a) => Show (OrbitList a) +deriving instance Eq (Orbit a) => Eq (OrbitList a) +deriving instance Ord (Orbit a) => Ord (OrbitList a) +deriving instance Show (Orbit a) => Show (OrbitList a) null :: OrbitList a -> Bool null (OrbitList x) = L.null x @@ -26,20 +26,20 @@ null (OrbitList x) = L.null x empty :: OrbitList a empty = OrbitList [] -singleOrbit :: Orbit a => a -> OrbitList a +singleOrbit :: Nominal a => a -> OrbitList a singleOrbit a = OrbitList [toOrbit a] rationals :: OrbitList Rat rationals = singleOrbit (Rat 0) -- f should be equivariant -map :: (Orbit a, Orbit b) => (a -> b) -> OrbitList a -> OrbitList b +map :: (Nominal a, Nominal b) => (a -> b) -> OrbitList a -> OrbitList b map f (OrbitList as) = OrbitList $ L.map (omap f) as -productWith :: forall a b c. (Orbit a, Orbit b, Orbit c) => (a -> b -> c) -> OrbitList a -> OrbitList b -> OrbitList c +productWith :: forall a b c. (Nominal a, Nominal b, Nominal c) => (a -> b -> c) -> OrbitList a -> OrbitList b -> OrbitList c productWith f (OrbitList as) (OrbitList bs) = map (uncurry f) (OrbitList (concat $ product (Proxy :: Proxy a) (Proxy :: Proxy b) <$> as <*> bs)) -filter :: Orbit a => (a -> Bool) -> OrbitList a -> OrbitList a +filter :: Nominal a => (a -> Bool) -> OrbitList a -> OrbitList a filter f = OrbitList . L.filter (f . getElementE) . unOrbitList @@ -47,17 +47,17 @@ type SortedOrbitList a = OrbitList a -- the above map and productWith preserve ordering if `f` is order preserving -- on orbits and filter is always order preserving -union :: Ord (Orb a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a +union :: Ord (Orbit a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a union (OrbitList x) (OrbitList y) = OrbitList (LO.union x y) -unionAll :: Ord (Orb a) => [SortedOrbitList a] -> SortedOrbitList a +unionAll :: Ord (Orbit a) => [SortedOrbitList a] -> SortedOrbitList a unionAll = OrbitList . LO.unionAll . fmap unOrbitList -minus :: Ord (Orb a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a +minus :: Ord (Orbit a) => SortedOrbitList a -> SortedOrbitList a -> SortedOrbitList a minus (OrbitList x) (OrbitList y) = OrbitList (LO.minus x y) -- decompose a into b and c (should be order preserving), and then throw away b -projectWith :: (Orbit a, Orbit b, Orbit c, Eq (Orb b), Ord (Orb c)) => (a -> (b, c)) -> SortedOrbitList a -> SortedOrbitList c +projectWith :: (Nominal a, Nominal b, Nominal c, Eq (Orbit b), Ord (Orbit c)) => (a -> (b, c)) -> SortedOrbitList a -> SortedOrbitList c projectWith f = unionAll . fmap OrbitList . groupOnFst . splitOrbs . unOrbitList . map f where splitOrbs = fmap (\o -> (omap fst o, omap snd o)) diff --git a/test/Bench.hs b/test/Bench.hs index e6d7245..d3c2ed0 100644 --- a/test/Bench.hs +++ b/test/Bench.hs @@ -5,14 +5,14 @@ import Control.DeepSeq import Criterion.Main -import Orbit +import Nominal import Support import EquivariantSet import EquivariantMap instance NFData Rat -(\/) :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a +(\/) :: Ord (Orbit a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a (\/) = EquivariantSet.union bigset :: (Rat, Rat, Rat, _) -> Bool