sessiontypes-0.1.0: Session types library

Safe HaskellSafe
LanguageHaskell2010

Control.SessionTypes.Codensity

Description

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

Synopsis

Documentation

newtype IxC m s r a Source #

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

Instances

Monad m => MonadSession (IxC m) Source # 

Methods

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

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

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

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

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

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 Source #

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

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

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

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

IxMonad (Cap *) (IxC m) Source # 

Methods

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

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

return :: a -> m i i a Source #

fail :: String -> m i i a Source #

IxApplicative (Cap *) (IxC m) Source # 

Methods

pure :: a -> f i i a Source #

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

IxFunctor (Cap *) (IxC m) Source # 

Methods

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

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

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 Source #

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.