{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE ScopedTypeVariables    #-}

--------------------------------------------------------------------------------
-- |
--
-- Module      :  Data.Act
-- Description :  Group torsors for left and right actions.
-- Copyright   :  (c) Alice Rixte 2025
-- License     :  BSD 3
-- Maintainer  :  alice.rixte@u-bordeaux.fr
-- Stability   :  unstable
-- Portability :  non-portable (GHC extensions)
--
-- == Presentation
--
--
--------------------------------------------------------------------------------

module Data.Act.Torsor
  ( LTorsor (..)
  , RTorsor (..)
  )
where

import Data.Coerce
import Data.Functor.Identity
import Data.Monoid

import Data.Group

import Data.Act.Act

-- | A left group torsor.
--
-- The most well known example of a torsor is the particular case of an affine
-- space where the group is the additive group of the vector space and the set
-- is a set of points. Torsors are more general than affine spaces since they
-- don't enforce linearity. Notice that 'LActDistrib' may correspond to a
-- linearity condition if you need one.
--
-- See this nLab article for more information :
-- https://ncatlab.org/nlab/show/torsor
--
-- [In algebraic terms : ]
--
-- A left group action is a torsor if and only if for every pair @(x,y) :: (x,
-- x)@, there exists a unique group element @g :: g@ such that @g <>$ x = y@.
--
-- [In Haskell terms : ]
--
-- Instances must satisfy the following law :
--
-- * @ y .-. x <>$ x == @ @y@
-- * if @g <>$ x == y@ then @g == y .-. x@
--
class LActGp x g => LTorsor x g where
  {-# MINIMAL ldiff | (.-.) #-}
  -- | @ldiff y x@ is the only group element such that @'ldiff' y x <>$ x = y@.
  ldiff :: x -> x -> g
  ldiff x
y x
x = x
y x -> x -> g
forall x g. (LTorsor x g, LTorsor x g) => x -> x -> g
.-. x
x
  infix 6 `ldiff`
  {-# INLINE ldiff #-}

  -- | Infix synonym for 'ldiff'.
  --
  -- This represents a point minus a point.
  --
  (.-.) :: LTorsor x g => x -> x -> g
  (.-.) = x -> x -> g
forall x g. LTorsor x g => x -> x -> g
ldiff
  infix 6 .-.
  {-# INLINE (.-.) #-}


instance LTorsor x () where
  ldiff :: x -> x -> ()
ldiff x
_ x
_ = ()
  {-# INLINE ldiff #-}

instance LTorsor x g => LTorsor x (Identity g) where
  ldiff :: x -> x -> Identity g
ldiff x
y x
x = g -> Identity g
forall a. a -> Identity a
Identity (x -> x -> g
forall x g. LTorsor x g => x -> x -> g
ldiff x
y x
x)
  {-# INLINE ldiff #-}

instance (LTorsor x g, LTorsor y h) => LTorsor (x, y) (g,h) where
  ldiff :: (x, y) -> (x, y) -> (g, h)
ldiff (x
y1, y
y2) (x
x1, y
x2) = (x -> x -> g
forall x g. LTorsor x g => x -> x -> g
ldiff x
y1 x
x1, y -> y -> h
forall x g. LTorsor x g => x -> x -> g
ldiff y
y2 y
x2)
  {-# INLINE ldiff #-}

instance {-# OVERLAPPING #-} LTorsor x g
  => LTorsor (Identity x) (Identity g) where
  ldiff :: Identity x -> Identity x -> Identity g
ldiff (Identity x
y) (Identity x
x) = g -> Identity g
forall a. a -> Identity a
Identity (x -> x -> g
forall x g. LTorsor x g => x -> x -> g
ldiff x
y x
x)
  {-# INLINE ldiff #-}


instance Group g => LTorsor g (ActSelf g) where
  ldiff :: g -> g -> ActSelf g
ldiff g
y g
x = g -> ActSelf g
forall s. s -> ActSelf s
ActSelf (g
y g -> g -> g
forall m. Group m => m -> m -> m
~~ g
x)
  {-# INLINE ldiff #-}

instance (Group g, Coercible x g) => LTorsor x (ActSelf' g) where
  ldiff :: x -> x -> ActSelf' g
ldiff x
y x
x = g -> ActSelf' g
forall x. x -> ActSelf' x
ActSelf' ((x -> g
forall a b. Coercible a b => a -> b
coerce x
y :: g) g -> g -> g
forall m. Group m => m -> m -> m
~~ (x -> g
forall a b. Coercible a b => a -> b
coerce x
x :: g))
  {-# INLINE ldiff #-}


instance RTorsor x g => LTorsor x (Dual g) where
  ldiff :: x -> x -> Dual g
ldiff x
y x
x = g -> Dual g
forall a. a -> Dual a
Dual (x -> x -> g
forall x g. RTorsor x g => x -> x -> g
rdiff x
y x
x)
  {-# INLINE ldiff #-}

instance Num x => LTorsor x (Sum x) where
  ldiff :: x -> x -> Sum x
ldiff x
y x
x = x -> Sum x
forall a. a -> Sum a
Sum (x
y x -> x -> x
forall a. Num a => a -> a -> a
- x
x)
  {-# INLINE ldiff #-}

instance Fractional x => LTorsor x (Product x) where
  ldiff :: x -> x -> Product x
ldiff x
y x
x = x -> Product x
forall a. a -> Product a
Product (x
y x -> x -> x
forall a. Fractional a => a -> a -> a
/ x
x)
  {-# INLINE ldiff #-}



-- | A right group torsor.
--
-- [In algebraic terms : ]
--
-- A left group action is a torsor if and only if for every pair @(x,y) :: (x,
-- x)@, there exists a unique group element @g :: g@ such that @g <>$ x = y@.
--
-- [In Haskell terms : ]
--
-- Instances must satisfy the following law :
--
-- * @ x $<> y .~. x == @ @y@
-- * if @x $<> g == y@ then @g == y .~. x@
--
class RActGp x g => RTorsor x g where
  {-# MINIMAL rdiff | (.~.) #-}
  -- | @rdiff y x@ is the only group element such that @'rdiff' y x $<> x = y@.
  rdiff :: x -> x -> g
  rdiff x
y x
x = x
y x -> x -> g
forall x g. (RTorsor x g, RTorsor x g) => x -> x -> g
.~. x
x
  infix 6 `rdiff`
  {-# INLINE rdiff #-}

  -- | Infix synonym for 'rdiff'.
  --
  -- This represents a point minus a point.
  --
  (.~.) :: RTorsor x g => x -> x -> g
  (.~.) = x -> x -> g
forall x g. RTorsor x g => x -> x -> g
rdiff
  infix 6 .~.
  {-# INLINE (.~.) #-}

instance RTorsor x () where
  rdiff :: x -> x -> ()
rdiff x
_ x
_ = ()
  {-# INLINE rdiff #-}

instance RTorsor x g => RTorsor x (Identity g) where
  rdiff :: x -> x -> Identity g
rdiff x
y x
x = g -> Identity g
forall a. a -> Identity a
Identity (x -> x -> g
forall x g. RTorsor x g => x -> x -> g
rdiff x
y x
x)
  {-# INLINE rdiff #-}

instance {-# OVERLAPPING #-} RTorsor x g
  => RTorsor (Identity x) (Identity g) where
  rdiff :: Identity x -> Identity x -> Identity g
rdiff (Identity x
y) (Identity x
x) = g -> Identity g
forall a. a -> Identity a
Identity (x -> x -> g
forall x g. RTorsor x g => x -> x -> g
rdiff x
y x
x)
  {-# INLINE rdiff #-}

instance (RTorsor x g, RTorsor y h) => RTorsor (x, y) (g,h) where
  rdiff :: (x, y) -> (x, y) -> (g, h)
rdiff (x
y1, y
y2) (x
x1, y
x2) = (x -> x -> g
forall x g. RTorsor x g => x -> x -> g
rdiff x
y1 x
x1, y -> y -> h
forall x g. RTorsor x g => x -> x -> g
rdiff y
y2 y
x2)
  {-# INLINE rdiff #-}

instance Group g => RTorsor g (ActSelf g) where
  rdiff :: g -> g -> ActSelf g
rdiff g
y g
x = g -> ActSelf g
forall s. s -> ActSelf s
ActSelf (g
y g -> g -> g
forall m. Group m => m -> m -> m
~~ g
x)
  {-# INLINE rdiff #-}

instance (Group g, Coercible x g) => RTorsor x (ActSelf' g) where
  rdiff :: x -> x -> ActSelf' g
rdiff x
y x
x = g -> ActSelf' g
forall x. x -> ActSelf' x
ActSelf' ((x -> g
forall a b. Coercible a b => a -> b
coerce x
y :: g) g -> g -> g
forall m. Group m => m -> m -> m
~~ (x -> g
forall a b. Coercible a b => a -> b
coerce x
x :: g))
  {-# INLINE rdiff #-}

instance LTorsor x g => RTorsor x (Dual g) where
  rdiff :: x -> x -> Dual g
rdiff x
y x
x = g -> Dual g
forall a. a -> Dual a
Dual (x -> x -> g
forall x g. LTorsor x g => x -> x -> g
ldiff x
y x
x)
  {-# INLINE rdiff #-}

instance Num x => RTorsor x (Sum x) where
  rdiff :: x -> x -> Sum x
rdiff x
y x
x = x -> Sum x
forall a. a -> Sum a
Sum (x
y x -> x -> x
forall a. Num a => a -> a -> a
- x
x)
  {-# INLINE rdiff #-}

instance Fractional x => RTorsor x (Product x) where
  rdiff :: x -> x -> Product x
rdiff x
y x
x = x -> Product x
forall a. a -> Product a
Product (x
y x -> x -> x
forall a. Fractional a => a -> a -> a
/ x
x)
  {-# INLINE rdiff #-}