diff --git a/ons-hs.cabal b/ons-hs.cabal index 54c6771..9e36c32 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -18,10 +18,13 @@ library exposed-modules: EquivariantMap , EquivariantSet , Orbit + , Orbit.Class + , Orbit.Products , Support build-depends: base >= 4.7 && < 5 , containers , data-ordlist + , MemoTrie default-language: Haskell2010 executable ons-hs-exe diff --git a/src/EquivariantSet.hs b/src/EquivariantSet.hs index 7873122..dbed768 100644 --- a/src/EquivariantSet.hs +++ b/src/EquivariantSet.hs @@ -108,12 +108,12 @@ filter f (EqSet s) = EqSet . Set.filter (f . getElementE) $ s -- 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 f = EqSet . Set.map (toOrbit . f . getElementE) . unEqSet +map f = EqSet . Set.map (omap f) . unEqSet -- f should also preserve order on the orbit types! -- This means you should know the representation to use it well mapMonotonic :: (Orbit a, Orbit b) => (a -> b) -> EquivariantSet a -> EquivariantSet b -mapMonotonic f = EqSet . Set.mapMonotonic (toOrbit . f . getElementE) . unEqSet +mapMonotonic f = EqSet . Set.mapMonotonic (omap f) . unEqSet -- Conversion diff --git a/src/Orbit.hs b/src/Orbit.hs index 3fdbe59..bcd14c0 100644 --- a/src/Orbit.hs +++ b/src/Orbit.hs @@ -3,39 +3,29 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} -module Orbit where +module Orbit + ( module Orbit + , module Orbit.Class + ) where import Support (Support, Rat(..)) import qualified Support +import Orbit.Products +import Orbit.Class + -- TODO: Make generic instances (we already have sums and products) -- TODO: For products: replace [Ordering] with Vec Ordering if better -- TODO: replace Support by an ordered vector / list for speed? --- 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 == Set.size . support --- * getElement o s is defined if index o == Set.size s -class Orbit a where - data Orb a :: * - toOrbit :: a -> Orb a - support :: a -> Support - getElement :: Orb a -> Support -> a - index :: Orb a -> Int - -- We can get 'default' values, if we don't care about the support. getElementE :: Orbit a => Orb a -> a getElementE orb = getElement orb (Support.def (index 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. @@ -113,8 +103,8 @@ deriving instance (Eq (Orb a), Eq (Orb b)) => Eq (Orb (a, b)) deriving instance (Ord (Orb a), Ord (Orb b)) => Ord (Orb (a, b)) -- Could be in prelude or some other general purpose lib -partitionOrd :: (a -> Ordering) -> [a] -> ([a],[a]) -{-# INLINE partitionOrd #-} +{-# INLINABLE partitionOrd #-} +partitionOrd :: (a -> Ordering) -> [a] -> ([a], [a]) partitionOrd p xs = foldr (selectOrd p) ([], []) xs selectOrd :: (a -> Ordering) -> a -> ([a], [a]) -> ([a], [a]) @@ -123,19 +113,21 @@ selectOrd f x ~(ls, rs) = case f x of EQ -> (x : ls, x : rs) GT -> (ls, x : rs) --- Enumerate all orbits in a product. In lexicographical order! +-- Enumerate all orbits in a product A x B. In lexicographical order! product :: (Orbit a, Orbit b) => Orb a -> Orb b -> [Orb (a, b)] product oa ob = OrbPair oa ob <$> prodStrings (index oa) (index ob) --- I tried Seq [Ordering], it was slower -prodStrings :: Int -> Int -> [[Ordering]] -prodStrings 0 0 = [[]] -prodStrings 0 n = [replicate n GT] -prodStrings n 0 = [replicate n LT] -prodStrings 1 1 = [[LT, GT], [EQ], [GT, LT]] -prodStrings n m = ((LT :) <$> prodStrings (n-1) m) - ++ ((EQ :) <$> prodStrings (n-1) (m-1)) - ++ ((GT :) <$> prodStrings n (m-1)) +-- Separated product: A * B = { (a,b) | Exist C1, C2 disjoint supporting a, b resp.} +separatedProduct :: (Orbit a, Orbit b) => Orb a -> Orb b -> [Orb (a, b)] +separatedProduct oa ob = OrbPair oa ob <$> sepProdStrings (index oa) (index ob) + +-- "Left product": A |x B = { (a,b) | C supports a => C supports b } +leftProduct :: (Orbit a, Orbit b) => Orb a -> Orb b -> [Orb (a, b)] +leftProduct oa ob = OrbPair oa ob <$> rincProdStrings (index oa) (index ob) + +{-# INLINABLE product #-} +{-# INLINABLE separatedProduct #-} +{-# INLINABLE leftProduct #-} -- Data structure for the discrete nominal sets with a trivial action. diff --git a/src/Orbit/Class.hs b/src/Orbit/Class.hs new file mode 100644 index 0000000..67634db --- /dev/null +++ b/src/Orbit/Class.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE TypeFamilies #-} + +module Orbit.Class where + +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 == Set.size . support +-- * getElement o s is defined if index o == Set.size s +class Orbit a where + data Orb a :: * + toOrbit :: a -> Orb a + support :: a -> Support + getElement :: Orb a -> Support -> a + index :: Orb a -> Int + + +{- +I tried to do generics, but failed. One cannot do generic injective +data constructors. I will keep it here now, for later reference. + +{-# language DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +import GHC.Generic + + default Orb a :: (Generic a, GOrbit (Rep a)) => * + data Orb a = Orb () -- how to make a default data instance declaration? + + default toOrbit :: (Generic a, GOrbit (Rep a)) => a -> Orb a + toOrbit = _ . gtoOrbit . from + + default support :: (Generic a, GOrbit (Rep a)) => a -> Support + support = gsupport . from + + default getElement :: (Generic a, GOrbit (Rep a)) => Orb a -> Support -> a + getElement = undefined + + default index :: (Generic a, GOrbit (Rep a)) => Orb a -> Int + index = undefined + +class GOrbit f where + data GOrb f :: * -> * + gtoOrbit :: f a -> GOrb f a + gsupport :: f a -> Support + ggetElement :: GOrb f a -> Support -> f a + gindex :: GOrb f a -> Int +-} diff --git a/src/Orbit/Products.hs b/src/Orbit/Products.hs new file mode 100644 index 0000000..f0be39f --- /dev/null +++ b/src/Orbit/Products.hs @@ -0,0 +1,41 @@ +module Orbit.Products where + +import Control.Applicative +import Data.MemoTrie + +prodStrings :: Alternative f => Int -> Int -> f [Ordering] +prodStrings = memo2 gen where + gen 0 0 = pure [] + gen 0 n = pure $ replicate n GT + gen n 0 = pure $ replicate n LT + gen 1 1 = pure [LT, GT] <|> pure [EQ] <|> pure [GT, LT] + gen n m = (LT :) <$> prodStrings (n-1) m + <|> (EQ :) <$> prodStrings (n-1) (m-1) + <|> (GT :) <$> prodStrings n (m-1) + +sepProdStrings :: Alternative f => Int -> Int -> f [Ordering] +sepProdStrings = memo2 gen where + gen 0 0 = pure [] + gen 0 n = pure $ replicate n GT + gen n 0 = pure $ replicate n LT + gen 1 1 = pure [LT, GT] <|> pure [GT, LT] + gen n m = (LT :) <$> sepProdStrings (n-1) m + <|> (GT :) <$> sepProdStrings n (m-1) + +rincProdStrings :: Alternative f => Int -> Int -> f [Ordering] +rincProdStrings = memo2 gen where + gen n 0 = pure $ replicate n LT + gen 0 _ = empty + gen 1 1 = pure [EQ] + gen n m + | n < m = empty + | otherwise = (LT :) <$> rincProdStrings (n-1) m + <|> (EQ :) <$> rincProdStrings (n-1) (m-1) + +{-# INLINABLE prodStrings #-} +{-# INLINABLE sepProdStrings #-} +{-# INLINABLE rincProdStrings #-} + +{-# SPECIALIZE prodStrings :: Int -> Int -> [[Ordering]] #-} +{-# SPECIALIZE sepProdStrings :: Int -> Int -> [[Ordering]] #-} +{-# SPECIALIZE rincProdStrings :: Int -> Int -> [[Ordering]] #-} diff --git a/stack.yaml b/stack.yaml index 350ec44..12a8d61 100644 --- a/stack.yaml +++ b/stack.yaml @@ -15,7 +15,7 @@ # resolver: # name: custom-snapshot # location: "./custom-snapshot.yaml" -resolver: lts-9.10 +resolver: lts-10.5 # User packages to be built. # Various formats can be used as shown in the example below.