1
Fork 0
mirror of https://github.com/Jaxan/ons-hs.git synced 2025-04-27 06:37:44 +02:00

Moves Orbit class to separate file. Adds more types of products

This commit is contained in:
Joshua Moerman 2018-02-27 16:55:03 +01:00
parent 8487919a7c
commit 1f0e50898f
6 changed files with 127 additions and 35 deletions

View file

@ -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

View file

@ -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

View file

@ -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.

56
src/Orbit/Class.hs Normal file
View file

@ -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
-}

41
src/Orbit/Products.hs Normal file
View file

@ -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]] #-}

View file

@ -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.