{-# Language DataKinds, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables,
             TypeFamilies, TypeOperators, UndecidableInstances #-}

-- | A /natural transformation/ is a concept from category theory for a mapping between two functors and their objects
-- that preserves a naturality condition. In Haskell the naturality condition boils down to parametricity, so a
-- natural transformation between two functors @f@ and @g@ is represented as
--
-- > type NaturalTransformation f g = ∀a. f a → g a
--
-- This type appears in several Haskell libraries, most obviously in
-- [natural-transformations](https://hackage.haskell.org/package/natural-transformation). There are times, however,
-- when we crave more control. Sometimes what we want to do depends on which type @a@ is hiding in that @f a@ we're
-- given. Sometimes, in other words, we need an /unnatural/ transformation.
--
-- This means we have to abandon parametricity for ad-hoc polymorphism, and that means type classes. There are two
-- steps to defining a transformation:
--
-- * an instance of the base class 'Transformation' declares the two functors being mapped, much like a function type
--   signature,
-- * while the actual mapping of values is performed by an arbitrary number of instances of the method '$', a bit like
--   multiple equation clauses that make up a single function definition.
--
-- The module is meant to be imported qualified, and the importing module will require at least the
-- @FlexibleInstances@, @MultiParamTypeClasses@, and @TypeFamilies@ language extensions to declare the appropriate
-- instances.

module Transformation where

import Data.Coerce (Coercible, coerce)
import qualified Data.Functor.Compose as Functor
import Data.Functor.Const (Const)
import Data.Functor.Product (Product(Pair))
import Data.Functor.Sum (Sum(InL, InR))
import Data.Kind (Type)
import qualified Rank2

import Prelude hiding (($))

-- $setup
-- >>> :seti -XFlexibleInstances -XMultiParamTypeClasses -XTypeFamilies -XTypeOperators
-- >>> import Transformation (Transformation)
-- >>> import qualified Transformation
-- >>> data MaybeToList = MaybeToList
-- >>> instance Transformation MaybeToList where {type Domain MaybeToList = Maybe; type Codomain MaybeToList = []}

-- | A 'Transformation', natural or not, maps one functor to another.
-- For example, here's the declaration for a transformation that maps `Maybe` to `[]`:
--
-- data MaybeToList = MaybeToList
-- instance Transformation MaybeToList where
--    type Domain MaybeToList = Maybe
--    type Codomain MaybeToList = []
class Transformation t where
   type Domain t :: Type -> Type
   type Codomain t :: Type -> Type

-- | Before we can apply a 'Transformation', we also need to declare 'At' which base types it is applicable and how
-- it works. If the transformation is natural, we'll need only one instance declaration.
--
-- >>> :{
-- instance MaybeToList `Transformation.At` a where
--    MaybeToList $ Just x = [x]
--    MaybeToList $ Nothing = []
-- :}
--
-- >>> MaybeToList Transformation.$ (Just True)
-- [True]
--
-- An unnatural 'Transformation' can behave differently depending on the base type and even on its value.
--
-- >>> :{
-- instance {-# OVERLAPS #-} MaybeToList `At` Char where
--    MaybeToList $ Just '\0' = []
--    MaybeToList $ Just c = [c]
--    MaybeToList $ Nothing = []
-- :}
class Transformation t => At t x where
   -- | Apply the transformation @t@ at type @x@ to map 'Domain' to the 'Codomain' functor.
   ($) :: t -> Domain t x -> Codomain t x
   infixr 0 $

-- | Alphabetical synonym for '$'
apply :: t `At` x => t -> Domain t x -> Codomain t x
apply :: forall t x. At t x => t -> Domain t x -> Codomain t x
apply = t -> Domain t x -> Codomain t x
forall t x. At t x => t -> Domain t x -> Codomain t x
($)

-- | Transformation that coerces a @p x@ to @q x@
data Coercion (p :: Type -> Type) (q :: Type -> Type) = Coercion

-- | Composition of two transformations
data Compose t u = Compose t u

-- | Transformation under a 'Data.Functor.Functor'
newtype Mapped (f :: Type -> Type) t = Mapped t

-- | Transformation under a 'Foldable'
newtype Folded (f :: Type -> Type) t = Folded t

-- | Transformation under a 'Traversable'
newtype Traversed (f :: Type -> Type) t = Traversed t

instance Transformation (Coercion p q) where
   type Domain (Coercion p q) = p
   type Codomain (Coercion p q) = q

instance (Transformation t, Transformation u, Domain t ~ Codomain u) => Transformation (Compose t u) where
   type Domain (Compose t u) = Domain u
   type Codomain (Compose t u) = Codomain t

instance Transformation t => Transformation (Mapped f t) where
   type Domain (Mapped f t) = Functor.Compose f (Domain t)
   type Codomain (Mapped f t) = Functor.Compose f (Codomain t)

instance Transformation t => Transformation (Folded f t) where
   type Domain (Folded f t) = Functor.Compose f (Domain t)
   type Codomain (Folded f t) = Codomain t

instance (Transformation t, Codomain t ~ Functor.Compose m n) => Transformation (Traversed f t) where
   type Domain (Traversed f t) = Functor.Compose f (Domain t)
   type Codomain (Traversed f t) =
      Functor.Compose (ComposeOuter (Codomain t)) (Functor.Compose f (ComposeInner (Codomain t)))

instance Coercible (p x) (q x) => Coercion p q `At` x where
   Coercion p q
Coercion $ :: Coercion p q
-> Domain (Coercion p q) x -> Codomain (Coercion p q) x
$ Domain (Coercion p q) x
x = p x -> q x
forall a b. Coercible a b => a -> b
coerce p x
Domain (Coercion p q) x
x

type family ComposeOuter (c :: Type -> Type) :: Type -> Type where
   ComposeOuter (Functor.Compose p q) = p

type family ComposeInner (c :: Type -> Type) :: Type -> Type where
   ComposeInner (Functor.Compose p q) = q

instance (t `At` x, u `At` x, Domain t ~ Codomain u) => Compose t u `At` x where
   Compose t
t u
u $ :: Compose t u -> Domain (Compose t u) x -> Codomain (Compose t u) x
$ Domain (Compose t u) x
x =  t
t t -> Domain t x -> Codomain t x
forall t x. At t x => t -> Domain t x -> Codomain t x
$ u
u u -> Domain u x -> Codomain u x
forall t x. At t x => t -> Domain t x -> Codomain t x
$ Domain u x
Domain (Compose t u) x
x

instance (t `At` x, Functor f) => Mapped f t `At` x where
   Mapped t
t $ :: Mapped f t -> Domain (Mapped f t) x -> Codomain (Mapped f t) x
$ Functor.Compose f (Domain t x)
x = f (Codomain t x) -> Compose f (Codomain t) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Functor.Compose ((t
t t -> Domain t x -> Codomain t x
forall t x. At t x => t -> Domain t x -> Codomain t x
$) (Domain t x -> Codomain t x) -> f (Domain t x) -> f (Codomain t x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Domain t x)
x)

instance (t `At` x, Foldable f, Codomain t ~ Const m, Monoid m) => Folded f t `At` x where
   Folded t
t $ :: Folded f t -> Domain (Folded f t) x -> Codomain (Folded f t) x
$ Functor.Compose f (Domain t x)
x = (Domain t x -> Const m x) -> f (Domain t x) -> Const m x
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (t
t t -> Domain t x -> Codomain t x
forall t x. At t x => t -> Domain t x -> Codomain t x
$) f (Domain t x)
x

instance (t `At` x, Traversable f, Codomain t ~ Functor.Compose m n, Applicative m) => Traversed f t `At` x where
   Traversed t
t $ :: Traversed f t
-> Domain (Traversed f t) x -> Codomain (Traversed f t) x
$ Functor.Compose f (Domain t x)
x = m (Compose f n x) -> Compose m (Compose f n) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Functor.Compose (f (n x) -> Compose f n x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Functor.Compose (f (n x) -> Compose f n x) -> m (f (n x)) -> m (Compose f n x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Domain t x -> m (n x)) -> f (Domain t x) -> m (f (n x))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse (Compose m n x -> m (n x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
Functor.getCompose (Compose m n x -> m (n x))
-> (Domain t x -> Compose m n x) -> Domain t x -> m (n x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t
t t -> Domain t x -> Codomain t x
forall t x. At t x => t -> Domain t x -> Codomain t x
$)) f (Domain t x)
x)

instance Transformation (Rank2.Arrow (p :: Type -> Type) q x) where
   type Domain (Rank2.Arrow p q x) = p
   type Codomain (Rank2.Arrow p q x) = q

instance Rank2.Arrow p q x `At` x where
   $ :: Arrow p q x -> Domain (Arrow p q x) x -> Codomain (Arrow p q x) x
($) = Arrow p q x -> p x -> q x
Arrow p q x -> Domain (Arrow p q x) x -> Codomain (Arrow p q x) x
forall {k} (p :: k -> *) (q :: k -> *) (a :: k).
Arrow p q a -> p a -> q a
Rank2.apply

instance (Transformation t1, Transformation t2, Domain t1 ~ Domain t2) => Transformation (t1, t2) where
   type Domain (t1, t2) = Domain t1
   type Codomain (t1, t2) = Product (Codomain t1) (Codomain t2)

instance (t `At` x, u `At` x, Domain t ~ Domain u) => (t, u) `At` x where
   (t
t, u
u) $ :: (t, u) -> Domain (t, u) x -> Codomain (t, u) x
$ Domain (t, u) x
x = Codomain t x -> Codomain u x -> Product (Codomain t) (Codomain u) x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (t
t t -> Domain t x -> Codomain t x
forall t x. At t x => t -> Domain t x -> Codomain t x
$ Domain t x
Domain (t, u) x
x) (u
u u -> Domain u x -> Codomain u x
forall t x. At t x => t -> Domain t x -> Codomain t x
$ Domain u x
Domain (t, u) x
x)

instance (Transformation t1, Transformation t2, Domain t1 ~ Domain t2) => Transformation (Either t1 t2) where
   type Domain (Either t1 t2) = Domain t1
   type Codomain (Either t1 t2) = Sum (Codomain t1) (Codomain t2)

instance (t `At` x, u `At` x, Domain t ~ Domain u) => Either t u `At` x where
   Left t
t $ :: Either t u -> Domain (Either t u) x -> Codomain (Either t u) x
$ Domain (Either t u) x
x = Codomain t x -> Sum (Codomain t) (Codomain u) x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (t
t t -> Domain t x -> Codomain t x
forall t x. At t x => t -> Domain t x -> Codomain t x
$ Domain t x
Domain (Either t u) x
x)
   Right u
t $ Domain (Either t u) x
x = Codomain u x -> Sum (Codomain t) (Codomain u) x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (u
t u -> Domain u x -> Codomain u x
forall t x. At t x => t -> Domain t x -> Codomain t x
$ Domain u x
Domain (Either t u) x
x)