MoreParameterizedMoreUtils.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Unsafe #-}
-- instance Traversablef (->) (,) f => Traversable f where

module Data.Parameterized.New where

import Prelude hiding (Functor(..), Applicative(..), Traversable(..), id, (.))
import Prelude ((<*>))
import qualified Prelude (Functor(..), Applicative(..), Traversable(..), (.))
import Control.Category (Category(..))
import Data.Kind (Type)
import Data.Functor.Compose
import Data.Functor.Identity

-- | Natural transformations between functors
newtype (~>) (f :: k -> Type) (g :: k -> Type) =
  Nat { unNat :: forall x. f x -> g x }

------------------------------------------------------------

-- | Think of @p@ as Hom in the domain category and @q@ as Hom in the codomain
class (Category p, Category q) => Functor (p :: k -> k -> Type) (q :: l -> l -> Type) (f :: k -> l) where
  fmap :: p a b -> q (f a) (f b)

-- | These are /exactly/ functors.
instance Prelude.Functor f => Functor (->) (->) f where fmap = Prelude.fmap
instance Functor (->) (->) f => Prelude.Functor f where fmap = fmap

type FunctorF (m :: (k -> Type) -> Type) = Functor (~>) (->) m
type FunctorFC (t :: (k -> Type) -> l -> Type) = Functor (~>) (~>) t

fmapF :: FunctorF m => (forall x. f x -> g x) -> m f -> m g
fmapF f = fmap (Nat f)

fmapFC :: FunctorFC t
       => forall f g. (forall x. f x -> g x) -> (forall x. t f x -> t g x)
fmapFC f = unNat $ fmap (Nat f)

------------------------------------------------------------

-- | Natural transformations between functors, take 2.
newtype Natural (q :: l -> l -> Type) (f :: k -> l) (g :: k -> l) =
  Natural { unNatural :: forall x. q (f x) (g x) }

-- | Functor categories
instance (Category q) => Category (Natural (q :: l -> l -> Type)) where
  id = id
  (.) = (.)

-- | (Forwards, vertical) composition of natural transformations
vertical :: Category q => Natural q f g -> Natural q g h -> Natural q f h
vertical (Natural eta) (Natural eps) = Natural (eps . eta)

-- | (Forwards, vertical) composition of natural transformations
--
-- Codomain 'Type' because of 'Compose'
horizontal :: forall q (f :: k -> l) g (h :: l -> Type) j.
              ( Category q
              , Functor q (->) h
              )
           => Natural q f g
           -> Natural (->) h j
           -> Natural (->) (Compose h f) (Compose j g)
horizontal (Natural eta) (Natural eps) =
  Natural (\(Compose foo) -> Compose (eps (fmap eta foo)))

------------------------------------------------------------
-- An /even more/ categorical definition of bifunctor

class (Category p, Category q) => Bifunctor p q (xp :: k -> k -> l) where
  bimap ::
    p x y ->            -- x --> y in p
    p v w ->            -- v --> w in p
    q (xp x v) (xp y w) -- (x ⊗ v) --> (y ⊗ w) in q

instance Bifunctor (->) (->) (,) where
  bimap f g (x, v) = (f x, g v)

instance Bifunctor (Natural (->)) (Natural (->)) Compose where
  bimap f g = horizontal g f

-- data FunDelta (f :: k -> Type) (g :: k -> Type) a = FunDelta (f a) (g a)

-- proj1 :: (Category p) p (FunDelta f g a) (f a)
-- proj1 (FunDelta fa _) = fa

-- proj2 :: FunDelta f g a -> g a
-- proj2 (FunDelta _ ga) = ga

-- univFunDelta1 :: Category p => p b (FunDelta f g a) -> (p b (f a), p b (g a))
-- univFunDelta1 both = (_, _)

-- univFunDelta2 :: Category p => p b (f a) -> p b (g a) -> p b (FunDelta f g a)
-- univFunDelta2 (fst, snd) = _

-- -- | Warm up...
-- instance (Category q) => Bifunctor (Natural (->)) (Natural (->)) FunDelta where
--   bimap (Natural eta) (Natural eps) =
--     Natural (\(FunDelta x v) -> FunDelta (eta x) (eps v))

-- -- | The real...
-- instance (Category q) => Bifunctor (Natural q) (Natural q) FunDelta where
--   bimap (Natural eta) (Natural eps) =
--     Natural _

------------------------------------------------------------

-- Control.Category.Dual
newtype Op p a b = Op { unOp :: p b a }

instance (Category p) => Category (Op p) where
  id = Op id
  Op f . Op g = Op (g . f)

------------------------------------------------------------

-- newtype CatProd p q a b = CatProd (p a b, q a b)

-- class (Category p, Category q) => CatProd p q where

-- | Specialized case avoiding the need for @Op@ and product categories
class (Category p) => Profunctor p (f :: k -> k -> Type) where
  -- | The last @->@ here should be thought of as the @Hom@ in 'Type'.
  dimap :: p a b -> p c d -> f b c -> f a d

