From fa2061ac43cb4d59c5cffc3222c38a9af899cf27 Mon Sep 17 00:00:00 2001
From: Joshua Moerman <lakseru@gmail.com>
Date: Fri, 27 Oct 2017 18:21:34 +0200
Subject: [PATCH] Orbit instance for Support . More documentation .

---
 src/EquivariantMap.hs |  26 ++++++----
 src/EquivariantSet.hs |  40 ++++++++++----
 src/Orbit.hs          | 118 +++++++++++++++++++++++++++---------------
 3 files changed, 120 insertions(+), 64 deletions(-)

diff --git a/src/EquivariantMap.hs b/src/EquivariantMap.hs
index 4d1f85b..bc05898 100644
--- a/src/EquivariantMap.hs
+++ b/src/EquivariantMap.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 module EquivariantMap where
 
@@ -14,8 +14,17 @@ import qualified Data.Map as Map
 import EquivariantSet (EquivariantSet(EqSet))
 import Orbit
 
--- Very similar to EquivariantSet
--- Some of the notes there apply here too
+-- TODO: foldable / traversable
+-- TODO: adjust / alter / update
+-- TODO: -WithKey functions
+-- TODO: don't export the helper functions
+-- TODO: cleanup (usage of getElelemtE is not necessary)
+-- TODO: replace [Bool] by Vec Bool if better?
+
+-- Very similar to EquivariantSet, but then the map analogue. The important
+-- 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]) }
 
 -- Need undecidableIntances for this
@@ -27,23 +36,18 @@ deriving instance (Show (Orb k), Show (Orb v)) => Show (EquivariantMap k v)
 deriving instance Ord (Orb k) => Monoid (EquivariantMap k v)
 deriving instance Ord (Orb k) => Semigroup (EquivariantMap k v)
 
--- TODO: foldable / traversable
--- TODO: adjust / alter / update
--- TODO: *WithKey functions
-
--- Some helper functions
--- TODO: don't export these
+-- Helper functions
 
 mapel :: (Orbit k, Orbit v) => k -> v -> (Orb v, [Bool])
 mapel k v = (toOrbit v, bv (Set.toAscList (support k)) (Set.toAscList (support v)))
 
 bv :: [Rat] -> [Rat] -> [Bool]
 bv l [] = replicate (length l) False
-bv [] l = undefined -- Non-equivariant function
+bv [] l = 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 -> undefined -- Non-equivariant function
+  GT -> error "Non-equivariant function"
 
 mapelInv :: (Orbit k, Orbit v) => k -> (Orb v, [Bool]) -> v
 mapelInv x (oy, bv) = getElement oy (Set.fromAscList . fmap fst . Prelude.filter snd $ zip (Set.toAscList (support x)) bv)
diff --git a/src/EquivariantSet.hs b/src/EquivariantSet.hs
index fa7b155..c6a8bfd 100644
--- a/src/EquivariantSet.hs
+++ b/src/EquivariantSet.hs
@@ -1,7 +1,9 @@
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module EquivariantSet where
 
@@ -11,12 +13,15 @@ import Data.Semigroup (Semigroup)
 
 import Orbit
 
--- Given a nominal type, we can construct equivariant sets
--- These simply use a set data structure from prelude
--- This works well because orbits are uniquely represented
--- Note that functions such as toList do not return an ordered
--- list since the representatives are chosen arbitrarily.
--- TODO: think about folds (and size)
+-- TODO: think about folds (the monoids should be nominal?)
+-- TODO: partition / fromList / ...
+
+-- Given a nominal type, we can construct equivariant sets. These simply use a
+-- standard set data structure. This works well because orbits are uniquely
+-- represented. Although internally it is just a set of orbits, the interface
+-- 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) }
 
 -- Need undecidableIntances for this
@@ -29,14 +34,27 @@ deriving instance Show (Orb a) => Show (EquivariantSet a)
 deriving instance Ord (Orb a) => Monoid (EquivariantSet a)
 deriving instance Ord (Orb a) => Semigroup (EquivariantSet a)
 
