TT.hs

{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Schemes.TT where

import Pandora.Core.Functor (type (:.), type (>), type (>>>), type (~>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (<~), (<~~~), (<~~~~), (=#-)))
import Pandora.Pattern.Betwixt (Betwixt)
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category (identity, (<--), (<---), (<----), (<-----))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--), (<-|---), (<-|-|-)))
import Pandora.Pattern.Functor.Contravariant (Contravariant)
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)), (<-/-/-))
import Pandora.Pattern.Functor.Distributive (Distributive ((-<<)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\)))
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.Sum ((:+:), bitraverse_sum)
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.Algebraic (empty, point, extract, (<-||-), (<-||---))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))

newtype TT ct ct' t t' a = TT (t :. t' >>> a)

infixr 6 <::>, >::>, <::<, >::<

type (<::>) = TT Covariant Covariant
type (>::>) = TT Contravariant Covariant
type (<::<) = TT Covariant Contravariant
type (>::<) = TT Contravariant Contravariant

instance Interpreted (->) (TT ct ct' t t') where
	type Primary (TT ct ct' t t') a = t :. t' >>> a
	run ~(TT x) = x
	unite = TT

instance (Semigroupoid m, Covariant m m t, Covariant (Betwixt m m) m t, Covariant m (Betwixt m m) t', Interpreted m (t <::> t')) => Covariant m m (t <::> t') where
	(<-|-) f = (=#-) ((<-|-|-) f)

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) t') => Semimonoidal (-->) (:*:) (:*:) (t <::> t') where
	mult = Straight <-- TT . (<-|-) (mult @(-->) <~) . (mult @(-->) <~) . (run <-||-) . (run @(->) <-|-)

instance (Covariant (->) (->) t, Covariant (->) (->) t', Semimonoidal (-->) (:*:) (:*:) t', Monoidal (-->) (-->) (:*:) (:*:) t, Monoidal (-->) (-->) (:*:) (:*:) t') => Monoidal (-->) (-->) (:*:) (:*:) (t <::> t') where
	unit _ = Straight <-- TT . point . point . (<~ One)

instance (Covariant (->) (->) t, Covariant (->) (->) t', Semimonoidal (-->) (:*:) (:+:) t) => Semimonoidal (-->) (:*:) (:+:) (t <::> t') where
	mult = Straight <-- \(TT x :*: TT y) -> TT
		<----- bitraverse_sum identity identity
			<-|-- mult @(-->) @(:*:) @(:+:)
				<~~~ x :*: y

instance (Covariant (->) (->) t, Covariant (->) (->) t', Semimonoidal (-->) (:*:) (:+:) t, Monoidal (-->) (-->) (:*:) (:+:) t) => Monoidal (-->) (-->) (:*:) (:+:) (t <::> t') where
	unit _ = Straight <-- \_ -> TT empty

instance (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t, Semimonoidal (<--) (:*:) (:*:) t') => Semimonoidal (<--) (:*:) (:*:) (t <::> t') where
	mult = Flip <-- \(TT xys) -> TT <-||--- TT <-|--- mult @(<--) <~~~~ (mult @(<--) <~) <-|- xys

instance (Covariant (->) (->) t, Monoidal (<--) (-->) (:*:) (:*:) t, Monoidal (<--) (-->) (:*:) (:*:) t') => Monoidal (<--) (-->) (:*:) (:*:) (t <::> t') where
	unit _ = Flip <-- \(TT x) -> Straight <---- constant <--- extract <-- extract x

instance (Traversable (->) (->) t, Traversable (->) (->) t') => Traversable (->) (->) (t <::> t') where
	f <-/- x = TT <-|-- (f <-/-/- run x)

instance (Bindable (->) t, Distributive (->) (->) t, Covariant (->) (->) t', Bindable (->) t') => Bindable (->) (t <::> t') where
	f =<< TT x = TT <--- (\i -> (identity =<<) <-|- run . f -<< i) =<< x

instance Monoidal (-->) (-->) (:*:) (:*:) t => Liftable (->) (TT Covariant Covariant t) where
	lift :: Covariant (->) (->) t' => t' ~> t <::> t'
	lift = TT . point

instance Monoidal (<--) (-->) (:*:) (:*:) t => Lowerable (->) (TT Covariant Covariant t) where
	lower :: t <::> t' ~> t'
	lower (TT x) = extract x

instance Covariant (->) (->) t => Hoistable (->) (TT Covariant Covariant t) where
	(/|\) :: t' ~> v -> (t <::> t' ~> t <::> v)
	f /|\ TT x = TT <---- f <-|- x