module Data.Profunctor.Cofun
( -- * Co-functions
  Cofun(..)
  -- * Mixfix syntax
, type (>-)
, type (-~)
  -- * Construction
, (>-)
  -- * Elimination
, withCofun
, elimCofun
, runCofun
  -- * Computation
, cocurry
, uncocurry
, coap
) where

import Data.Bifunctor.Disjunction
import Data.Functor.Continuation
import Data.Functor.Contravariant
import Data.Profunctor
import Data.Profunctor.Fun.Internal

-- Co-functions

data Cofun r b a = (:>-) { Cofun r b a -> r ! b
coreturn :: r ! b, Cofun r b a -> a
coconst :: a }

infixr 0 :>-

instance Profunctor (Cofun r) where
  dimap :: (a -> b) -> (c -> d) -> Cofun r b c -> Cofun r a d
dimap a -> b
f c -> d
g (r ! b
b :>- c
a) = (a -> b) -> (r ! b) -> r ! a
forall (f :: Type -> Type) a b.
Contravariant f =>
(a -> b) -> f b -> f a
contramap a -> b
f r ! b
b (r ! a) -> d -> Cofun r a d
forall r b a. (r ! b) -> a -> (b >- r) -~ a
>- c -> d
g c
a
  lmap :: (a -> b) -> Cofun r b c -> Cofun r a c
lmap a -> b
f (r ! b
b :>- c
a) = (a -> b) -> (r ! b) -> r ! a
forall (f :: Type -> Type) a b.
Contravariant f =>
(a -> b) -> f b -> f a
contramap a -> b
f r ! b
b (r ! a) -> c -> Cofun r a c
forall r b a. (r ! b) -> a -> (b >- r) -~ a
>- c
a
  rmap :: (b -> c) -> Cofun r a b -> Cofun r a c
rmap b -> c
g (r ! a
b :>- b
a) = r ! a
b (r ! a) -> c -> Cofun r a c
forall r b a. (r ! b) -> a -> (b >- r) -~ a
>- b -> c
g b
a


-- Mixfix syntax

type a >-r = Cofun r a
type r-~ b = r b

infixr 1 >-
infixr 0 -~


-- Construction

(>-) :: (r ! b) -> a -> (b >-r-~ a)
>- :: (r ! b) -> a -> (b >- r) -~ a
(>-) = (r ! b) -> a -> (b >- r) -~ a
forall r b a. (r ! b) -> a -> (b >- r) -~ a
(:>-)


-- Elimination

withCofun :: (b >-r-~ a) -> s ! ((r ! b) -> (s ! a))
withCofun :: ((b >- r) -~ a) -> s ! ((r ! b) -> s ! a)
withCofun (r ! b
b :>- a
a) = (((r ! b) -> s ! a) -> s) -> s ! ((r ! b) -> s ! a)
forall r a. (a -> r) -> r ! a
K (\ (r ! b) -> s ! a
f -> (r ! b) -> s ! a
f r ! b
b (s ! a) -> a -> s
forall r a. (r ! a) -> a -> r
! a
a)

elimCofun :: (b ~~r~> a) -> r ! (a >-r-~ b)
elimCofun :: ((b ~~ r) ~> a) -> r ! ((a >- r) -~ b)
elimCofun (b ~~ r) ~> a
f = (((a >- r) -~ b) -> r) -> r ! ((a >- r) -~ b)
forall r a. (a -> r) -> r ! a
K (\ (r ! a
a :>- b
b) -> (b ~~ r) ~> a
f ((b ~~ r) ~> a) -> (r ! a) -> r ! b
forall r a b. Fun r a b -> (r ! b) -> r ! a
# r ! a
a (r ! b) -> b -> r
forall r a. (r ! a) -> a -> r
! b
b)

runCofun :: (b -> a) -> r ! (a >-r-~ b)
runCofun :: (b -> a) -> r ! ((a >- r) -~ b)
runCofun b -> a
f = (((a >- r) -~ b) -> r) -> r ! ((a >- r) -~ b)
forall r a. (a -> r) -> r ! a
K (\ (r ! a
a :>- b
b) -> r ! a
a (r ! a) -> a -> r
forall r a. (r ! a) -> a -> r
! b -> a
f b
b)


