{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}

-- |

-- Module      : OAlg.Category.Unify

-- Description : unification of categories

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- unification of categories, i.e. projecting morphisms by dropping the parameterization by there

-- 'domain' and 'range'.

module OAlg.Category.Unify
  (
    -- * Morphism

    SomeMorphism(..), SomeObjectClass(..)
  , SomeMorphismSite(..)
  , someOne
  , SomeCmpb3(..), SomeCmpb2(..), smCmpb2
  
    -- * Path

  , SomePath(..), somePath
  , SomePathSite(..)
  
    -- * Entity

  , SomeEntity(..)

    -- * Application

  , SomeApplication(..)
  , xSomeAppl

  )
  where

import Data.Typeable
import Data.Type.Equality

import Data.List ((++))

import OAlg.Category.Definition
import OAlg.Structure.Definition
import OAlg.Category.Path

import OAlg.Data.Identity
import OAlg.Data.X
import OAlg.Data.Dualisable
import OAlg.Data.Validable
import OAlg.Data.Maybe
import OAlg.Data.Equal
import OAlg.Data.Show
import OAlg.Data.Boolean

import OAlg.Entity.Definition

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

-- SomeApplication -


-- | some application.

data SomeApplication h where
  SomeApplication :: h x y -> x -> SomeApplication h

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

-- xSomeAppl -


-- | random variable for some application.

xSomeAppl :: (Morphism m, Transformable (ObjectClass m) XStd) => m x y -> X (SomeApplication m)
xSomeAppl :: forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) XStd) =>
m x y -> X (SomeApplication m)
xSomeAppl m x y
m = (x -> SomeApplication m) -> X x -> X (SomeApplication m)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (m x y -> x -> SomeApplication m
forall (h :: * -> * -> *) x y. h x y -> x -> SomeApplication h
SomeApplication m x y
m) (m x y -> X x
forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) XStd) =>
m x y -> X x
xStd m x y
m)


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

-- SomeMorphism -


-- | some morphism.

data SomeMorphism m where
  SomeMorphism :: m x y -> SomeMorphism m

instance Show2 m => Show (SomeMorphism m) where
  show :: SomeMorphism m -> String
show (SomeMorphism m x y
f) = String
"SomeMorphism[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ m x y -> String
forall a b. m a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 m x y
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

instance (Morphism m, TransformableObjectClassTyp m, Typeable m, Eq2 m)
  => Eq (SomeMorphism m) where
  SomeMorphism m x y
f == :: SomeMorphism m -> SomeMorphism m -> Bool
== SomeMorphism m x y
g = case Struct Typ x
-> Struct Typ x
-> Struct Typ y
-> Struct Typ y
-> m x y
-> m x y
-> Maybe (m x y :~: m x y)
forall (m :: * -> * -> *) x x' y y'.
Typeable m =>
Struct Typ x
-> Struct Typ x'
-> Struct Typ y
-> Struct Typ y'
-> m x y
-> m x' y'
-> Maybe (m x y :~: m x' y')
eqlMorphism Struct Typ x
Struct (ObjectClass (Sub Typ m)) x
tx Struct Typ x
Struct (ObjectClass (Sub Typ m)) x
tx' Struct Typ y
Struct (ObjectClass (Sub Typ m)) y
ty Struct Typ y
Struct (ObjectClass (Sub Typ m)) y
ty' m x y
f m x y
g of
    Just m x y :~: m x y
Refl -> m x y -> m x y -> Bool
forall x y. m x y -> m x y -> Bool
forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 m x y
f m x y
m x y
g
    Maybe (m x y :~: m x y)
Nothing   -> Bool
False

    where tx :: Struct (ObjectClass (Sub Typ m)) x
tx  = Sub Typ m x y -> Struct (ObjectClass (Sub Typ m)) x
forall x y. Sub Typ m x y -> Struct (ObjectClass (Sub Typ m)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain (m x y -> Sub Typ m x y
forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) Typ) =>
m x y -> Sub Typ m x y
subTyp m x y
f)
          tx' :: Struct (ObjectClass (Sub Typ m)) x
