-- |
-- 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
  , viewF, reviewF, overF
  , fromF
  ) where

import           Control.Natural
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 :: (f ~> g) -> (g ~> f) -> f <~> g
isoF = (f ~> g) -> (g ~> f) -> p (g a) (g a) -> p (f a) (f a)
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap

-- | Use a '<~>' by retrieving the "forward" function:
--
-- @
-- 'viewF'   :: (f <~> g) -> f a -> g a
-- @
viewF :: f <~> g -> f ~> g
viewF :: (f <~> g) -> f ~> g
viewF i :: f <~> g
i = Forget (g x) (f x) (f x) -> f x -> g x
forall r a b. Forget r a b -> a -> r
runForget (Forget (g x) (g x) (g x) -> Forget (g x) (f x) (f x)
f <~> g
i ((g x -> g x) -> Forget (g x) (g x) (g x)
forall r a b. (a -> r) -> Forget r a b
Forget g x -> g x
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 :: (f <~> g) -> g ~> f
reviewF i :: f <~> g
i x :: g x
x = Tagged (f x) (f x) -> f x
forall k (s :: k) b. Tagged s b -> b
unTagged (Tagged (g x) (g x) -> Tagged (f x) (f x)
f <~> g
i (g x -> Tagged (g x) (g x)
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 :: (f <~> g) -> (g ~> g) -> f ~> f
overF i :: f <~> g
i f :: g ~> g
f = (g x -> g x) -> f x -> f x
f <~> g
i g x -> g x
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 :: (f <~> g) -> g <~> f
fromF i :: f <~> g
i = (g ~> f) -> (f ~> g) -> g <~> f
forall k (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF ((f <~> g) -> g ~> f
forall k (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF f <~> g
i) ((f <~> g) -> f ~> g
forall k (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF f <~> g
i)