{- |
Module      :  Control.Monad.Trans.Indexed.Cont
Copyright   :  (C) 2024 Eitan Chatav
License     :  BSD 3-Clause License (see the file LICENSE)
Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>

The continuation indexed monad transformer.
-}

module Control.Monad.Trans.Indexed.Cont
  ( ContIx (..)
  , callCCIx
  , evalContIx
  , mapContIx
  , withContIx
  , resetIx
  , shiftIx
  , toContT
  , fromContT
  ) where

import Control.Monad.Cont
import Control.Monad.Trans
import Control.Monad.Trans.Indexed

newtype ContIx i j m x = ContIx {forall {k} (i :: k) (j :: k) (m :: k -> *) x.
ContIx i j m x -> (x -> m j) -> m i
runContIx :: (x -> m j) -> m i}
  deriving (forall a b. (a -> b) -> ContIx i j m a -> ContIx i j m b)
-> (forall a b. a -> ContIx i j m b -> ContIx i j m a)
-> Functor (ContIx i j m)
forall k (i :: k) (j :: k) (m :: k -> *) a b.
a -> ContIx i j m b -> ContIx i j m a
forall k (i :: k) (j :: k) (m :: k -> *) a b.
(a -> b) -> ContIx i j m a -> ContIx i j m b
forall a b. a -> ContIx i j m b -> ContIx i j m a
forall a b. (a -> b) -> ContIx i j m a -> ContIx i j m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k (i :: k) (j :: k) (m :: k -> *) a b.
(a -> b) -> ContIx i j m a -> ContIx i j m b
fmap :: forall a b. (a -> b) -> ContIx i j m a -> ContIx i j m b
$c<$ :: forall k (i :: k) (j :: k) (m :: k -> *) a b.
a -> ContIx i j m b -> ContIx i j m a
<$ :: forall a b. a -> ContIx i j m b -> ContIx i j m a
Functor
instance IxMonadTrans ContIx where
  joinIx :: forall (m :: * -> *) i j k1 y.
Monad m =>
ContIx i j m (ContIx j k1 m y) -> ContIx i k1 m y
joinIx (ContIx (ContIx j k1 m y -> m j) -> m i
k) = ((y -> m k1) -> m i) -> ContIx i k1 m y
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((y -> m k1) -> m i) -> ContIx i k1 m y)
-> ((y -> m k1) -> m i) -> ContIx i k1 m y
forall a b. (a -> b) -> a -> b
$ \y -> m k1
f -> (ContIx j k1 m y -> m j) -> m i
k ((ContIx j k1 m y -> m j) -> m i)
-> (ContIx j k1 m y -> m j) -> m i
forall a b. (a -> b) -> a -> b
$ \(ContIx (y -> m k1) -> m j
g) -> (y -> m k1) -> m j
g y -> m k1
f
instance i ~ j => Applicative (ContIx i j m) where
  pure :: forall a. a -> ContIx i j m a
pure a
x = ((a -> m j) -> m i) -> ContIx i j m a
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((a -> m j) -> m i) -> ContIx i j m a)
-> ((a -> m j) -> m i) -> ContIx i j m a
forall a b. (a -> b) -> a -> b
$ \a -> m j
k -> a -> m j
k a
x
  ContIx ((a -> b) -> m j) -> m i
cf <*> :: forall a b.
ContIx i j m (a -> b) -> ContIx i j m a -> ContIx i j m b
<*> ContIx (a -> m j) -> m i
cx = ((b -> m j) -> m i) -> ContIx i j m b
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((b -> m j) -> m i) -> ContIx i j m b)
-> ((b -> m j) -> m i) -> ContIx i j m b
forall a b. (a -> b) -> a -> b
$ \ b -> m j
k -> ((a -> b) -> m j) -> m i
cf (((a -> b) -> m j) -> m i) -> ((a -> b) -> m j) -> m i
forall a b. (a -> b) -> a -> b
$ \ a -> b
f -> (a -> m j) -> m i
cx (b -> m j
k (b -> m j) -> (a -> b) -> a -> m j
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)
instance i ~ j => Monad (ContIx i j m) where
  return :: forall a. a -> ContIx i j m a
return = a -> ContIx i j m a
forall a. a -> ContIx i j m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  ContIx (a -> m j) -> m i
cx >>= :: forall a b.
ContIx i j m a -> (a -> ContIx i j m b) -> ContIx i j m b
>>= a -> ContIx i j m b
k = ((b -> m j) -> m i) -> ContIx i j m b
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((b -> m j) -> m i) -> ContIx i j m b)
-> ((b -> m j) -> m i) -> ContIx i j m b
forall a b. (a -> b) -> a -> b
$ \ b -> m j
c -> (a -> m j) -> m i
cx (\ a
x -> ContIx j j m b -> (b -> m j) -> m j
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
ContIx i j m x -> (x -> m j) -> m i
runContIx (a -> ContIx i j m b
k a
x) b -> m j
c)
instance i ~ j => MonadTrans (ContIx i j) where
  lift :: forall (m :: * -> *) a. Monad m => m a -> ContIx i j m a
lift = ((a -> m j) -> m i) -> ContIx i j m a
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((a -> m j) -> m i) -> ContIx i j m a)
-> (m a -> (a -> m j) -> m i) -> m a -> ContIx i j m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> (a -> m j) -> m i
m a -> (a -> m j) -> m j
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
(>>=)
instance i ~ j => MonadCont (ContIx i j m) where callCC :: forall a b.
((a -> ContIx i j m b) -> ContIx i j m a) -> ContIx i j m a
callCC = ((a -> ContIx i j m b) -> ContIx i i m a) -> ContIx i i m a
((a -> ContIx i j m b) -> ContIx i j m a) -> ContIx i j m a
forall {k} x (j :: k) (k :: k) (m :: k -> *) y (i :: k).
((x -> ContIx j k m y) -> ContIx i j m x) -> ContIx i j m x
callCCIx

