Copyright | (c) 2011 Patrick Bahr |
---|---|
License | BSD3 |
Maintainer | Patrick Bahr <paba@diku.dk> |
Stability | experimental |
Portability | non-portable (GHC Extensions) |
Safe Haskell | None |
Language | Haskell98 |
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 b Source
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 a Source
type AlgT m f g = Alg f (TermT m g) Source
This type represents algebras which have terms with thunks as carrier.