-- --< Header >-- {{{

{-# LANGUAGE GADTs, ExplicitNamespaces, QuantifiedConstraints #-}

{- |

Description : Evidence t'Data.Hetero.Evidence.Exactly.Exactly' corresponding to each t'Data.Hetero.Role.Role'
Copyright   : (c) L. S. Leary, 2025

Evidence 'Exactly' corresponding to each 'Role'.

-}

-- }}}

-- --< Exports >-- {{{

module Data.Hetero.Evidence.Exactly (

  -- * Exactly
  Exactly(..),
  roleEx,
  reflEx,
  symEx,
  transEx,
  hetTransEx,
  maxEx,
  weakenEx,
  applyEx,
  innerEx,

) where

-- }}}

-- --< Imports >-- {{{

-- base
import Prelude hiding (id, (.))
import Data.Type.Equality ((:~:)(..))
import Data.Type.Ord (OrderingI(..), Min, Max)
import Data.Coerce (Coercible)
import Control.Category (Category(..))

-- ord-axiomata
import Data.Type.Ord.Axiomata (type (<=), TotalOrder(..))

-- heterogeneous-comparison
import Data.Hetero.Role
  ( RoleKind(..), Role(..), KnownRole(..), expositRole
  , SubNominal, SuperPhantom
  )

-- }}}

-- --< Exactly >-- {{{

{- |

Evidence of equivalence, /exactly/ corresponding to an associated role.

 +---------------------+-------------------+-------------------+
 |  'Role'             | Equivalence       | Evidence          |
 +=====================+===================+===================+
 | v'Phantom'          | Trivial/Universal | @()@              |
 +---------------------+-------------------+-------------------+
 | v'Representational' | Representational  | @'Coercible' a b@ |
 +---------------------+-------------------+-------------------+
 | v'Nominal'          | Nominal           | @a ~ b@           |
 +---------------------+-------------------+-------------------+

-}
data Exactly (r :: RoleKind) a b where
  PhantEx ::                  Exactly Phantom          a b
  ReprEx  :: Coercible a b => Exactly Representational a b
  NomEx   ::                  Exactly Nominal          a a

instance KnownRole r => Category (Exactly r) where
  id :: forall (a :: k). Exactly r a a
id  = Exactly r a a
forall {k} (r :: RoleKind) (a :: k). KnownRole r => Exactly r a a
reflEx
  . :: forall (b :: k) (c :: k) (a :: k).
Exactly r b c -> Exactly r a b -> Exactly r a c
(.) = (Exactly r a b -> Exactly r b c -> Exactly r a c)
-> Exactly r b c -> Exactly r a b -> Exactly r a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Exactly r a b -> Exactly r b c -> Exactly r a c
forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k).
Exactly r a b -> Exactly r b c -> Exactly r a c
transEx

-- | The 'Role' to which a piece of evidence 'Exactly' corresponds.
roleEx :: Exactly r a b -> Role r
roleEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx = \case
  Exactly r a b
PhantEx -> Role r
Role Phantom
Phantom
  Exactly r a b
ReprEx  -> Role r
Role Representational
Representational
  Exactly r a b
NomEx   -> Role r
Role Nominal
Nominal

-- | Reflexivity.
reflEx :: forall r a. KnownRole r => Exactly r a a
reflEx :: forall {k} (r :: RoleKind) (a :: k). KnownRole r => Exactly r a a
reflEx = case forall (r :: RoleKind). KnownRole r => Role r
knownRole @r of
  Role r
Phantom          -> Exactly r a a
Exactly Phantom a a
forall {k} (a :: k) (b :: k). Exactly Phantom a b
PhantEx
  Role r
Representational -> Exactly r a a
Exactly Representational a a
forall {k} (a :: k) (b :: k).
Coercible a b =>
Exactly Representational a b
ReprEx
  Role r
Nominal          -> Exactly r a a
Exactly Nominal a a
forall {k} (a :: k). Exactly Nominal a a
NomEx

-- | Symmetry.
symEx :: Exactly r a b -> Exactly r b a
symEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Exactly r b a
symEx = \case
  Exactly r a b
PhantEx -> Exactly r b a
Exactly Phantom b a
forall {k} (a :: k) (b :: k). Exactly Phantom a b
PhantEx
  Exactly r a b
ReprEx  -> Exactly r b a
Exactly Representational b a
forall {k} (a :: k) (b :: k).
Coercible a b =>
Exactly Representational a b
ReprEx
  Exactly r a b
NomEx   -> Exactly r b a
Exactly Nominal b b
forall {k} (a :: k). Exactly Nominal a a
NomEx

-- | 'Role'-homogeneous transitivity.
transEx :: Exactly r a b -> Exactly r b c -> Exactly r a c
transEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k).
Exactly r a b -> Exactly r b c -> Exactly r a c
transEx Exactly r a b
PhantEx Exactly r b c
PhantEx = Exactly r a c
Exactly Phantom a c
forall {k} (a :: k) (b :: k). Exactly Phantom a b
PhantEx
transEx Exactly r a b
ReprEx  Exactly r b c
ReprEx  = Exactly r a c
Exactly Representational a c
forall {k} (a :: k) (b :: k).
Coercible a b =>
Exactly Representational a b
ReprEx
transEx Exactly r a b
NomEx   Exactly r b c
NomEx   = Exactly r a c
Exactly Nominal a a
forall {k} (a :: k). Exactly Nominal a a
NomEx

{- |

'Exactly' is a category graded by the 'Min' monoid on 'RoleKind' with identity:

@
'NomEx' :: 'Exactly' t'Nominal' a a
@

-}
hetTransEx
  :: forall r s a b c
  .  Exactly r a b -> Exactly s b c {- ^ -}
  -> Exactly (Min r s) a c
hetTransEx :: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k)
       (c :: k).
Exactly r a b -> Exactly s b c -> Exactly (Min r s) a c
hetTransEx Exactly r a b
e1 Exactly s b c
e2 = case Sing RoleKind r
Role r
r Sing RoleKind r -> Sing RoleKind s -> OrderingI r s
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
forall (a :: RoleKind) (b :: RoleKind).
Sing RoleKind a -> Sing RoleKind b -> OrderingI a b
<|=|> Sing RoleKind s
Role s
s of
  OrderingI r s
LTI -> Role r -> (KnownRole r => Exactly r a c) -> Exactly r a c
forall (r :: RoleKind) s. Role r -> (KnownRole r => s) -> s
expositRole Role r
r (Exactly r a b -> Exactly r b c -> Exactly r a c
forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k).
Exactly r a b -> Exactly r b c -> Exactly r a c
transEx           Exactly r a b
e1 (Exactly s b c -> Exactly r b c
forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, r <= s) =>
Exactly s a b -> Exactly r a b
weakenEx Exactly s b c
e2))
  OrderingI r s
