module Data.Profunctor.Fun
( -- * CPS functions
  Fun(..)
  -- ** Mixfix syntax
, type (~~)
, type (~>)
  -- ** Construction
, fun
  -- ** Elimination
, elimFun
) where

import Data.Functor.Continuation
import Data.Profunctor.Cofun
import Data.Profunctor.Fun.Internal

-- Elimination

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