Polys.idr

module Polys

import Control.Monad.Identity
import Data.Morphisms

data ProductMeh: (Type -> Type) -> (Type -> Type) -> Type -> Type where
  Prod: (f a, g a) -> ProductMeh f g a

data NaturalTransformation : (Type -> Type) -> (Type -> Type) -> Type where
  NT : (f a -> g a) -> NaturalTransformation f g

data TATransformation :  (((Type -> Type -> Type) -> Type) -> Type) ->  (((Type -> Type -> Type) -> Type) -> Type) -> Type where
  TA: {a: (Type -> Type -> Type) -> Type} -> f a -> g a -> TATransformation f g

data BinaturalTransformation : (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type where
  Bor : (f a b -> g a b) -> BinaturalTransformation f g

interface PSemigroup (m: k) (ff: k -> k -> Type) (xx: k) where
  μ: xx `ff` m

interface PSemigroup m ff xx => PMonoid (m: k) (ff: k -> k -> Type) (xx: k) (i: k) where
  η: i `ff` m

interface Endofunctor (f: k -> k) (ff: k -> k -> Type) where
  map: a `ff` b -> f a `ff` f b

-- interface Endofunctor f ff => Traverse (f: k -> k) (ff: k -> k -> Type) where
--   traverse: Applicative m => a `ff` m b -> f a `ff` m (f b)

-- Traversable t   = Traverse t (->)
-- Bitraversable t = Traverse t (forall (a, b) (g a b -> h a b))
-- TATraversable t = Traverse (((Type -> Type -> Type) -> Type) -> Type) t

Functor: (Type -> Type) -> Type
Functor f   = Endofunctor f Morphism

FunctorK: ((Type -> Type) -> Type -> Type) -> Type
FunctorK f  = Endofunctor f NaturalTransformation

-- This is a pretty nonsensical name for this. It’s really a functor in the category of bifunctors … maybe?
BifunctorK: ((Type -> Type -> Type) -> (Type -> Type -> Type)) -> Type
BifunctorK f = Endofunctor f BinaturalTransformation

TAFunctor: ((((Type -> Type -> Type) -> Type) -> Type) -> ((Type -> Type -> Type) -> Type) -> Type) -> Type
TAFunctor f = Endofunctor f TATransformation

Semigroup1: Type -> Type
Semigroup1 a = PSemigroup a Morphism (a, a)
Monoid1: Type -> Type
Monoid1 a    = PMonoid a Morphism (a, a) ()

Bind: (Type -> Type) -> Type
Bind m = PSemigroup m NaturalTransformation (m . m)
Monad: (Type -> Type) -> Type
Monad m = PMonoid m NaturalTransformation (m . m) Identity

SemigroupK: (Type -> Type) -> Type
SemigroupK m = PSemigroup m NaturalTransformation (ProductMeh m m)
MonoidK: (Type -> Type) -> Type
MonoidK m    = PMonoid m NaturalTransformation (ProductMeh m m) Identity

-- MonadK: ((Type -> Type) -> Type -> Type) -> Type
-- MonadK m = PMonoid   ((Type -> Type) -> Type -> Type) m (m . m) Id

-- Problems with poly-kinded type classes so far
-- • how to have Monad extend Functor when Monad is just a specialization of
--   Monoid (and other similar things)
-- • how to specify the types for poly-kinded Traverse