Data.Comp.Thunk

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

Documentation

type TermT m f = Term (m :+: f)

This type represents terms with thunks.

type CxtT m h f a = Cxt h (m :+: f) a

This type represents contexts with thunks.

thunk :: m (CxtT m h f a) -> CxtT m h f a

This function turns a monadic computation into a thunk.

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

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

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

whnfPr :: (MonadFail m, g :<: f) => TermT m f -> m (g (TermT m f))

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, Traversable f) => TermT m f -> m (Term f)

This function evaluates all thunks.

nfPr :: (MonadFail m, Traversable g, g :<: f) => TermT m f -> m (Term g)

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 f

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 f

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 f

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 f

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 f infixl 1

Variant of eval with flipped argument positions

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

Variant of deepEval with flipped argument positions

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

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

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

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 a

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 Bool

This function decides equality of terms with thunks.

strict :: (f :<: g, Traversable f, Monad m) => f (TermT m g) -> TermT m g

This combinator makes the evaluation of the given functor application strict by evaluating all thunks of immediate subterms.

strictAt :: (f :<: g, Traversable f, Monad m) => Pos f -> f (TermT m g) -> TermT m g

This combinator is a variant of strict that only makes a subset of the arguments of a functor application strict. The first argument of this combinator specifies which positions are supposed to be strict.