evalContIx :: Monad m => ContIx x j m j -> m x
evalContIx :: forall (m :: * -> *) x j. Monad m => ContIx x j m j -> m x
evalContIx ContIx x j m j
c = ContIx x j m j -> (j -> m j) -> m x
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
ContIx i j m x -> (x -> m j) -> m i
runContIx ContIx x j m j
c j -> m j
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

mapContIx :: (m i -> m j) -> ContIx i k m x -> ContIx j k m x
mapContIx :: forall {k} (m :: k -> *) (i :: k) (j :: k) (k :: k) x.
(m i -> m j) -> ContIx i k m x -> ContIx j k m x
mapContIx m i -> m j
g (ContIx (x -> m k) -> m i
f) = ((x -> m k) -> m j) -> ContIx j k m x
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((x -> m k) -> m j) -> ContIx j k m x)
-> ((x -> m k) -> m j) -> ContIx j k m x
forall a b. (a -> b) -> a -> b
$ m i -> m j
g (m i -> m j) -> ((x -> m k) -> m i) -> (x -> m k) -> m j
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> m k) -> m i
f

withContIx :: ((y -> m k) -> x -> m j) -> ContIx i j m x -> ContIx i k m y
withContIx :: forall {k} y (m :: k -> *) (k :: k) x (j :: k) (i :: k).
((y -> m k) -> x -> m j) -> ContIx i j m x -> ContIx i k m y
withContIx (y -> m k) -> x -> m j
f (ContIx (x -> m j) -> m i
g) = ((y -> m k) -> m i) -> ContIx i k m y
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((y -> m k) -> m i) -> ContIx i k m y)
-> ((y -> m k) -> m i) -> ContIx i k m y
forall a b. (a -> b) -> a -> b
$ (x -> m j) -> m i
g ((x -> m j) -> m i)
-> ((y -> m k) -> x -> m j) -> (y -> m k) -> m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (y -> m k) -> x -> m j
f

callCCIx :: ((x -> ContIx j k m y) -> ContIx i j m x) -> ContIx i j m x
callCCIx :: forall {k} x (j :: k) (k :: k) (m :: k -> *) y (i :: k).
((x -> ContIx j k m y) -> ContIx i j m x) -> ContIx i j m x
callCCIx (x -> ContIx j k m y) -> ContIx i j m x
f = ((x -> m j) -> m i) -> ContIx i j m x
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((x -> m j) -> m i) -> ContIx i j m x)
-> ((x -> m j) -> m i) -> ContIx i j m x
forall a b. (a -> b) -> a -> b
$ \x -> m j
k -> ContIx i j m x -> (x -> m j) -> m i
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
ContIx i j m x -> (x -> m j) -> m i
runContIx ((x -> ContIx j k m y) -> ContIx i j m x
f (((y -> m k) -> m j) -> ContIx j k m y
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (((y -> m k) -> m j) -> ContIx j k m y)
-> (x -> (y -> m k) -> m j) -> x -> ContIx j k m y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m j -> (y -> m k) -> m j
forall a b. a -> b -> a
const (m j -> (y -> m k) -> m j) -> (x -> m j) -> x -> (y -> m k) -> m j
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> m j
k)) x -> m j
k

shiftIx :: Monad m => ((x -> m j) -> ContIx i k m k) -> ContIx i j m x
shiftIx :: forall (m :: * -> *) x j i k.
Monad m =>
((x -> m j) -> ContIx i k m k) -> ContIx i j m x
shiftIx (x -> m j) -> ContIx i k m k
f = ((x -> m j) -> m i) -> ContIx i j m x
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (ContIx i k m k -> m i
forall (m :: * -> *) x j. Monad m => ContIx x j m j -> m x
evalContIx (ContIx i k m k -> m i)
-> ((x -> m j) -> ContIx i k m k) -> (x -> m j) -> m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> m j) -> ContIx i k m k
f)

resetIx :: Monad m => ContIx x j m j -> ContIx i i m x
resetIx :: forall (m :: * -> *) x j i.
Monad m =>
ContIx x j m j -> ContIx i i m x
resetIx = m x -> ContIx i i m x
forall (m :: * -> *) a. Monad m => m a -> ContIx i i m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m x -> ContIx i i m x)
-> (ContIx x j m j -> m x) -> ContIx x j m j -> ContIx i i m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContIx x j m j -> m x
forall (m :: * -> *) x j. Monad m => ContIx x j m j -> m x
evalContIx

toContT :: ContIx i i m x -> ContT i m x
toContT :: forall {k} (i :: k) (m :: k -> *) x. ContIx i i m x -> ContT i m x
toContT (ContIx (x -> m i) -> m i
f) = ((x -> m i) -> m i) -> ContT i m x
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (x -> m i) -> m i
f

fromContT :: ContT i m x -> ContIx i i m x
fromContT :: forall {k} (i :: k) (m :: k -> *) x. ContT i m x -> ContIx i i m x
fromContT (ContT (x -> m i) -> m i
f) = ((x -> m i) -> m i) -> ContIx i i m x
forall {k} (i :: k) (j :: k) (m :: k -> *) x.
((x -> m j) -> m i) -> ContIx i j m x
ContIx (x -> m i) -> m i
f