content: {-# LANGUAGE CPP, KindSignatures, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, ConstraintKinds, NoImplicitPrelude, TypeFamilies, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables, DataKinds, DefaultSignatures #-}
  module Hask.Prof 
    ( Prof, ProfunctorOf, Procompose(..)
    ) where
  
  import Hask.Category
  
  type Prof c d = Nat (Op c) (Nat d (->))
  
  class    (Bifunctor f, Dom f ~ Op p, Dom2 f ~ q, Cod2 f ~ (->)) => ProfunctorOf p q f
  instance (Bifunctor f, Dom f ~ Op p, Dom2 f ~ q, Cod2 f ~ (->)) => ProfunctorOf p q f
  
  data Procompose (c :: i -> i -> *) (d :: j -> j -> *) (e :: k -> k -> *)
                  (p :: j -> k -> *) (q :: i -> j -> *) (a :: i) (b :: k) where
    Procompose :: Ob d x => p x b -> q a x -> Procompose c d e p q a b
  
  instance (Category c, Category d, Category e) => Functor (Procompose c d e) where
    type Dom (Procompose c d e) = Prof d e
    type Cod (Procompose c d e) = Nat (Prof c d) (Prof c e)
    fmap = fmap' where
      fmap' :: Prof d e a b -> Nat (Prof c d) (Prof c e) (Procompose c d e a) (Procompose c d e b)
      fmap' (Nat n) = Nat $ Nat $ Nat $ \(Procompose p q) -> Procompose (runNat n p) q
  
  instance (Category c, Category d, Category e, ProfunctorOf d e p) => Functor (Procompose c d e p) where
    type Dom (Procompose c d e p) = Prof c d
    type Cod (Procompose c d e p) = Prof c e
    fmap = fmap' where
      fmap' :: Prof c d a b -> Prof c e (Procompose c d e p a) (Procompose c d e p b)
      fmap' (Nat n) = Nat $ Nat $ \(Procompose p q) -> Procompose p (runNat n q)
  
  instance (Category c, Category d, Category e, ProfunctorOf d e p, ProfunctorOf c d q) => Functor (Procompose c d e p q) where
    type Dom (Procompose c d e p q) = Op c
    type Cod (Procompose c d e p q) = Nat e (->)
    fmap f = case observe f of
      Dict -> Nat $ \(Procompose p q) -> Procompose p (runNat (fmap f) q)
  
  instance (Category c, Category d, Category e, ProfunctorOf d e p, ProfunctorOf c d q, Ob c a) => Functor (Procompose c d e p q a) where
    type Dom (Procompose c d e p q a) = e
    type Cod (Procompose c d e p q a) = (->)
    fmap f (Procompose p q) = Procompose (fmap1 f p) q
  
  -- TODO
  
  {-
  associateProcompose :: Iso (Prof c e) (Prof c e) (->)
    (Procompose c d f (Procompose d e f p q) r) (Procompose c' d' f' (Procompose d' e' f' p' q') r')
    (Procompose c e f p (Procompose c d e q r)) (Procompose c' e' f' p' (Procompose c' d' e' q' r'))
  associateProcompose = dimap
    (Nat $ Nat $ \ (Procompose (Procompose a b) c) -> Procompose a (Procompose b c))
    (Nat $ Nat $ \ (Procompose a (Procompose b c)) -> Procompose (Procompose a b) c)
  -}
  