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 (m :+: f)
- type CxtT m h f a = Cxt h (m :+: f) a
- thunk :: m :<: f => m (Cxt h f a) -> Cxt h f a
- whnf :: Monad m => TermT m f -> m (f (TermT m f))
- whnf' :: Monad m => TermT m f -> m (TermT m f)
- whnfPr :: (Monad m, g :<: f) => TermT m f -> m (g (TermT m f))
- nf :: (Monad m, Traversable f) => TermT m f -> m (Term f)
- nfPr :: (Monad m, Traversable g, g :<: f) => TermT m f -> m (Term g)
- eval :: Monad m => (f (TermT m f) -> TermT m f) -> TermT m f -> TermT m f
- eval2 :: Monad m => (f (TermT m f) -> f (TermT m f) -> TermT m f) -> TermT m f -> TermT m f -> TermT m f
- deepEval :: (Traversable f, Monad m) => (Term f -> TermT m f) -> TermT m f -> TermT m f
- deepEval2 :: (Monad m, Traversable f) => (Term f -> Term f -> TermT m f) -> TermT m f -> TermT m f -> TermT m f
- (#>) :: Monad m => TermT m f -> (f (TermT m f) -> TermT m f) -> TermT m f
- (#>>) :: (Monad m, Traversable f) => TermT m f -> (Term f -> TermT m f) -> TermT m f
- type AlgT m f g = Alg f (TermT m g)
- cataT :: (Traversable f, Monad m) => Alg f a -> TermT m f -> m a
- cataTM :: forall m f a. (Traversable f, Monad m) => AlgM m f a -> TermT m f -> m a
- eqT :: (EqF f, Foldable f, Functor f, Monad m) => TermT m f -> TermT m f -> m Bool
- strict :: (f :<: g, Traversable f, Monad m) => f (TermT m g) -> TermT m g
- strictAt :: (f :<: g, Traversable f, Monad m) => Pos f -> f (TermT m g) -> TermT m g

# Documentation

thunk :: m :<: f => m (Cxt h f a) -> Cxt h f aSource

This function turns a monadic computation into a thunk.

whnf :: Monad m => TermT m f -> m (f (TermT m f))Source

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

whnfPr :: (Monad m, g :<: f) => TermT m f -> m (g (TermT m f))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.

nfPr :: (Monad m, Traversable 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`

.

eval :: Monad m => (f (TermT m f) -> TermT m f) -> TermT m f -> TermT m fSource

This function inspects the topmost non-thunk node (using
`whnf`

) according to the given function.

eval2 :: Monad m => (f (TermT m f) -> f (TermT m f) -> TermT m f) -> TermT m f -> TermT m f -> TermT m fSource

This function inspects the topmost non-thunk nodes of two terms
(using `whnf`

) according to the given function.

deepEval :: (Traversable f, Monad m) => (Term f -> TermT m f) -> TermT m f -> TermT m fSource

This function inspects a term (using `nf`

) according to the
given function.

deepEval2 :: (Monad m, Traversable f) => (Term f -> Term f -> TermT m f) -> TermT m f -> TermT m f -> TermT m fSource

This function inspects two terms (using `nf`

) according
to the given function.

(#>) :: Monad m => TermT m f -> (f (TermT m f) -> TermT m f) -> TermT m fSource

Variant of `eval`

with flipped argument positions

(#>>) :: (Monad m, Traversable f) => TermT m f -> (Term f -> TermT m f) -> TermT m fSource

Variant of `deepEval`

with flipped argument positions

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

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

cataT :: (Traversable f, Monad m) => Alg f a -> TermT m f -> m aSource

This combinator runs a catamorphism on a term with thunks.

cataTM :: forall m f a. (Traversable f, Monad m) => AlgM m f a -> TermT m f -> m aSource

This combinator runs a monadic catamorphism on a term with thunks

eqT :: (EqF f, Foldable f, Functor f, Monad m) => TermT m f -> TermT m f -> m BoolSource

This function decides equality of terms with thunks.