+-- We could derive a correct instance if I had written generic instances.
+-- Didn't do that yet, but a direct instance is also nice.
+instance Orbit (EquivariantSet a) where
+  newtype Orb (EquivariantSet a) = OrbEqSet (EquivariantSet a)
+  toOrbit = OrbEqSet
+  support _ = Set.empty
+  getElement (OrbEqSet x) _ = x
+  index _ = 0
+
+deriving instance Show (Orb a) => Show (Orb (EquivariantSet a))
+deriving instance Eq (Orb a) => Eq (Orb (EquivariantSet a))
+deriving instance Ord (Orb a) => Ord (Orb (EquivariantSet a))
+
 
 -- Query
 
 null :: EquivariantSet a -> Bool
 null = Set.null . unEqSet
 
-size :: EquivariantSet a -> Int
-size = Set.size . unEqSet
+orbits :: EquivariantSet a -> Int
+orbits = Set.size . unEqSet
 
 member :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> Bool
 member a = Set.member (toOrbit a) . unEqSet
@@ -71,7 +89,7 @@ difference a b = EqSet $ Set.difference (unEqSet a) (unEqSet b)
 intersection :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
 intersection a b = EqSet $ Set.intersection (unEqSet a) (unEqSet b)
 
--- This is the meat of the file!
+-- This is the meat of the file! Relies on the ordering of Orbit.product
 product :: (Orbit a, Orbit b) => EquivariantSet a -> EquivariantSet b -> EquivariantSet (a, b)
 product (EqSet sa) (EqSet sb) = EqSet . Set.fromDistinctAscList . concat
                               $ Orbit.product <$> Set.toAscList sa <*> Set.toAscList sb
diff --git a/src/Orbit.hs b/src/Orbit.hs
index 4b9d99e..1e4b3a1 100644
--- a/src/Orbit.hs
+++ b/src/Orbit.hs
@@ -1,44 +1,58 @@
-{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module Orbit where
 
 import Data.Set (Set)
 import qualified Data.Set as Set
 
--- We only need ordering on this structure
--- I wrap it, because Rational is a type synonym
+-- 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?
+
+
+-- We take some model of the dense linear order. The rationals are a natural
+-- choice. (Note that every countable model is order-isomorphic, so it doesn't
+-- matter so much in the end.) I wrap it in a newtype, so we will only use the
+-- Ord instances, and because it's not very nice to work with type synonyms.
+-- Show instance included for debugging.
 newtype Rat = Rat { unRat :: Rational }
-  deriving (Eq, Ord)
+  deriving (Eq, Ord, Show)
 
--- Just for debugging
-instance Show Rat where
-  show (Rat r) = show r
-  showsPrec n (Rat r) = showsPrec n r
 
--- A support is a set of rational numbers
--- Can also be represented as sorted list/vector
--- I should experiment with that, once I have some tests
+-- A support is a set of rational numbers, which can always be ordered. Can
+-- also be represented as sorted list/vector. Maybe I should also make it into
+-- a newtype.
 type Support = Set Rat
 
--- Type class indicating that we can associate orbits with elements
--- In fact, it means that a is a nominal type
+-- 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
-  -- Precondition: size of set == index
   getElement :: Orb a -> Support -> a
-  -- Size of least support
   index :: Orb a -> Int
 
--- Just some element
+-- We can get 'default' values, if we don't care about the support.
 getElementE :: Orbit a => Orb a -> a
 getElementE orb = getElement orb (Set.fromAscList . fmap (Rat . toRational) $ [1 .. index orb])
 
--- Rational numbers fit the bill
+
+-- 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
   data Orb Rat = OrbRational
   toOrbit _ = OrbRational
@@ -52,8 +66,45 @@ deriving instance Show (Orb Rat)
 deriving instance Eq (Orb Rat)
 deriving instance Ord (Orb Rat)
 
--- Cartesian product of nominal sets as well
--- TODO: replace [Ordering] with Vec Ordering if better
+
+-- 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
+  newtype Orb Support = OrbSupport Int
+  toOrbit s = OrbSupport (Set.size s)
+  support s = s
+  getElement _ s = s
+  index (OrbSupport n) = n
+
+deriving instance Show (Orb Support)
+deriving instance Eq (Orb Support)
+deriving instance Ord (Orb Support)
+
+
+-- Disjoint unions are easy: just work on either side.
+instance (Orbit a, Orbit b) => Orbit (Either a b) where
+  newtype Orb (Either a b) = OrbEither (Either (Orb a) (Orb b))
+  toOrbit (Left a) = OrbEither (Left (toOrbit a))
+  toOrbit (Right b) = OrbEither (Right (toOrbit b))
+  support (Left a) = support a
+  support (Right b) = support b
+  getElement (OrbEither (Left oa)) s = Left (getElement oa s)
+  getElement (OrbEither (Right ob)) s = Right (getElement ob s)
+  index (OrbEither (Left oa)) = index oa
+  index (OrbEither (Right ob)) = index ob
+
+deriving instance (Show (Orb a), Show (Orb b)) => Show (Orb (Either a b))
+deriving instance (Eq (Orb a), Eq (Orb b)) => Eq (Orb (Either a b))
+deriving instance (Ord (Orb a), Ord (Orb b)) => Ord (Orb (Either a b))
+
+
+-- 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 (Orbit a, Orbit b) => Orbit (a, b) where
   data Orb (a,b) = OrbPair !(Orb a) !(Orb b) ![Ordering]
   toOrbit (a, b) = OrbPair (toOrbit a) (toOrbit b) (bla sa sb) 
@@ -88,8 +139,7 @@ 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. 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)
 
