{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
--------------------------------------------------------------------
-- |
-- Copyright :  (c) Edward Kmett 2014
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
-- @
-- Prof  :: (j -> k -> *) -> (i -> j -> *) -> i -> k -> *
-- ProfR :: (i -> j -> *) -> (i -> k -> *) -> j -> k -> *
-- @
--------------------------------------------------------------------
module Hask.Prof where

import Hask.Core

-- forward profunctor composition forms a weak category.
data Prof :: (j -> k -> *) -> (i -> j -> *) -> i -> k -> * where
  Prof :: p b c -> q a b -> Prof p q a c

instance Category ((~>) :: i -> i -> *) => Semitensor (Prof :: (i -> i -> *) -> (i -> i -> *) -> i -> i -> *) where
  type Tensorable Prof = Profunctor
  second = fmap1
  associate = associateProf

type instance I Prof = (~>)
instance Category ((~>) :: i -> i -> *) => Tensor (Prof :: (i -> i -> *) -> (i -> i -> *) -> i -> i -> *) where
  lambda = lambdaProf
  rho = rhoProf

instance Functor Prof where
  fmap f = nat3 $ \(Prof p q) -> Prof (runNat2 f p) q

instance Functor (Prof p) where
  fmap f = nat2 $ \(Prof p q) -> Prof p (runNat2 f q)

instance Contravariant q => Contravariant (Prof p q) where
  contramap f = Nat $ \(Prof p q) -> Prof p (runNat (contramap f) q)

instance Post Functor p => Functor (Prof p q a) where
  fmap f (Prof p q) = Prof (fmap1 f p) q

instance Functor q => Functor (Prof p q) where
  fmap f = Nat $ \(Prof p q) -> Prof p (runNat (fmap f) q)

instance Post Contravariant p => Contravariant (Prof p q a) where
  contramap f (Prof p q) = Prof (contramap1 f p) q

associateProf :: Iso (Prof (Prof p q) r) (Prof (Prof p' q') r')
                     (Prof p (Prof q r)) (Prof p' (Prof q' r'))
associateProf = dimap
  (nat2 $ \ (Prof (Prof a b) c) -> Prof a (Prof b c))
  (nat2 $ \ (Prof a (Prof b c)) -> Prof (Prof a b) c)

whiskerProfL :: (p ~> q) -> Prof p r ~> Prof q r
whiskerProfL = first

whiskerProfR :: (p ~> q) -> Prof l p ~> Prof l q
whiskerProfR = fmap

lambdaProf :: (Category k, k ~ Hom, Post Functor p) => Iso (Prof k p) (Prof k q) p q
lambdaProf = dimap (nat2 $ \(Prof k p) -> fmap1 k p) (nat2 $ Prof id)

rhoProf :: (Category k, k ~ Hom, Contravariant p) => Iso (Prof p k) (Prof q k) p q
rhoProf = dimap (nat2 $ \(Prof p k) -> lmap k p) (nat2 $ \q -> Prof q id)

newtype ProfR p q a b = ProfR { runProfR :: forall x. p x a -> q x b }

instance Contravariant ProfR where
  contramap f = nat3 $ \(ProfR pq) -> ProfR $ \p -> pq (runNat2 f p)

instance Functor (ProfR p) where
  fmap f = nat2 $ \(ProfR pq) -> ProfR $ \p -> runNat2 f (pq p)

instance Post Functor p => Contravariant (ProfR p q) where
  contramap f = Nat $ \(ProfR pq) -> ProfR $ \p -> pq (fmap1 f p)

instance Post Functor q => Functor (ProfR p q a) where
  fmap f (ProfR pq) = ProfR $ \p -> fmap1 f (pq p)

instance Post Contravariant p => Functor (ProfR p q) where
  fmap f = Nat $ \(ProfR pq) -> ProfR $ \p -> pq (contramap1 f p)

instance Post Contravariant q => Contravariant (ProfR p q a) where
  contramap f (ProfR pq) = ProfR $ \p -> contramap1 f (pq p)

type instance I ProfR = (~>)

iotaProf :: (Category p, p ~ (~>), Contravariant q') => Iso (ProfR p q) (ProfR (~>) q') q q'
iotaProf = dimap (nat2 $ \(ProfR f) -> f id) (nat2 $ \f -> ProfR $ \p -> lmap p f)

jotProf :: Post Functor p => (~>) ~> ProfR p p
jotProf = nat2 $ \f -> ProfR (fmap1 f)

instance Curried Prof ProfR where
  curry k = nat2 $ \p -> ProfR $ \q -> runNat2 k (Prof p q)
  uncurry k = nat2 $ \(Prof p q) -> runProfR (runNat2 k p) q

-- To cocurry Prof we'd have the following universal property:

--newtype ProfL p q a b = ProfL { runProfL :: forall r. (q ~> Prof r p) ~> r a b }
--
--instance Cocurried ProfL Prof where
--  uncocurry l = nat2 $ \k -> runProfL k l
--
--  -- but to cocurry, we'd need to be able to 'smuggle information out' in c.
--  cocurry l = nat2 $ \b -> case runNat2 l (ProfL $ \f -> case runNat2 f b of Prof p q -> _uh) of
--    x -> _wat