-- Computation

cocurry :: Disj d => (c -> a `d` b) -> (b >-r-~ c) ~~r~> a
cocurry :: (c -> d a b) -> (((b >- r) -~ c) ~~ r) ~> a
cocurry c -> d a b
f = ((r ! a) -> ((b >- r) -~ c) -> r) -> (((b >- r) -~ c) ~~ r) ~> a
forall r b a. ((r ! b) -> a -> r) -> (a ~~ r) ~> b
fun (\ r ! a
k (r ! b
b :>- c
c) -> (r ! a
k (r ! a) -> (r ! b) -> r ! d a b
forall (d :: Type -> Type -> Type) (k :: Type -> Type) a b.
(Disj d, Representable k) =>
k a -> k b -> k (d a b)
<!!> r ! b
b) (r ! d a b) -> d a b -> r
forall r a. (r ! a) -> a -> r
! c -> d a b
f c
c)

uncocurry :: Disj d => ((b >-r-~ c) ~~r~> a) -> (c ~~r~> (a `d` b))
uncocurry :: ((((b >- r) -~ c) ~~ r) ~> a) -> (c ~~ r) ~> d a b
uncocurry (((b >- r) -~ c) ~~ r) ~> a
f = ((r ! d a b) -> c -> r) -> (c ~~ r) ~> d a b
forall r b a. ((r ! b) -> a -> r) -> (a ~~ r) ~> b
fun (\ r ! d a b
k c
c -> (((b >- r) -~ c) ~~ r) ~> a
f ((((b >- r) -~ c) ~~ r) ~> a) -> (r ! a) -> r ! ((b >- r) -~ c)
forall r a b. Fun r a b -> (r ! b) -> r ! a
# (r ! d a b) -> r ! a
forall (k :: Type -> Type) (d :: Type -> Type -> Type) a b.
(Contravariant k, Disj d) =>
k (d a b) -> k a
inlK r ! d a b
k (r ! ((b >- r) -~ c)) -> ((b >- r) -~ c) -> r
forall r a. (r ! a) -> a -> r
! ((r ! d a b) -> r ! b
forall (k :: Type -> Type) (d :: Type -> Type -> Type) a b.
(Contravariant k, Disj d) =>
k (d a b) -> k b
inrK r ! d a b
k (r ! b) -> c -> (b >- r) -~ c
forall r b a. (r ! b) -> a -> (b >- r) -~ a
>- c
c))

coap :: Disj d => c ~~r~> ((b >-r-~ c) `d` b)
coap :: (c ~~ r) ~> d ((b >- r) -~ c) b
coap = ((r ! d ((b >- r) -~ c) b) -> r ! c)
-> (c ~~ r) ~> d ((b >- r) -~ c) b
forall r a b. ((r ! b) -> r ! a) -> Fun r a b
Fun (\ r ! d ((b >- r) -~ c) b
k -> ((r ! d ((b >- r) -~ c) b) -> r ! b
forall (k :: Type -> Type) (d :: Type -> Type -> Type) a b.
(Contravariant k, Disj d) =>
k (d a b) -> k b
inrK r ! d ((b >- r) -~ c) b
k (r ! b) -> c -> (b >- r) -~ c
forall r b a. (r ! b) -> a -> (b >- r) -~ a
>-) (c -> (b >- r) -~ c) -> (r ! ((b >- r) -~ c)) -> r ! c
forall (f :: Type -> Type) a b.
Contravariant f =>
(a -> b) -> f b -> f a
>$< (r ! d ((b >- r) -~ c) b) -> r ! ((b >- r) -~ c)
forall (k :: Type -> Type) (d :: Type -> Type -> Type) a b.
(Contravariant k, Disj d) =>
k (d a b) -> k a
inlK r ! d ((b >- r) -~ c) b
k)