tx' = Sub Typ m x y -> Struct (ObjectClass (Sub Typ m)) x
forall x y. Sub Typ m x y -> Struct (ObjectClass (Sub Typ m)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain (m x y -> Sub Typ m x y
forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) Typ) =>
m x y -> Sub Typ m x y
subTyp m x y
g)
          ty :: Struct (ObjectClass (Sub Typ m)) y
ty  = Sub Typ m x y -> Struct (ObjectClass (Sub Typ m)) y
forall x y. Sub Typ m x y -> Struct (ObjectClass (Sub Typ m)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range (m x y -> Sub Typ m x y
forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) Typ) =>
m x y -> Sub Typ m x y
subTyp m x y
f)
          ty' :: Struct (ObjectClass (Sub Typ m)) y
ty' = Sub Typ m x y -> Struct (ObjectClass (Sub Typ m)) y
forall x y. Sub Typ m x y -> Struct (ObjectClass (Sub Typ m)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range (m x y -> Sub Typ m x y
forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) Typ) =>
m x y -> Sub Typ m x y
subTyp m x y
g)

          subTypStruct :: Struct Typ x -> Struct Typ y -> m x y -> Sub Typ m x y
          subTypStruct :: forall x y (m :: * -> * -> *).
Struct Typ x -> Struct Typ y -> m x y -> Sub Typ m x y
subTypStruct Struct Typ x
Struct Struct Typ y
Struct = m x y -> Sub Typ m x y
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub
          
          subTyp :: (Morphism m, Transformable (ObjectClass m) Typ) => m x y -> Sub Typ m x y
          subTyp :: forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) Typ) =>
m x y -> Sub Typ m x y
subTyp m x y
m = Struct Typ x -> Struct Typ y -> m x y -> Sub Typ m x y
forall x y (m :: * -> * -> *).
Struct Typ x -> Struct Typ y -> m x y -> Sub Typ m x y
subTypStruct (Struct (ObjectClass m) x -> Struct Typ x
forall x. Struct (ObjectClass m) x -> Struct Typ x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass m) x -> Struct Typ x)
-> Struct (ObjectClass m) x -> Struct Typ x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ m x y -> Struct (ObjectClass m) x
forall x y. m x y -> Struct (ObjectClass m) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain m x y
m) (Struct (ObjectClass m) y -> Struct Typ y
forall x. Struct (ObjectClass m) x -> Struct Typ x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass m) y -> Struct Typ y)
-> Struct (ObjectClass m) y -> Struct Typ y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ m x y -> Struct (ObjectClass m) y
forall x y. m x y -> Struct (ObjectClass m) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range m x y
m) m x y
m 


instance Validable2 m => Validable (SomeMorphism m) where
  valid :: SomeMorphism m -> Statement
valid (SomeMorphism m x y
f) = m x y -> Statement
forall x y. m x y -> Statement
forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 m x y
f

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

-- SomeCmpb2 -


-- | some composable morphisms.

data SomeCmpb2 c where
  SomeCmpb2 :: c y z -> c x y -> SomeCmpb2 c
  
--------------------------------------------------------------------------------

-- SomeCmpb3 -


-- | some composable morphisms.

data SomeCmpb3 c where
  SomeCmpb3 :: c x w -> c y x ->  c z y -> SomeCmpb3 c

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

-- smCmpb2 -


-- | composing the two composables.

smCmpb2 :: Category h => SomeCmpb2 h -> SomeMorphism h
smCmpb2 :: forall (h :: * -> * -> *).
Category h =>
SomeCmpb2 h -> SomeMorphism h
smCmpb2 (SomeCmpb2 h y z
f h x y
g) = h x z -> SomeMorphism h
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (h y z
f h y z -> h x y -> h x z
forall y z x. h y z -> h x y -> h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h x y
g)


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

