Control.SessionTypes.Codensity

This module defines a new type for constructing more efficient STTerm programs.

Documentation

newtype IxC m s r a

We define an indexed codensity monad that allows us to reduce quadratic complexity from repeated use of (>>=) in a session typed program to linear complexity.

Constructors

IxC

Fields

• runIxC :: forall b k. (a -> STTerm m r k b) -> STTerm m s k b

Instances

Monad m => MonadSession (IxC m)

Methods

send :: a -> IxC m (Cap * ctx ((* :!> a) r)) (Cap * ctx r) ()

recv :: IxC m (Cap * ctx ((* :?> a) r)) (Cap * ctx r) a

sel1 :: IxC m (Cap * ctx (Sel * ((ST * ': s) xs))) (Cap * ctx s) ()

sel2 :: IxC m (Cap * ctx (Sel * ((ST * ': s) ((ST * ': t) xs)))) (Cap * ctx (Sel * ((ST * ': t) xs))) ()

offZ :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ctx (Off * ((ST * ': s) [ST *]))) r a

offS :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ctx (Off * ((ST * ': t) xs))) r a -> IxC m (Cap * ctx (Off * ((ST * ': s) ((ST * ': t) xs)))) r a

recurse :: IxC m (Cap * ((ST * ': s) ctx) s) r a -> IxC m (Cap * ctx (R * s)) r a

weaken :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ((ST * ': t) ctx) (Wk * s)) r a

var :: IxC m (Cap * ((ST * ': s) ctx) s) r a -> IxC m (Cap * ((ST * ': s) ctx) (V *)) r a

eps :: a -> IxC m (Cap * ctx (Eps *)) (Cap * ctx (Eps *)) a

IxMonad (Cap *) (IxC m)

Methods

(>>=) :: m s t a -> (a -> m t k b) -> m s k b

(>>) :: m s t a -> m t k b -> m s k b

return :: a -> m i i a

fail :: String -> m i i a

IxApplicative (Cap *) (IxC m)

Methods

pure :: a -> f i i a

(<*>) :: f s r (a -> b) -> f r k a -> f s k b

IxFunctor (Cap *) (IxC m)

Methods

fmap :: (a -> b) -> f j k a -> f j k b

abs :: Monad m => IxC m s r a -> STTerm m s r a

Turns the IxC representation of a program to the STTerm representation.

The idea is to apply abs on a IxC program to make the resulting STTerm program more efficient.

rep :: Monad m => STTerm m s r a -> IxC m s r a

Transforms an STTerm program into a IxC representation.

Note that applying this function to a session typed program and then applying abs to the result will not be more efficient.

This is because applying rep already induces quadratic complexity.