Some random functions/types related to Lan

[Icelandjack]

Some of these may belong in Data.Functor.Kan.Lan.

From Monads Need Not Be Endofunctors

fold :: (forall xx. (f xx -> a) -> (g x -> lan)) -> (Lan f g a -> lan)
fold a (Lan b c) = a b c
-- as in paper, or
fold' :: Lan f g a -> (forall lan. (forall xx. (f xx -> a) -> (g xx -> lan)) -> lan)
fold' (Lan a b) c = c a b

hoistLan :: (g ~> g') -> (Lan f g ~> Lan f g')
hoistLan tau = fold (\g -> Lan g . tau)

---

The tensor that is defined F ·_J G = Lan J F · G

data Comp :: (k -> Type) -> (k -> Type) -> (k' -> Type) -> (k' -> Type) where
  Comp :: (j xx -> g a) -> (f xx -> Comp j f g a)

foldComp :: (forall xx. (j xx -> g a) -> (f xx -> r)) -> (Comp j f g a -> r)
foldComp f (Comp a b) = f a b

intro2 :: m ~> Comp rel m rel
intro2 = Comp id

elim1 :: Comp rel rel m ~> m
elim1 = foldComp id

disassoc :: Comp rel (Comp rel f g) h ~> Comp rel f (Comp rel g h)
disassoc = foldComp $ \g -> foldComp $ \f -> Comp (Comp g . f) 

is really more useful with some kind of relative monad

class RelMonad m rel where
  royalReturn :: rel ~> m
  relativeBind :: (rel a -> m b) -> (m a -> m b)

unit :: RelMonad m rel => rel ~> m
unit = royalReturn

mult :: RelMonad m rel => Comp rel m m ~> m
mult = foldComp relativeBind