-- SomeEntity -


-- | some entity @x@ in @__x__@ having the given @'ObjectClass' __m__@ as structure.

data SomeEntity m where
  SomeEntity :: Entity x => Struct (ObjectClass m) x -> x -> SomeEntity m

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

-- SomePath -


-- | some path

data SomePath m where
  SomePath :: Path m x y -> SomePath m 

instance Show2 m => Show (SomePath m) where
  show :: SomePath m -> String
show (SomePath Path m x y
pth) = String
"SomePath[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Path m x y -> String
forall a b. Path m a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 Path m x y
pth String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

type instance Dual (SomePath m) = SomePath (Op2 m)

instance Morphism m => Dualisable (SomePath m) where
  toDual :: SomePath m -> Dual (SomePath m)
toDual (SomePath Path m x y
pth) = Path (Op2 m) y x -> SomePath (Op2 m)
forall (m :: * -> * -> *) x y. Path m x y -> SomePath m
SomePath (Path (Op2 m) y x -> SomePath (Op2 m))
-> Path (Op2 m) y x -> SomePath (Op2 m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Path m x y -> Dual (Path m x y)
forall x. Dualisable x => x -> Dual x
toDual Path m x y
pth
  fromDual :: Dual (SomePath m) -> SomePath m
fromDual (SomePath Path (Op2 m) x y
pth') = Path m y x -> SomePath m
forall (m :: * -> * -> *) x y. Path m x y -> SomePath m
SomePath (Path m y x -> SomePath m) -> Path m y x -> SomePath m
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dual (Path m y x) -> Path m y x
forall x. Dualisable x => Dual x -> x
fromDual Dual (Path m y x)
Path (Op2 m) x y
pth'
  
--------------------------------------------------------------------------------

-- SomeObjectClass -


-- | some object class.

data SomeObjectClass m where
  SomeObjectClass :: Transformable (ObjectClass m) Typ
    => Struct (ObjectClass m) x -> SomeObjectClass m

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

-- SomeObjectClass - Dualisable -


type instance Dual (SomeObjectClass m) = SomeObjectClass (Op2 m)

instance Dualisable (SomeObjectClass m) where
  toDual :: SomeObjectClass m -> Dual (SomeObjectClass m)
toDual (SomeObjectClass Struct (ObjectClass m) x
s) = Struct (ObjectClass (Op2 m)) x -> SomeObjectClass (Op2 m)
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass Struct (ObjectClass m) x
Struct (ObjectClass (Op2 m)) x
s
  fromDual :: Dual (SomeObjectClass m) -> SomeObjectClass m
fromDual (SomeObjectClass Struct (ObjectClass (Op2 m)) x
s) = Struct (ObjectClass m) x -> SomeObjectClass m
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass Struct (ObjectClass m) x
Struct (ObjectClass (Op2 m)) x
s

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

-- SomeObjectClass - Entity -


deriving instance Show (SomeObjectClass m)

instance Eq (SomeObjectClass m) where
  SomeObjectClass Struct (ObjectClass m) x
o == :: SomeObjectClass m -> SomeObjectClass m -> Bool
== SomeObjectClass Struct (ObjectClass m) x
o' = case Struct (ObjectClass m) x
-> Struct (ObjectClass m) x -> Maybe (x :~: x)
forall a b.
Struct (ObjectClass m) a
-> Struct (ObjectClass m) b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct (ObjectClass m) x
o Struct (ObjectClass m) x
o' of
    Just x :~: x
Refl -> Struct (ObjectClass m) x
o Struct (ObjectClass m) x -> Struct (ObjectClass m) x -> Bool
forall a. Eq a => a -> a -> Bool
== Struct (ObjectClass m) x
Struct (ObjectClass m) x
o'
    Maybe (x :~: x)
Nothing   -> Bool
False

instance Validable (SomeObjectClass m) where
  valid :: SomeObjectClass m -> Statement
valid (SomeObjectClass Struct (ObjectClass m) x
o) = Struct (ObjectClass m) x -> Statement
forall a. Validable a => a -> Statement
valid Struct (ObjectClass m) x
o

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

-- someOne


-- | some 'cOne' for some object class.

someOne :: Category c => SomeObjectClass c -> SomeMorphism c
someOne :: forall (c :: * -> * -> *).
Category c =>
SomeObjectClass c -> SomeMorphism c
someOne (SomeObjectClass Struct (ObjectClass c) x
s) = c x x -> SomeMorphism c
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne Struct (ObjectClass c) x
s) 

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

-- SomePathSite -


-- | some path parameterized either by its 'domain' or 'range'.

data SomePathSite s m x where
  SomePathDomain :: Path m x y -> SomePathSite From m x
  SomePathRange  :: Path m x y -> SomePathSite To m y

type instance Dual (SomePathSite s m y) = SomePathSite (Dual s) (Op2 m) y

instance Morphism m => Dualisable (SomePathSite To m y) where
  toDual :: SomePathSite 'To m y -> Dual (SomePathSite 'To m y)