class (Monoidal p xp, Profunctor p homp) => Closed p xp homp where
  curry :: p (xp a b) c -> p a (homp b c)
  uncurry :: p a (homp b c) -> p (xp a b) c

class (Closed p xp homp) => CCC p xp homp where
  eval :: p (xp (homp a b) a) b

instance Profunctor (->) (->) where
  dimap ab cd bc = cd . bc . ab

instance Closed (->) (,) (->) where
  curry = Prelude.curry
  uncurry = Prelude.uncurry

instance CCC (->) (,) (->) where
  eval (f, a) = f a

------------------------------------------------------------
-- "An applicative is just a lax monoidal functor, what's the problem?"

class (Category p, Bifunctor p p xp) => Monoidal p xp where
  type family Id p xp :: k
  -- | TODO: define and upgrade to an iso?
  assoc :: p (xp k1 (xp k2 k3)) (xp (xp k1 k2) k3)
  -- assoc :: p (xp (xp k1 k2) k3) (xp k1 (xp k2 k3))

instance Monoidal (->) (,) where
  type instance Id (->) (,) = ()
  -- assoc ((x, y), z) = (x, (y, z))
  assoc (x, (y, z)) = ((x, y), z)

-- | The ol' monoidal category of endofunctors... whence monads are monoids
instance Monoidal (Natural (->)) Compose where
  type instance Id (Natural (->)) Compose = Identity
  assoc = Natural $ \(Compose fg) ->
    Compose (Compose (fmap getCompose fg))

class ( Monoidal p xp
      , Monoidal q xq
      ) => Applicative p (xp :: k -> k -> k) q (xq :: l -> l -> l) (m :: k -> l) where

  -- | Arrow from the monoidal identity in q to f applied to the identity in p
  unit :: q (Id q xq) (m (Id p xp))

  -- | This should be natural in @x@ and @y@.
  prod :: forall (x :: k) (y :: k). q (xq (m x) (m y)) (m (xp x y))

-- (<*>) :: (CCC p xp homp) => _
-- ff <*> fa = _

instance Prelude.Applicative f => Applicative (->) (,) (->) (,) f where
  unit = Prelude.pure
  prod (fx, fy) = (,) <$> fx <*> fy

-- | See https://bit.ly/2Wb1lco
instance Applicative (->) (,) (->) (,) f => Prelude.Applicative f where
  pure a = fmap (const a) (unit @(->) @(,) @(->) @(,) ())
  (<*>) ff fa =
    (fmap :: (a -> b) -> (f a -> f b))
      (eval :: (a -> b, a) -> b)
      ((prod @(->) @(,) :: (f a, f b) -> f (a, b))
        (ff, fa))

------------------------------------------------------------

-- | Functor category with postcomposition by a given functor
newtype Postcompose q m a b =
  Postcompose { unPostcompose :: Natural q a (Compose m b) }

-- Applicative p (xp :: k -> k -> k) q (xq :: l -> l -> l) (m :: k -> l) where
instance ( Monoidal p xp
         , Monoidal q xq
         , Profunctor q q -- Require that Hom is actually a profunctor
         , Applicative p xp q xq m) => (Category (Postcompose q m)) where
  -- | TODO: need generalization of pure?
  id = Postcompose (Natural _)

------------------------------------------------------------
-- A terrible idea™

-- An traversable (endo)functor is
-- + A functor G : Set -> Set
-- + With a distributive law (natural transformation) distr : G⋅F ⇒ F⋅G
--   for applicative functors F

class ( Functor p p t
      , Monoidal p xp
      ) => Traversable (p :: k -> k -> Type) xp (t :: k -> k) where
  -- We would like this to be: @Natural p (Compose t m) (Compose m t)@
  -- But Compose is limited to things wit codomain 'Type'.
  distr :: (Applicative p xp p xp m)
        => forall x. p (t (m x)) (m (t x))

instance (Foldable t, Traversable (->) (,) t) => Prelude.Traversable t where
  traverse :: Prelude.Applicative f => (a -> f b) -> t a -> f (t b)
  traverse f ts = distr @(->) @(,) (Prelude.fmap f ts)

-- type TraversableF = Traversable p xp t

-- | This is ill-kinded :'(
-- traverseF :: (Traversable (->) (,) t, Prelude.Applicative m)
--           => (forall x. f x -> m (g x)) -> t f -> m (t g)
-- traverseF f ts = _

traverseFC :: forall f g m p xp t.
              ( Traversable p xp t
              , Prelude.Applicative m)
           => (forall x. f x -> m (g x)) -> (forall x. t f x -> m (t g x))
traverseFC f ts = _
  -- "p" in fmap needs to be (p a b := Natural f (Compose m g))
  -- "q" in fmap needs to be (q a b := Natural (t f) (Compose m (t g)))
  -- let foo :: ()
  --     foo = fmap @p @xp f ts
  -- in _


  -- fmap :: p a b -> q (f a) (f b)