MoreParameterizedMoreUtils.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Parameterized.New where

import Control.Category (Category)
import Data.Kind (Type)
import Data.Functor.Compose
import Data.Functor.Const

-- | 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) => FunctorOf (p :: k -> k -> Type) (q :: l -> l -> Type) (f :: k -> l) where
  mapOf :: p a b -> q (f a) (f b)

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

fmapF :: FunctorF m => (forall x. f x -> g x) -> m f -> m g
fmapF f = mapOf (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 $ mapOf (Nat f)
  
------------------------------------------------------------

newtype App m tg = App { unApp :: m tg }

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

class TraversableOf (c :: (* -> *) -> k -> k) (q :: k -> k -> Type) (t :: (j -> *) -> k) where
  traverseOf :: forall (f :: j -> *) (g :: j -> *) (m :: Type -> Type). Applicative m
             => (f ~> (Compose m g)) -> q (t f) (c m (t g))

type TraversableF = TraversableOf App (->)
type TraversableFC = TraversableOf Compose (~>)

traverseF :: (TraversableF t, Applicative m)
          => (forall x. f x -> m (g x)) -> t f -> m (t g)
traverseF f ts = unApp $ traverseOf (Nat (Compose . f)) ts

traverseFC :: (TraversableFC t, Applicative m)
           => (forall x. f x -> m (g x)) -> (forall x. t f x -> m (t g x))
traverseFC f = getCompose . unNat (traverseOf (Nat (Compose . f)))

-- That wasn't very good. What's that 'c' thing? What are the semantics?
-- Let's try again...

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

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

------------------------------------------------------------
-- 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

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

class (Category p, Bifunctor p p xp) => Monoidal p xp where
  data family Id p xp :: k
  assoc :: p (xp (xp k1 k2) k3) (xp k1 (xp k2 x3))

class ( Monoidal p xp
      , Monoidal q xq
      ) => ApplicativeOf 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
  pureOf :: q (Id q xq) (m (Id p xp))

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

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

class TraversableOff (t :: (k -> *) -> l -> *) where
  -- traverseF  :: Applicative m => (forall x. f x -> m (g x)) -> t f -> m (t g)
  -- traverseFC :: Applicative m => (forall x. f x -> m (g x)) -> (forall x. t f x -> m (t g x))
  traversableOff :: forall p xp q xq r (f :: k -> *) (g :: k -> *) (m :: * -> *).
                    ( Category q
                    , ApplicativeOf p xp q xq m
                    )
                 => Natural q f (Compose m g)
                 -> Natural r (t f) (Compose m (t g))

type family Ignore (t :: (k -> *) -> *) (f :: k -> *) :: l -> *
type instance Ignore (t :: (k -> *) -> *) f = Const (t f)

-- traverseFOff  :: ( Applicative m
--                  , TraversableOff (Ignore t)
--                  ) => (forall x. f x -> m (g x)) -> t f -> m (t g)
-- traverseFOff f ts = _

-- traverseFC :: Applicative m => (forall x. f x -> m (g x)) -> (forall x. t f x -> m (t g x))