Copyright	(c) 2011 Patrick Bahr
License	BSD3
Maintainer	Patrick Bahr <[email protected]>
Stability	experimental
Portability	non-portable (GHC Extensions)
Safe Haskell	None
Language	Haskell2010

Data.Comp.Thunk

Description

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

Synopsis

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

Documentation

type TermT (m :: Type -> Type) (f :: Type -> Type) = Term (m :+: f) Source #

This type represents terms with thunks.

type CxtT (m :: Type -> Type) h (f :: Type -> Type) a = Cxt h (m :+: f) a Source #

This type represents contexts with thunks.

thunk :: forall m h (f :: Type -> Type) a. m (CxtT m h f a) -> CxtT m h f a Source #

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.

whnf' :: forall m (f :: Type -> Type). Monad m => TermT m f -> m (TermT m f) Source #

whnfPr :: forall m g (f :: Type -> Type). (MonadFail 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.

nf :: forall m (f :: Type -> Type). (Monad m, Traversable f) => TermT m f -> m (Term f) Source #

This function evaluates all thunks.

nfPr :: forall m (g :: Type -> Type) (f :: Type -> Type). (MonadFail 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 :: forall (m :: Type -> Type) f. Monad m => (f (TermT m f) -> TermT m f) -> TermT m f -> TermT m f Source #

This function inspects the topmost non-thunk node (using whnf) according to the given function.

eval2 :: forall (m :: Type -> Type) f. Monad m => (f (TermT m f) -> f (TermT m f) -> TermT m f) -> TermT m f -> TermT m f -> TermT m f Source #

This function inspects the topmost non-thunk nodes of two terms (using whnf) according to the given function.

deepEval :: forall (f :: Type -> Type) (m :: Type -> Type). (Traversable f, Monad m) => (Term f -> TermT m f) -> TermT m f -> TermT m f Source #

This function inspects a term (using nf) according to the given function.

deepEval2 :: forall (m :: Type -> Type) (f :: Type -> Type). (Monad m, Traversable f) => (Term f -> Term f -> TermT m f) -> TermT m f -> TermT m f -> TermT m f Source #

This function inspects two terms (using nf) according to the given function.

(#>) :: forall (m :: Type -> Type) f. Monad m => TermT m f -> (f (TermT m f) -> TermT m f) -> TermT m f infixl 1 Source #

Variant of eval with flipped argument positions

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

Variant of deepEval with flipped argument positions

type AlgT (m :: Type -> Type) (f :: Type -> Type) (g :: Type -> Type) = 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 a Source #

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

This combinator runs a monadic catamorphism on a term with thunks

eqT :: forall (f :: Type -> Type) m. (EqF f, Foldable f, Functor f, Monad m) => TermT m f -> TermT m f -> m Bool Source #

This function decides equality of terms with thunks.

strict :: forall f (g :: Type -> Type) (m :: Type -> Type). (f :<: g, Traversable f, Monad m) => f (TermT m g) -> TermT m g Source #

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

strictAt :: forall f (g :: Type -> Type) (m :: Type -> Type). (f :<: g, Traversable f, Monad m) => Pos f -> f (TermT m g) -> TermT m g Source #

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.