toDual (SomePathRange Path m x y
pth) = Path (Op2 m) y x -> SomePathSite 'From (Op2 m) y
forall (m :: * -> * -> *) x x. Path m x x -> SomePathSite 'From m x
SomePathDomain (Path m x y -> Dual (Path m x y)
forall x. Dualisable x => x -> Dual x
toDual Path m x y
pth)
  fromDual :: Dual (SomePathSite 'To m y) -> SomePathSite 'To m y
fromDual (SomePathDomain Path (Op2 m) y y
pth') = Path m y y -> SomePathSite 'To m y
forall (m :: * -> * -> *) x y. Path m x y -> SomePathSite 'To m y
SomePathRange (Dual (Path m y y) -> Path m y y
forall x. Dualisable x => Dual x -> x
fromDual Dual (Path m y y)
Path (Op2 m) y y
pth')

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

-- somePath -


-- | embedding.

somePath :: SomePathSite s m x -> SomePath m
somePath :: forall (s :: Site) (m :: * -> * -> *) x.
SomePathSite s m x -> SomePath m
somePath (SomePathDomain Path m x y
pth) = Path m x y -> SomePath m
forall (m :: * -> * -> *) x y. Path m x y -> SomePath m
SomePath Path m x y
pth
somePath (SomePathRange Path m x x
pth) = Path m x x -> SomePath m
forall (m :: * -> * -> *) x y. Path m x y -> SomePath m
SomePath Path m x x
pth

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

-- SomeMorphismSite -


-- | some morphism given by a 'Site'.

data SomeMorphismSite s m x where
  SomeMorphismDomain :: m x y -> SomeMorphismSite From m x
  SomeMorphismRange  :: m x y -> SomeMorphismSite To m y

type instance Dual (SomeMorphismSite s m y) = SomeMorphismSite (Dual s) (Op2 m) y

instance Dualisable (SomeMorphismSite To m y) where
  toDual :: SomeMorphismSite 'To m y -> Dual (SomeMorphismSite 'To m y)
toDual (SomeMorphismRange m x y
m) = Op2 m y x -> SomeMorphismSite 'From (Op2 m) y
forall (m :: * -> * -> *) x x. m x x -> SomeMorphismSite 'From m x
SomeMorphismDomain (m x y -> Op2 m y x
forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2 m x y
m)
  fromDual :: Dual (SomeMorphismSite 'To m y) -> SomeMorphismSite 'To m y
fromDual (SomeMorphismDomain (Op2 m y y
m)) = m y y -> SomeMorphismSite 'To m y
forall (m :: * -> * -> *) x y. m x y -> SomeMorphismSite 'To m y
SomeMorphismRange m y y
m