Portability | non-portable (GHC Extensions) |
---|---|

Stability | experimental |

Maintainer | Patrick Bahr <paba@diku.dk> |

This modules defines terms & contexts with thunks, with deferred monadic computations.

- type TermT m f = Term (Thunk m :+: f)
- type TrmT m f a = Trm (Thunk m :+: f) a
- type CxtT h m f a = Cxt h (Thunk m :+: f) a
- data Thunk m a b
- thunk :: (Thunk m) :<: f => m (Cxt h f a b) -> Cxt h f a b
- whnf :: Monad m => TrmT m f a -> m (Either a (f a (TrmT m f a)))
- whnf' :: Monad m => TrmT m f a -> m (TrmT m f a)
- whnfPr :: (Monad m, g :<: f) => TrmT m f a -> m (g a (TrmT m f a))
- nf :: (Monad m, Ditraversable f) => TrmT m f a -> m (Trm f a)
- nfT :: (ParamFunctor m, Monad m, Ditraversable f) => TermT m f -> m (Term f)
- nfPr :: (Monad m, Ditraversable g, g :<: f) => TrmT m f a -> m (Trm g a)
- nfTPr :: (ParamFunctor m, Monad m, Ditraversable g, g :<: f) => TermT m f -> m (Term g)
- evalStrict :: (Ditraversable g, Monad m, g :<: f) => (g (TrmT m f a) (f a (TrmT m f a)) -> TrmT m f a) -> g (TrmT m f a) (TrmT m f a) -> TrmT m f a
- type AlgT m f g = Alg f (TermT m g)
- strict :: (f :<: g, Ditraversable f, Monad m) => f a (TrmT m g a) -> TrmT m g a
- strict' :: (f :<: g, Ditraversable f, Monad m) => f (TrmT m g a) (TrmT m g a) -> TrmT m g a

# Documentation

thunk :: (Thunk m) :<: f => m (Cxt h f a b) -> Cxt h f a bSource

This function turns a monadic computation into a thunk.

whnf :: Monad m => TrmT m f a -> m (Either a (f a (TrmT m f a)))Source

This function evaluates all thunks until a non-thunk node is found.

whnfPr :: (Monad m, g :<: f) => TrmT m f a -> m (g a (TrmT m f a))Source

This function first evaluates the argument term into whnf via
`whnf`

and then projects the top-level signature to the desired
subsignature. Failure to do the projection is signalled as a
failure in the monad.

nf :: (Monad m, Ditraversable f) => TrmT m f a -> m (Trm f a)Source

This function evaluates all thunks.

nfT :: (ParamFunctor m, Monad m, Ditraversable f) => TermT m f -> m (Term f)Source

This function evaluates all thunks.

nfPr :: (Monad m, Ditraversable g, g :<: f) => TrmT m f a -> m (Trm g a)Source

This function evaluates all thunks while simultaneously
projecting the term to a smaller signature. Failure to do the
projection is signalled as a failure in the monad as in `whnfPr`

.

nfTPr :: (ParamFunctor m, Monad m, Ditraversable g, g :<: f) => TermT m f -> m (Term g)Source

This function evaluates all thunks while simultaneously
projecting the term to a smaller signature. Failure to do the
projection is signalled as a failure in the monad as in `whnfPr`

.

evalStrict :: (Ditraversable g, Monad m, g :<: f) => (g (TrmT m f a) (f a (TrmT m f a)) -> TrmT m f a) -> g (TrmT m f a) (TrmT m f a) -> TrmT m f aSource

type AlgT m f g = Alg f (TermT m g)Source

This type represents algebras which have terms with thunks as carrier.