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

module Transformation where

import qualified Data.Functor as Rank1
import Data.Functor.Product (Product(Pair))
import Data.Functor.Sum (Sum(InL, InR))
import Data.Kind (Type)
import Data.Monoid (Ap)
import Data.Semigroup (Semigroup((<>)))
import qualified Rank2

import Prelude hiding (($))

-- | A 'Transformation', natural or not, maps one functor to another.
class Transformation t where
   type Domain t :: Type -> Type
   type Codomain t :: Type -> Type

-- | An unnatural 'Transformation' can behave differently at different points.
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 :: 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
($)

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

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 (t `At` x, u `At` x, Domain t ~ Codomain u) => Compose t u `At` x where
   Compose t :: t
t u :: u
u $ :: Compose t u -> Domain (Compose t u) x -> Codomain (Compose t u) x
$ 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 Transformation (Rank2.Arrow p 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 -> 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
t, u :: u
u) $ :: (t, u) -> Domain (t, u) x -> Codomain (t, u) x
$ 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
t $ :: Either t u -> Domain (Either t u) x -> Codomain (Either t u) x
$ 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 t :: u
t $ x :: 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)