langston-barrett · May 17, 2019 17:34 · May 17, 2019 · May 17, 2019 · May 17, 2019 · May 17, 2019
diff --git a/MoreParameterizedMoreUtils.hs b/MoreParameterizedMoreUtils.hs
@@ -49,7 +49,7 @@ 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.
@@ -117,6 +117,43 @@ instance Bifunctor (Natural (->)) (Natural (->)) Compose 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?"
 
@@ -142,18 +179,40 @@ class ( Monoidal p xp
       ) => 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))
+  unit :: 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))
+  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
-  pure = Prelude.pure
-  ap (fx, fy) = (,) <$> fx <*> fy
+  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))
 
--- instance Applicative (->) (,) (->) (,) f => Applicative f where
---   pure a = _
---   (<Type>) f x = _
+------------------------------------------------------------
+
+-- | 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™
@@ -182,10 +241,16 @@ instance (Foldable t, Traversable (->) (,) t) => Prelude.Traversable t where
 --           => (forall x. f x -> m (g x)) -> t f -> m (t g)
 -- traverseF f ts = _
 
-traverseFC ::
+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 = undefined
-  -- let distr 
-  -- -- distr @(~>) _ _
+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)
diff --git a/MoreParameterizedMoreUtils.hs b/MoreParameterizedMoreUtils.hs
@@ -2,16 +2,18 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE IncoherentInstances #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverlappingInstances #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE Unsafe #-}
 -- instance Traversablef (->) (,) f => Traversable f where
 
 module Data.Parameterized.New where
@@ -22,6 +24,7 @@ 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) =
@@ -58,9 +61,22 @@ instance (Category q) => Category (Natural (q :: l -> l -> Type)) where
   id = id
   (.) = (.)
 
--- | (Forwards) composition of natural transformations
-composeNatural :: Category q => Natural q f g -> Natural q g h -> Natural q f h
-composeNatural (Natural eta) (Natural eps) = Natural (eps . eta)
+-- | (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
@@ -74,10 +90,10 @@ class (Category p, Category q) => Bifunctor p q (xp :: k -> k -> l) where
 instance Bifunctor (->) (->) (,) where
   bimap f g (x, v) = (f x, g v)
 
--- instance (Category q) => Bifunctor (Natural q) (Natural q) Compose where
---   bimap f g = Natural (composeNatural f g)
+instance Bifunctor (Natural (->)) (Natural (->)) Compose where
+  bimap f g = horizontal g f
 
--- data FunDelta (f :: k -> *) (g :: k -> *) a = FunDelta (f a) (g a)
+-- 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
@@ -107,11 +123,19 @@ instance Bifunctor (->) (->) (,) where
 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 (xp k1 k2) k3) (xp k1 (xp k2 k3))
+  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))
+  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
@@ -129,7 +153,7 @@ instance Prelude.Applicative f => Applicative (->) (,) (->) (,) f where
 
 -- instance Applicative (->) (,) (->) (,) f => Applicative f where
 --   pure a = _
---   (<*>) f x = _
+--   (<Type>) f x = _
 
 ------------------------------------------------------------
 -- A terrible idea™

diff --git a/MoreParameterizedMoreUtils.hs b/MoreParameterizedMoreUtils.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -9,12 +11,17 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- instance Traversablef (->) (,) f => Traversable f where
+
 module Data.Parameterized.New where
 
-import Control.Category (Category)
+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.Const
 
 -- | Natural transformations between functors
 newtype (~>) (f :: k -> Type) (g :: k -> Type) =
@@ -23,49 +30,38 @@ newtype (~>) (f :: k -> Type) (g :: k -> Type) =
 ------------------------------------------------------------
 
 -- | 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)
+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) = FunctorOf (~>) (->) m
-type FunctorFC (t :: (k -> Type) -> l -> Type) = FunctorOf (~>) (~>) t
+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 = mapOf (Nat f)
+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 $ mapOf (Nat f)
+fmapFC f = unNat $ fmap (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) =
+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) composition of natural transformations
+composeNatural :: Category q => Natural q f g -> Natural q g h -> Natural q f h
+composeNatural (Natural eta) (Natural eps) = Natural (eps . eta)
+
 ------------------------------------------------------------
 -- An /even more/ categorical definition of bifunctor
 
@@ -75,42 +71,97 @@ class (Category p, Category q) => Bifunctor p q (xp :: k -> k -> l) where
     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 (Category q) => Bifunctor (Natural q) (Natural q) Compose where
+--   bimap f g = Natural (composeNatural f g)
+
+-- data FunDelta (f :: k -> *) (g :: k -> *) 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
-  data family Id p xp :: k
-  assoc :: p (xp (xp k1 k2) k3) (xp k1 (xp k2 x3))
+  type family Id p xp :: k
+  -- | TODO: define and upgrade to an iso?
+  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))
 
 class ( Monoidal p xp
       , Monoidal q xq
-      ) => ApplicativeOf p (xp :: k -> k -> k) q (xq :: l -> l -> l) (m :: k -> l) where
+      ) => 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
-  pureOf :: q (Id q xq) (m (Id p xp))
+  pure :: 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))
+  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 = _
+--   (<*>) f x = _
 
 ------------------------------------------------------------
 -- 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))
+-- 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 @(~>) _ _
diff --git a/MoreParameterizedMoreUtils.hs b/MoreParameterizedMoreUtils.hs
@@ -0,0 +1,116 @@
+{-# 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))