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 _

------------------------------------------------------------
-- "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
  pure :: q (Id q xq) (m (Id p xp))

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

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

-- instance Applicative (->) (,) (->) (,) f => Applicative f where
--   pure a = _
--   (<Type>) f x = _

------------------------------------------------------------
-- 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 ::
              ( 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 = undefined
  -- let distr 
  -- -- distr @(~>) _ _