{-# LANGUAGE FunctionalDependencies #-}
module Data.Functor.Contravariant.Applicative
( -- * Contravariant applicative functors
  Contrapply(..)
, Contrapplicative(..)
) where

import Data.Functor.Continuation
import Data.Functor.Contravariant
import Data.Functor.Contravariant.CPS
import Data.Profunctor.Cofun
import Data.Profunctor.Fun

-- Contravariant applicative functors

class ContravariantCPS r k => Contrapply r k | k -> r where
  {-# MINIMAL coliftC2 | (<&>) #-}

  coliftC2 :: ((b >-r-~ c) ~~r~> a) -> k a -> k b -> k c
  coliftC2 (((b >- r) -~ c) ~~ r) ~> a
f k a
a k b
b = (((b >- r) -~ c) ~~ r) ~> a
f ((((b >- r) -~ c) ~~ r) ~> a) -> k a -> k ((b >- r) -~ c)
forall r (k :: Type -> Type) a' a.
ContravariantCPS r k =>
((a' ~~ r) ~> a) -> k a -> k a'
<#> k a
a k ((b >- r) -~ c) -> k b -> k c
forall r (k :: Type -> Type) a b.
Contrapply r k =>
k ((a >- r) -~ b) -> k a -> k b
<&> k b
b

  (<&>) :: k (a >-r-~ b) -> k a -> k b
  (<&>) = ((((a >- r) -~ b) ~~ r) ~> ((a >- r) -~ b))
-> k ((a >- r) -~ b) -> k a -> k b
forall r (k :: Type -> Type) b c a.
Contrapply r k =>
((((b >- r) -~ c) ~~ r) ~> a) -> k a -> k b -> k c
coliftC2 (((r ! ((a >- r) -~ b)) -> ((a >- r) -~ b) -> r)
-> (((a >- r) -~ b) ~~ r) ~> ((a >- r) -~ b)
forall r b a. ((r ! b) -> a -> r) -> (a ~~ r) ~> b
fun (!))

  infixl 3 <&>

instance Contrapply r ((!) r) where
  r ! ((a >- r) -~ b)
f <&> :: (r ! ((a >- r) -~ b)) -> (r ! a) -> r ! b
<&> r ! a
a = (b -> r) -> r ! b
forall r a. (a -> r) -> r ! a
K (\ b
b -> r ! ((a >- r) -~ b)
f (r ! ((a >- r) -~ b)) -> ((a >- r) -~ b) -> r
forall r a. (r ! a) -> a -> r
! (r ! a
a (r ! a) -> b -> (a >- r) -~ b
forall r b a. (r ! b) -> a -> (b >- r) -~ a
>- b
b))

instance Contrapply Bool Predicate where
  Predicate ((a >- Bool) -~ b) -> Bool
f <&> :: Predicate ((a >- Bool) -~ b) -> Predicate a -> Predicate b
<&> Predicate a -> Bool
a = (b -> Bool) -> Predicate b
forall a. (a -> Bool) -> Predicate a
Predicate (\ b
b -> ((a >- Bool) -~ b) -> Bool
f ((a -> Bool) -> Bool ! a
forall r a. (a -> r) -> r ! a
K a -> Bool
a (Bool ! a) -> b -> (a >- Bool) -~ b
forall r b a. (r ! b) -> a -> (b >- r) -~ a
>- b
b))

instance Contrapply r (Op r) where
  Op ((a >- r) -~ b) -> r
f <&> :: Op r ((a >- r) -~ b) -> Op r a -> Op r b
<&> Op a -> r
a = (b -> r) -> Op r b
forall a b. (b -> a) -> Op a b
Op (\ b
b -> ((a >- r) -~ b) -> r
f ((a -> r) -> r ! a
forall r a. (a -> r) -> r ! a
K a -> r
a (r ! a) -> b -> (a >- r) -~ b
forall r b a. (r ! b) -> a -> (b >- r) -~ a
>- b
b))


class Contrapply r k => Contrapplicative r k | k -> r where
  copure :: (b -> a) -> k (a >-r-~ b)

instance Contrapplicative r ((!) r) where
  copure :: (b -> a) -> r ! ((a >- r) -~ b)
copure = (b -> a) -> r ! ((a >- r) -~ b)
forall b a r. (b -> a) -> r ! ((a >- r) -~ b)
runCofun

instance Contrapplicative Bool Predicate where
  copure :: (b -> a) -> Predicate ((a >- Bool) -~ b)
copure = (((a >- Bool) -~ b) -> Bool) -> Predicate ((a >- Bool) -~ b)
forall a. (a -> Bool) -> Predicate a
Predicate ((((a >- Bool) -~ b) -> Bool) -> Predicate ((a >- Bool) -~ b))
-> ((b -> a) -> ((a >- Bool) -~ b) -> Bool)
-> (b -> a)
-> Predicate ((a >- Bool) -~ b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (!) ((Bool ! ((a >- Bool) -~ b)) -> ((a >- Bool) -~ b) -> Bool)
-> ((b -> a) -> Bool ! ((a >- Bool) -~ b))
-> (b -> a)
-> ((a >- Bool) -~ b)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> a) -> Bool ! ((a >- Bool) -~ b)
forall b a r. (b -> a) -> r ! ((a >- r) -~ b)
runCofun

instance Contrapplicative r (Op r) where
  copure :: (b -> a) -> Op r ((a >- r) -~ b)
copure = (((a >- r) -~ b) -> r) -> Op r ((a >- r) -~ b)
forall a b. (b -> a) -> Op a b
Op ((((a >- r) -~ b) -> r) -> Op r ((a >- r) -~ b))
-> ((b -> a) -> ((a >- r) -~ b) -> r)
-> (b -> a)
-> Op r ((a >- r) -~ b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (!) ((r ! ((a >- r) -~ b)) -> ((a >- r) -~ b) -> r)
-> ((b -> a) -> r ! ((a >- r) -~ b))
-> (b -> a)
-> ((a >- r) -~ b)
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> a) -> r ! ((a >- r) -~ b)
forall b a r. (b -> a) -> r ! ((a >- r) -~ b)
runCofun