{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Continuations, modelled as functions wrapped in a contravariant functor.
module Data.Functor.Continuation
( -- * Continuations
  type (!)(..)
  -- * Contravariant
, Contravariant(..)
, Representable(..)
  -- * Construction
, idK
) where

import qualified Control.Category as Cat
import           Data.Functor.Contravariant
import           Data.Functor.Contravariant.Adjunction
import           Data.Functor.Contravariant.Rep

-- Continuations

-- | Continuations, represented as functions. Note that the type parameters are in the opposite order, making this type a 'Contravariant' functor.
newtype r ! a = K { (!) :: a -> r }

infixl 7 !

instance Cat.Category (!) where
  id :: a ! a
id = a ! a
forall a. a ! a
idK
  b ! c
j . :: (b ! c) -> (a ! b) -> a ! c
. a ! b
k = (c -> a) -> a ! c
forall r a. (a -> r) -> r ! a
K ((a ! b
k (a ! b) -> b -> a
forall r a. (r ! a) -> a -> r
!) (b -> a) -> (c -> b) -> c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b ! c
j (b ! c) -> c -> b
forall r a. (r ! a) -> a -> r
!))

instance Contravariant ((!) r) where
  contramap :: (a -> b) -> (r ! b) -> r ! a
contramap a -> b
f = (a -> r) -> r ! a
forall r a. (a -> r) -> r ! a
K ((a -> r) -> r ! a) -> ((r ! b) -> a -> r) -> (r ! b) -> r ! a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b -> r) -> (a -> b) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) ((b -> r) -> a -> r) -> ((r ! b) -> b -> r) -> (r ! b) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (!)

instance Representable ((!) r) where
  type Rep ((!) r) = r
  tabulate :: (a -> Rep ((!) r)) -> r ! a
tabulate = (a -> Rep ((!) r)) -> r ! a
forall r a. (a -> r) -> r ! a
K
  index :: (r ! a) -> a -> Rep ((!) r)
index = (!)

instance r ~ s => Adjunction ((!) r) ((!) s) where
  unit :: a -> s ! (r ! a)
unit   a
a = ((s ! a) -> s) -> s ! (s ! a)
forall r a. (a -> r) -> r ! a
K ((s ! a) -> a -> s
forall r a. (r ! a) -> a -> r
! a
a)
  counit :: a -> r ! (s ! a)
counit a
a = ((r ! a) -> r) -> r ! (r ! a)
forall r a. (a -> r) -> r ! a
K ((r ! a) -> a -> r
forall r a. (r ! a) -> a -> r
! a
a)

  leftAdjunct :: (b -> r ! a) -> a -> s ! b
leftAdjunct  b -> r ! a
f a
a = (b -> r) -> r ! b
forall r a. (a -> r) -> r ! a
K (((r ! a) -> a -> r
forall r a. (r ! a) -> a -> r
! a
a) ((r ! a) -> r) -> (b -> r ! a) -> b -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> r ! a
f)
  rightAdjunct :: (a -> s ! b) -> b -> r ! a
rightAdjunct a -> s ! b
f b
a = (a -> s) -> s ! a
forall r a. (a -> r) -> r ! a
K (((s ! b) -> b -> s
forall r a. (r ! a) -> a -> r
! b
a) ((s ! b) -> s) -> (a -> s ! b) -> a -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> s ! b
f)


-- Construction

idK :: a ! a
idK :: a ! a
idK = (a -> a) -> a ! a
forall r a. (a -> r) -> r ! a
K a -> a
forall a. a -> a
id