-- |
-- Module      : Control.Natural.IsoF
-- Copyright   : (c) Justin Le 2019
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Types describing isomorphisms between two functors, and functions to
-- manipulate them.
module Control.Natural.IsoF (
    type (~>)
  , type (<~>)
  , isoF
  , coercedF
  , viewF, reviewF, overF
  , fromF
  ) where

import           Control.Natural
import           Data.Coerce
import           Data.Kind
import           Data.Profunctor
import           Data.Tagged

-- | The type of an isomorphism between two functors.  @f '<~>' g@ means that
-- @f@ and @g@ are isomorphic to each other.
--
-- We can effectively /use/ an @f \<~\> g@ with:
--
-- @
-- 'viewF'   :: (f \<~\> g) -> f a -> g a
-- 'reviewF' :: (f \<~\> g) -> g a -> a a
-- @
--
-- Use 'viewF' to extract the "@f@ to @g@" function, and 'reviewF' to
-- extract the "@g@ to @f@" function.  Reviewing and viewing the same value
-- (or vice versa) leaves the value unchanged.
--
-- One nice thing is that we can compose isomorphisms using '.' from
-- "Prelude":
--
-- @
-- ('.') :: f \<~\> g
--     -> g \<~\> h
--     -> f \<~\> h
-- @
--
-- Another nice thing about this representation is that we have the
-- "identity" isomorphism by using 'id' from "Prelude".
--
-- @
-- 'id' :: f '<~>' g
-- @
--
-- As a convention, most isomorphisms have form "X-ing", where the
-- forwards function is "ing".  For example, we have:
--
-- @
-- 'Data.HBifunctor.Tensor.splittingSF' :: 'Data.HBifunctor.Tensor.Monoidal' t => 'Data.HBifunctor.Associative.SF' t a '<~>' t f ('Data.HBifunctor.Tensor.MF' t f)
-- 'Data.HBifunctor.Tensor.splitSF'     :: Monoidal t => SF t a  '~>' t f (MF t f)
-- @
type f <~> g  = forall p a. Profunctor p => p (g a) (g a) -> p (f a) (f a)
infixr 0 <~>

-- | Create an @f '<~>' g@ by providing both legs of the isomorphism (the
-- @f a -> g a@ and the @g a -> f a@.
isoF
    :: f ~> g
    -> g ~> f
    -> f <~> g
isoF :: forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF f ~> g
f g ~> f
g p (g a) (g a)
a = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap f ~> g
f g ~> f
g p (g a) (g a)
a

-- | An isomorphism between two functors that are coercible/have the same
-- internal representation.  Useful for newtype wrappers.
coercedF :: forall f g. (forall x. Coercible (f x) (g x), forall x. Coercible (g x) (f x)) => f <~> g
coercedF :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
 forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
coercedF = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF coerce :: forall a b. Coercible a b => a -> b
coerce coerce :: forall a b. Coercible a b => a -> b
coerce

-- | Use a '<~>' by retrieving the "forward" function:
--
-- @
-- 'viewF'   :: (f <~> g) -> f a -> g a
-- @
viewF :: f <~> g -> f ~> g
viewF :: forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF f <~> g
i = forall {k} r a (b :: k). Forget r a b -> a -> r
runForget (f <~> g
i (forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget forall a. a -> a
id))

-- | Use a '<~>' by retrieving the "backwards" function:
--
-- @
-- 'viewF'   :: (f <~> g) -> f a -> g a
-- @
reviewF :: f <~> g -> g ~> f
reviewF :: forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF f <~> g
i g x
x = forall {k} (s :: k) b. Tagged s b -> b
unTagged (f <~> g
i (forall {k} (s :: k) b. b -> Tagged s b
Tagged g x
x))

-- | Lift a function @g a ~> g a@ to be a function @f a -> f a@, given an
-- isomorphism between the two.
--
-- One neat thing is that @'overF' i id == id@.
overF :: f <~> g -> g ~> g -> f ~> f
overF :: forall {k} (f :: k -> *) (g :: k -> *).
(f <~> g) -> (g ~> g) -> f ~> f
overF f <~> g
i g ~> g
f = f <~> g
i g ~> g
f

-- | Reverse an isomorphism.
--
-- @
-- 'viewF'   ('fromF' i) == 'reviewF' i
-- 'reviewF' ('fromF' i) == 'viewF' i
-- @
fromF
    :: forall (f :: Type -> Type) (g :: Type -> Type). ()
    => f <~> g
    -> g <~> f
fromF :: forall (f :: * -> *) (g :: * -> *). (f <~> g) -> g <~> f
fromF f <~> g
i = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF f <~> g
i) (forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF f <~> g
i)