@@ -102,25 +152,10 @@ prodStrings n m = ((LT :) <$> prodStrings (n-1) m)
   ++ ((EQ :) <$> prodStrings (n-1) (m-1))
   ++ ((GT :) <$> prodStrings n (m-1))
 
--- Also for sums
-instance (Orbit a, Orbit b) => Orbit (Either a b) where
-  newtype Orb (Either a b) = OrbEither (Either (Orb a) (Orb b))
-  toOrbit (Left a) = OrbEither (Left (toOrbit a))
-  toOrbit (Right b) = OrbEither (Right (toOrbit b))
-  support (Left a) = support a
-  support (Right b) = support b
-  getElement (OrbEither (Left oa)) s = Left (getElement oa s)
-  getElement (OrbEither (Right ob)) s = Right (getElement ob s)
-  index (OrbEither (Left oa)) = index oa
-  index (OrbEither (Right ob)) = index ob
 
-deriving instance (Show (Orb a), Show (Orb b)) => Show (Orb (Either a b))
-deriving instance (Eq (Orb a), Eq (Orb b)) => Eq (Orb (Either a b))
-deriving instance (Ord (Orb a), Ord (Orb b)) => Ord (Orb (Either a b))
-
--- Data structure for the discrete nominal sets
--- with a trivial action.
-data Trivial a = Trivial { unTrivial :: a }
+-- Data structure for the discrete nominal sets with a trivial action.
+newtype Trivial a = Trivial { unTrivial :: a }
+  deriving (Eq, Ord, Show)
 
 -- We need to remember the value!
 instance Orbit (Trivial a) where
@@ -134,8 +169,8 @@ deriving instance Show a => Show (Orb (Trivial a))
 deriving instance Eq a => Eq (Orb (Trivial a))
 deriving instance Ord a => Ord (Orb (Trivial a))
 
--- Orbits themselves are trivial,
--- but we need to keep track of the orbit
+
+-- Orbits themselves are trivial.
 instance Orbit a => Orbit (Orb a) where
   newtype Orb (Orb a) = OrbOrb (Orb a)
   toOrbit a = OrbOrb a
@@ -143,7 +178,6 @@ instance Orbit a => Orbit (Orb a) where
   getElement (OrbOrb oa) _ = oa
   index _ = 0
 
--- These are funny looking...
 deriving instance Show (Orb a) => Show (Orb (Orb a))
 deriving instance Eq (Orb a) => Eq (Orb (Orb a))
 deriving instance Ord (Orb a) => Ord (Orb (Orb a))