EQI ->                Exactly r a b -> Exactly r b c -> Exactly r a c
forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k).
Exactly r a b -> Exactly r b c -> Exactly r a c
transEx           Exactly r a b
e1           Exactly r b c
Exactly s b c
e2
  OrderingI r s
GTI -> Role s -> (KnownRole s => Exactly s a c) -> Exactly s a c
forall (r :: RoleKind) s. Role r -> (KnownRole r => s) -> s
expositRole Role s
s case Sing RoleKind s
-> Sing RoleKind r -> Compare s r :~: Reflect (Compare r s)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Compare a b :~: Reflect (Compare b a)
forall (a :: RoleKind) (b :: RoleKind).
Sing RoleKind a
-> Sing RoleKind b -> Compare a b :~: Reflect (Compare b a)
antiSym Sing RoleKind s
Role s
s Sing RoleKind r
Role r
r of
    Compare s r :~: Reflect (Compare r s)
Refl ->             Exactly s a b -> Exactly s b c -> Exactly s a c
forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k).
Exactly r a b -> Exactly r b c -> Exactly r a c
transEx (Exactly r a b -> Exactly s a b
forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, r <= s) =>
Exactly s a b -> Exactly r a b
weakenEx Exactly r a b
e1)          Exactly s b c
e2
 where
  r :: Role r
r = Exactly r a b -> Role r
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly r a b
e1
  s :: Role s
s = Exactly s b c -> Role s
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly s b c
e2

{- |

@'Exactly' _ a b@ is a monoid graded by the 'Max' monoid on 'RoleKind' with identity:

@
'PhantEx' :: 'Exactly' t'Phantom' a b
@

-}
maxEx
  :: Exactly r a b -> Exactly s a b {- ^ -}
  -> Exactly (Max r s) a b
maxEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
Exactly r a b -> Exactly s a b -> Exactly (Max r s) a b
maxEx Exactly r a b
e1 Exactly s a b
e2 = case Exactly r a b -> Role r
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly r a b
e1 Sing RoleKind r -> Sing RoleKind s -> OrderingI r s
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
forall (a :: RoleKind) (b :: RoleKind).
Sing RoleKind a -> Sing RoleKind b -> OrderingI a b
<|=|> Exactly s a b -> Role s
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly s a b
e2 of
  OrderingI r s
LTI -> Exactly s a b
Exactly (Max r s) a b
e2
  OrderingI r s
EQI -> Exactly s a b
Exactly (Max r s) a b
e2
  OrderingI r s
GTI -> Exactly r a b
Exactly (Max r s) a b
e1

-- | Weaken evidence for one 'Role' to evidence for a lesser @Role@.
weakenEx
  :: forall r s a b
   . (KnownRole r, r <= s)
  => Exactly s a b -> Exactly r a b
weakenEx :: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, r <= s) =>
Exactly s a b -> Exactly r a b
weakenEx Exactly s a b
e = case forall (r :: RoleKind). KnownRole r => Role r
knownRole @r of
  Role r
Phantom          -> Exactly r a b
Exactly Phantom a b
forall {k} (a :: k) (b :: k). Exactly Phantom a b
PhantEx
  Role r
Representational -> case Exactly s a b
e of
    Exactly s a b
ReprEx -> Exactly r a b
Exactly Representational a b
forall {k} (a :: k) (b :: k).
Coercible a b =>
Exactly Representational a b
ReprEx
    Exactly s a b
NomEx  -> Exactly r a b
Exactly Representational a b
forall {k} (a :: k) (b :: k).
Coercible a b =>
Exactly Representational a b
ReprEx
  Role r
Nominal          -> case Exactly s a b
e of
    Exactly s a b
NomEx  -> Exactly r a b
Exactly Nominal a a
forall {k} (a :: k). Exactly Nominal a a
NomEx

-- | If 'SubNominal' functions and their arguments are equivalent, then so are their respective applications.
applyEx
  :: SubNominal g
  => Exactly r f g -> Exactly r a b {- ^ -}
  -> Exactly r (f a) (g b)
applyEx :: forall {k} {k} (g :: k -> k) (r :: RoleKind) (f :: k -> k) (a :: k)
       (b :: k).
SubNominal g =>
Exactly r f g -> Exactly r a b -> Exactly r (f a) (g b)
applyEx Exactly r f g
PhantEx Exactly r a b
PhantEx = Exactly r (f a) (g b)
Exactly Phantom (f a) (g b)
forall {k} (a :: k) (b :: k). Exactly Phantom a b
PhantEx
applyEx Exactly r f g
ReprEx  Exactly r a b
ReprEx  = Exactly r (f a) (g b)
Exactly Representational (f a) (g b)
forall {k} (a :: k) (b :: k).
Coercible a b =>
Exactly Representational a b
ReprEx
applyEx Exactly r f g
NomEx   Exactly r a b
NomEx   = Exactly r (f a) (g b)
Exactly Nominal (f a) (f a)
forall {k} (a :: k). Exactly Nominal a a
NomEx

-- | If applications by @'SuperPhantom' f@ are equivalent, then so are the arguments.
innerEx
  :: SuperPhantom f
  => Exactly r (f a) (f b) {- ^ -}
  -> Exactly r a b
innerEx :: forall {k} {k} (f :: k -> k) (r :: RoleKind) (a :: k) (b :: k).
SuperPhantom f =>
Exactly r (f a) (f b) -> Exactly r a b
innerEx = \case
  Exactly r (f a) (f b)
PhantEx -> Exactly r a b
Exactly Phantom a b
forall {k} (a :: k) (b :: k). Exactly Phantom a b
PhantEx
  Exactly r (f a) (f b)
ReprEx  -> Exactly r a b
Exactly Representational a b
forall {k} (a :: k) (b :: k).
Coercible a b =>
Exactly Representational a b
ReprEx
  Exactly r (f a) (f b)
NomEx   -> Exactly r a b
Exactly Nominal a a
forall {k} (a :: k). Exactly Nominal a a
NomEx

-- }}}