{-# LANGUAGE
DeriveGeneric
, DeriveDataTypeable
, DerivingVia
, FlexibleInstances
, GeneralizedNewtypeDeriving
, MultiParamTypeClasses
, ScopedTypeVariables
, StandaloneDeriving
, TypeFamilies
, UndecidableInstances
#-}
{-|
Module: Data.Act
An "Act" of a semigroup \( S \) on a type \( X \) gives a way to transform terms of type \( X \) by terms of type \( S \),
in a way that is compatible with the semigroup operation on \( S \).
In the special case that there is a unique way of going from one term of type \( X \) to another
through a transformation by a term of type \( S \), we say that \( X \) is a torsor under \( S \).
For example, the plane has an action by translations. Given any two points, there is a unique translation
that takes the first point to the second. Note that an unmarked plane (like a blank piece of paper)
has no designated origin or reference point, whereas the set of translations is a plane with a given origin
(the zero translation). This is the distinction between an affine space (an unmarked plane) and a vector space.
Enforcing this distinction in the types can help to avoid confusing absolute points with translation vectors.
Simple 'Act' and 'Torsor' instances can be derived through self-actions:
> > newtype Seconds = Seconds { getSeconds :: Double }
> > deriving ( Act TimeDelta, Torsor TimeDelta )
> > via TimeDelta
> > newtype TimeDelta = TimeDelta { timeDeltaInSeconds :: Seconds }
> > deriving ( Semigroup, Monoid, Group )
> > via Sum Double
-}
module Data.Act
( Act(..)
, transportAction
, Trivial(..)
, Torsor(..)
, anti
, intertwiner
, Finitely(..)
)
where
-- base
import Data.Coerce
( coerce )
import Data.Data
( Data )
import Data.Functor.Const
( Const(..) )
import Data.Functor.Contravariant
( Op(..) )
import Data.Monoid
( Any(..), All(..)
, Sum(..), Product(..)
, Ap(..), Endo(..)
)
import Data.Semigroup
( Dual(..) )
import GHC.Generics
( Generic, Generic1 )
-- deepseq
import Control.DeepSeq
( NFData )
-- finitary
import Data.Finitary
( Finitary(..) )
-- finite-typelits
import Data.Finite
( Finite )
-- groups
import Data.Group
( Group(..) )
-----------------------------------------------------------------
-- | A left __act__ (or left __semigroup action__) of a semigroup @s@ on @x@ consists of an operation
--
-- @(•) :: s -> x -> x@
--
-- such that:
--
-- @a • ( b • x ) = ( a <> b ) • x@
--
-- In case @s@ is also a 'Monoid', we additionally require:
--
-- @mempty • x = x@
--
-- The synonym @ act = (•) @ is also provided.
class Semigroup s => Act s x where
{-# MINIMAL (•) | act #-}
-- | Left action of a semigroup.
(•), act :: s -> x -> x
(•) = act
act = (•)
infixr 5 •
infixr 5 `act`
-- | Transport an act:
--
-- <
>
transportAction :: ( a -> b ) -> ( b -> a ) -> ( g -> b -> b ) -> ( g -> a -> a )
transportAction to from actBy g = from . actBy g . to
-- | Natural left action of a semigroup on itself.
instance Semigroup s => Act s s where
(•) = (<>)
-- | Trivial act of a semigroup on any type (acting by the identity).
newtype Trivial a = Trivial { getTrivial :: a }
deriving stock ( Show, Read, Data, Generic, Generic1 )
deriving newtype ( Eq, Ord, Enum, Bounded, NFData )
instance Semigroup s => Act s ( Trivial a ) where
act _ = id
deriving via Any instance Act Any Bool
deriving via All instance Act All Bool
instance Num a => Act ( Sum a ) a where
act s = coerce ( act s :: Sum a -> Sum a )
instance Num a => Act ( Product a ) a where
act s = coerce ( act s :: Product a -> Product a )
instance {-# OVERLAPPING #-} Act () x where
act _ = id
instance ( Act s1 x1, Act s2 x2 )
=> Act ( s1, s2 ) ( x1,x2 ) where
act ( s1, s2 ) ( x1, x2 ) =
( act s1 x1, act s2 x2 )
instance ( Act s1 x1, Act s2 x2, Act s3 x3 )
=> Act ( s1, s2, s3 ) ( x1, x2, x3 ) where
act ( s1, s2, s3 ) ( x1, x2, x3 ) =
( act s1 x1, act s2 x2, act s3 x3 )
instance ( Act s1 x1, Act s2 x2, Act s3 x3, Act s4 x4 )
=> Act ( s1, s2, s3, s4 ) ( x1, x2, x3, x4 ) where
act ( s1, s2, s3, s4 ) ( x1, x2, x3, x4 ) =
( act s1 x1, act s2 x2, act s3 x3, act s4 x4 )
instance ( Act s1 x1, Act s2 x2, Act s3 x3, Act s4 x4, Act s5 x5 )
=> Act ( s1, s2, s3, s4, s5 ) ( x1, x2, x3, x4, x5 ) where
act ( s1, s2, s3, s4, s5 ) ( x1, x2, x3, x4, x5 ) =
( act s1 x1, act s2 x2, act s3 x3, act s4 x4, act s5 x5 )
deriving newtype instance Act s a => Act s ( Const a b )
-- | Acting through a functor using @fmap@.
instance ( Act s x, Functor f ) => Act s ( Ap f x ) where
act s = coerce ( fmap ( act s ) :: f x -> f x )
-- | Acting through the contravariant function arrow functor: right action.
--
-- If acting by a group, use `anti :: Group g => g -> Dual g` to act by the original group
-- instead of the opposite group.
instance ( Semigroup s, Act s a ) => Act ( Dual s ) ( Op b a ) where
act ( Dual s ) = coerce ( ( . act s ) :: ( a -> b ) -> ( a -> b ) )
-- | Acting through a function arrow: both covariant and contravariant actions.
--
-- If acting by a group, use `anti :: Group g => g -> Dual g` to act by the original group
-- instead of the opposite group.
instance ( Semigroup s, Act s a, Act t b ) => Act ( Dual s, t ) ( a -> b ) where
act ( Dual s, t ) p = act t . p . act s
-- | Action of a group on endomorphisms.
instance ( Group g, Act g a ) => Act g ( Endo a ) where
act g = coerce ( act ( anti g, g ) :: ( a -> a ) -> ( a -> a ) )
-- | Newtype for the action on a type through its 'Finitary' instance.
--
-- > data ABCD = A | B | C | D
-- > deriving stock ( Eq, Generic )
-- > deriving anyclass Finitary
-- > deriving ( Act ( Sum ( Finite 4 ) ), Torsor ( Sum ( Finite 4 ) ) )
-- > via Finitely ABCD
--
-- Sizes are checked statically. For instance if we had instead written:
--
-- > deriving ( Act ( Sum ( Finite 3 ) ), Torsor ( Sum ( Finite 3 ) ) )
-- > via Finitely ABCD
--
-- we would have gotten the error messages:
--
-- > * No instance for (Act (Sum (Finite 3)) (Finite 4))
-- > * No instance for (Torsor (Sum (Finite 3)) (Finite 4))
--
newtype Finitely a = Finitely { getFinitely :: a }
deriving stock ( Show, Read, Data, Generic, Generic1 )
deriving newtype ( Eq, Ord, NFData )
-- | Act on a type through its 'Finitary' instance.
instance ( Semigroup s, Act s ( Finite n ), Finitary a, n ~ Cardinality a )
=> Act s ( Finitely a ) where
act s = Finitely . fromFinite . act s . toFinite . getFinitely
-- | Torsor for a type using its 'Finitary' instance.
instance ( Group g, Torsor g ( Finite n ), Finitary a, n ~ Cardinality a )
=> Torsor g ( Finitely a ) where
Finitely x --> Finitely y = toFinite x --> toFinite y
-----------------------------------------------------------------
-- | A left __torsor__ consists of a /free/ and /transitive/ left action of a group on an inhabited type.
--
-- This precisely means that for any two terms @x@, @y@, there exists a /unique/ group element @g@ taking @x@ to @y@,
-- which is denoted @ y <-- x @ (or @ x --> y @, but the left-pointing arrow is more natural when working with left actions).
--
-- That is @ y <-- x @ is the /unique/ element satisfying:
--
-- @( y <-- x ) • x = y@
--
--
-- Note the order of composition of @<--@ and @-->@ with respect to @<>@:
--
-- > ( z <-- y ) <> ( y <-- x ) = z <-- x
--
-- > ( y --> z ) <> ( x --> y ) = x --> z
class ( Group g, Act g x ) => Torsor g x where
{-# MINIMAL (-->) | (<--) #-}
-- | Unique group element effecting the given transition
(<--), (-->) :: x -> x -> g
(-->) = flip (<--)
(<--) = flip (-->)
infix 7 -->
infix 7 <--
-- | A group's inversion anti-automorphism corresponds to an isomorphism to the opposite group.
--
-- The inversion allows us to obtain a left action from a right action (of the same group);
-- the equivalent operation is not possible for general semigroups.
anti :: Group g => g -> Dual g
anti g = Dual ( invert g )
-- | Any group is a torsor under its own natural left action.
instance Group g => Torsor g g where
h <-- g = h <> invert g
instance Num a => Torsor ( Sum a ) a where
(<--) = coerce ( (<--) :: Sum a -> Sum a -> Sum a )
-- | Given
--
-- * \( g \in G \) acting on \( A \),
-- * \( B \) a torsor under \( H \),
-- * a map \( p \colon A \to B \),
--
-- this function returns the unique element \( h \in H \) making the following diagram commute:
--
-- <
>
intertwiner :: forall h g a b. ( Act g a, Torsor h b ) => g -> ( a -> b ) -> a -> h
intertwiner g p a = p a --> p ( g • a )