{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}

-- |

-- Module      : OAlg.Structure.Distributive.Definition

-- Description : definition for distributive structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- distributive structures, i.e. multiplicative structures with a suitable additive structure.

module OAlg.Structure.Distributive.Definition
  ( -- * Distributive

    Distributive, Dst, TransformableDst, tauDst

    -- * Transposable

  , TransposableDistributive
  )
  where

import Data.Kind

import OAlg.Prelude

import OAlg.Structure.Oriented.Definition
import OAlg.Structure.Oriented.Opposite
import OAlg.Structure.Multiplicative.Definition
import OAlg.Structure.Fibred.Definition
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive.Definition

--------------------------------------------------------------------------------

-- Distributive -


-- | 'FibredOriented' structures equipped with an 'Additive' and 'Multiplicative' structure

-- satisfying the laws of __/distributivity/__.

--

-- __Properties__ Let @__d__@ be a 'Distributive' structure, then holds:

--

-- (1) #Dst1#For all @g@ in @__d__@ and @r@ in @'Root' __d__@ with

-- @'end' g '==' 'start' r@ holds: @'zero' r '*' g '==' 'zero' r'@

-- where @r' '==' 'start' g ':>' 'end' r@.

--

-- (2) #Dst2#For all @g@, @a@ and @b@ in @__d__@ with @'root' a '==' 'root' b@ and

-- @'start' a '==' 'end' g@ holds: @(a '+' b) '*' g == a'*'g '+' b'*'g@.

--

-- (3) #Dst3#For all @f@ in @__d__@ and @r@ in @'Root' __d__@ with

-- @'start' f '==' 'end' r@ holds: @f '*' 'zero' r '==' 'zero' r'@

-- where @r' = 'start' r ':>' 'end' f@.

--

-- (4) #Dst4#For all @f@, @a@ and @b@ in @__d__@ with @'root' a '==' 'root' b@ and

-- @'start' f '==' 'end' a@ holds: @f'*'(a '+' b) == f'*'a '+' f'*'b@.

--

-- __Note__ If @__d__@ is interpreted as a small category @__C__@ then it is usually called

-- __preadditive__. If @__d__@ is also 'Abelian' then @__C__@ is also usually called

-- __abelian__.

class (FibredOriented d, Additive d, Multiplicative d) => Distributive d

instance Distributive ()
instance Distributive Int
instance Distributive Integer
instance Distributive N
instance Distributive Z
instance Distributive Q
instance Entity p => Distributive (Orientation p)
instance Distributive d => Distributive (Op d)
instance Distributive d => Distributive (Id d)

--------------------------------------------------------------------------------

-- Transposable -


-- | transposable distributive structures.

--

-- __Property__ Let @__d__@ be a 'TransposableDistributive' structure, then holds:

--

-- (1) For all @r@ in @'Root' d@ holds:

-- @'transpose' ('zero' r) '==' 'zero' ('transpose' r)@

--

-- (2) For all @a@, @b@ in @__d__@ with @'root' a '==' 'root' b@ holds:

-- @'transpose' (a '+' b) '==' 'transpose' a '+' 'transpose' b@.

class (TransposableMultiplicative d, Distributive d) => TransposableDistributive d

instance Entity p => TransposableDistributive (Orientation p)
instance TransposableDistributive N
instance TransposableDistributive Z
instance TransposableDistributive Q

--------------------------------------------------------------------------------

-- Dst -

  
-- | type representing the class of 'Distributive' structures.

data Dst

type instance Structure Dst x = Distributive x

instance Transformable Dst Type where tau :: forall x. Struct Dst x -> Struct (*) x
tau Struct Dst x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct
instance TransformableType Dst

instance Transformable Dst Typ where tau :: forall x. Struct Dst x -> Struct Typ x
tau Struct Dst x
Struct = Struct Typ x
forall s x. Structure s x => Struct s x
Struct
instance Transformable Dst Ent where tau :: forall x. Struct Dst x -> Struct Ent x
tau Struct Dst x
Struct = Struct Ent x
forall s x. Structure s x => Struct s x
Struct
instance Transformable Dst Ort where tau :: forall x. Struct Dst x -> Struct Ort x
tau Struct Dst x
Struct = Struct Ort x
forall s x. Structure s x => Struct s x
Struct
instance Transformable Dst Mlt where tau :: forall x. Struct Dst x -> Struct Mlt x
tau Struct Dst x
Struct = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct
instance Transformable Dst Fbr where tau :: forall x. Struct Dst x -> Struct Fbr x
tau Struct Dst x
Struct = Struct Fbr x
forall s x. Structure s x => Struct s x
Struct
instance Transformable Dst FbrOrt where tau :: forall x. Struct Dst x -> Struct FbrOrt x
tau Struct Dst x
Struct = Struct FbrOrt x
forall s x. Structure s x => Struct s x
Struct
instance Transformable Dst Add where tau :: forall x. Struct Dst x -> Struct Add x
tau Struct Dst x
Struct = Struct Add x
forall s x. Structure s x => Struct s x
Struct
instance TransformableG Op Dst Dst where tauG :: forall x. Struct Dst x -> Struct Dst (Op x)
tauG Struct Dst x
Struct = Struct Dst (Op x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableG Op (Dst,t) Dst where tauG :: forall x. Struct (Dst, t) x -> Struct Dst (Op x)
tauG = Struct Dst x -> Struct Dst (Op x)
forall x. Struct Dst x -> Struct Dst (Op x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG (Struct Dst x -> Struct Dst (Op x))
-> (Struct (Dst, t) x -> Struct Dst x)
-> Struct (Dst, t) x
-> Struct Dst (Op x)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (Dst, t) x -> Struct Dst x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance TransformableOp Dst
instance TransformableGRefl Op Dst

--------------------------------------------------------------------------------

-- tauDst -


-- | 'tau' for 'Dst'.

tauDst :: Transformable s Dst => Struct s x -> Struct Dst x
tauDst :: forall s x. Transformable s Dst => Struct s x -> Struct Dst x
tauDst = Struct s x -> Struct Dst x
forall x. Struct s x -> Struct Dst x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau

--------------------------------------------------------------------------------

-- TransformableDst -


-- | helper class to avoid undecidable instances.

class ( TransformableFbrOrt s
      , TransformableMlt s
      , TransformableAdd s
      , Transformable s Dst
      ) => TransformableDst s

instance TransformableTyp Dst
instance TransformableOrt Dst
instance TransformableMlt Dst
instance TransformableFbr Dst
instance TransformableFbrOrt Dst
instance TransformableAdd Dst
instance TransformableDst Dst