Unbound.LocallyNameless.Fresh

The Fresh and LFresh classes, which govern monads with fresh name generation capabilities, and the FreshM(T) and LFreshM(T) monad (transformers) which provide useful default implementations.

The Fresh class

class Monad m => Fresh m where

The Fresh type class governs monads which can generate new globally unique Names based on a given Name.

Minimal complete definition

fresh

Methods

fresh :: Rep a => Name a -> m (Name a)

Generate a new globally unique name based on the given one.

Instances

Fresh m => Fresh (ListT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> ListT m (Name a)

Fresh m => Fresh (MaybeT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> MaybeT m (Name a)

Monad m => Fresh (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> FreshMT m (Name a)

Fresh m => Fresh (IdentityT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> IdentityT m (Name a)

Fresh m => Fresh (ExceptT e m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> ExceptT e m (Name a)

Fresh m => Fresh (StateT s m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> StateT s m (Name a)

Fresh m => Fresh (StateT s m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> StateT s m (Name a)

(Monoid w, Fresh m) => Fresh (WriterT w m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> WriterT w m (Name a)

(Monoid w, Fresh m) => Fresh (WriterT w m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> WriterT w m (Name a)

Fresh m => Fresh (ContT r m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> ContT r m (Name a)

Fresh m => Fresh (ReaderT r m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> ReaderT r m (Name a)

type FreshM = FreshMT Identity

A convenient monad which is an instance of Fresh. It keeps track of a global index used for generating fresh names, which is incremented every time fresh is called.

runFreshM :: FreshM a -> a

Run a FreshM computation (with the global index starting at zero).

contFreshM :: FreshM a -> Integer -> a

Run a FreshM computation given a starting index.

newtype FreshMT m a

The FreshM monad transformer. Keeps track of the lowest index still globally unused, and increments the index every time it is asked for a fresh name.

Constructors

FreshMT

Fields

• unFreshMT :: StateT Integer m a

Instances

MonadTrans FreshMT

Defined in Unbound.LocallyNameless.Fresh

Methods

lift :: Monad m => m a -> FreshMT m a

MonadWriter w m => MonadWriter w (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

writer :: (a, w) -> FreshMT m a

tell :: w -> FreshMT m ()

listen :: FreshMT m a -> FreshMT m (a, w)

pass :: FreshMT m (a, w -> w) -> FreshMT m a

MonadState s m => MonadState s (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

get :: FreshMT m s

put :: s -> FreshMT m ()

state :: (s -> (a, s)) -> FreshMT m a

MonadReader r m => MonadReader r (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

ask :: FreshMT m r

local :: (r -> r) -> FreshMT m a -> FreshMT m a

reader :: (r -> a) -> FreshMT m a

MonadError e m => MonadError e (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

throwError :: e -> FreshMT m a

catchError :: FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a

Monad m => Monad (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

(>>=) :: FreshMT m a -> (a -> FreshMT m b) -> FreshMT m b

(>>) :: FreshMT m a -> FreshMT m b -> FreshMT m b

return :: a -> FreshMT m a

fail :: String -> FreshMT m a

Functor m => Functor (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fmap :: (a -> b) -> FreshMT m a -> FreshMT m b

(<$) :: a -> FreshMT m b -> FreshMT m a

MonadFix m => MonadFix (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

mfix :: (a -> FreshMT m a) -> FreshMT m a

Monad m => Applicative (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

pure :: a -> FreshMT m a

(<*>) :: FreshMT m (a -> b) -> FreshMT m a -> FreshMT m b

liftA2 :: (a -> b -> c) -> FreshMT m a -> FreshMT m b -> FreshMT m c

(*>) :: FreshMT m a -> FreshMT m b -> FreshMT m b

(<*) :: FreshMT m a -> FreshMT m b -> FreshMT m a

MonadIO m => MonadIO (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

liftIO :: IO a -> FreshMT m a

MonadPlus m => Alternative (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

empty :: FreshMT m a

(<|>) :: FreshMT m a -> FreshMT m a -> FreshMT m a

some :: FreshMT m a -> FreshMT m [a]

many :: FreshMT m a -> FreshMT m [a]

MonadPlus m => MonadPlus (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

mzero :: FreshMT m a

mplus :: FreshMT m a -> FreshMT m a -> FreshMT m a

MonadCont m => MonadCont (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

callCC :: ((a -> FreshMT m b) -> FreshMT m a) -> FreshMT m a

Monad m => Fresh (FreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fresh :: Rep a => Name a -> FreshMT m (Name a)

runFreshMT :: Monad m => FreshMT m a -> m a

Run a FreshMT computation (with the global index starting at zero).

contFreshMT :: Monad m => FreshMT m a -> Integer -> m a

Run a FreshMT computation given a starting index for fresh name generation.

The LFresh class

class Monad m => LFresh m where

This is the class of monads that support freshness in an (implicit) local scope. Generated names are fresh for the current local scope, not necessarily globally fresh.

Minimal complete definition

lfresh, avoid, getAvoids

Methods

lfresh :: Rep a => Name a -> m (Name a)

Pick a new name that is fresh for the current (implicit) scope.

avoid :: [AnyName] -> m a -> m a

Avoid the given names when freshening in the subcomputation, that is, add the given names to the in-scope set.

getAvoids :: m (Set AnyName)

Get the set of names currently being avoided.

Instances

LFresh m => LFresh (ListT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> ListT m (Name a)

avoid :: [AnyName] -> ListT m a -> ListT m a

getAvoids :: ListT m (Set AnyName)

LFresh m => LFresh (MaybeT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> MaybeT m (Name a)

avoid :: [AnyName] -> MaybeT m a -> MaybeT m a

getAvoids :: MaybeT m (Set AnyName)

Monad m => LFresh (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> LFreshMT m (Name a)

avoid :: [AnyName] -> LFreshMT m a -> LFreshMT m a

getAvoids :: LFreshMT m (Set AnyName)

LFresh m => LFresh (IdentityT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> IdentityT m (Name a)

avoid :: [AnyName] -> IdentityT m a -> IdentityT m a

getAvoids :: IdentityT m (Set AnyName)

LFresh m => LFresh (ExceptT e m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> ExceptT e m (Name a)

avoid :: [AnyName] -> ExceptT e m a -> ExceptT e m a

getAvoids :: ExceptT e m (Set AnyName)

LFresh m => LFresh (StateT s m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> StateT s m (Name a)

avoid :: [AnyName] -> StateT s m a -> StateT s m a

getAvoids :: StateT s m (Set AnyName)

LFresh m => LFresh (StateT s m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> StateT s m (Name a)

avoid :: [AnyName] -> StateT s m a -> StateT s m a

getAvoids :: StateT s m (Set AnyName)

(Monoid w, LFresh m) => LFresh (WriterT w m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> WriterT w m (Name a)

avoid :: [AnyName] -> WriterT w m a -> WriterT w m a

getAvoids :: WriterT w m (Set AnyName)

(Monoid w, LFresh m) => LFresh (WriterT w m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> WriterT w m (Name a)

avoid :: [AnyName] -> WriterT w m a -> WriterT w m a

getAvoids :: WriterT w m (Set AnyName)

LFresh m => LFresh (ContT r m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> ContT r m (Name a)

avoid :: [AnyName] -> ContT r m a -> ContT r m a

getAvoids :: ContT r m (Set AnyName)

LFresh m => LFresh (ReaderT r m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> ReaderT r m (Name a)

avoid :: [AnyName] -> ReaderT r m a -> ReaderT r m a

getAvoids :: ReaderT r m (Set AnyName)

type LFreshM = LFreshMT Identity

A convenient monad which is an instance of LFresh. It keeps track of a set of names to avoid, and when asked for a fresh one will choose the first unused numerical name.

runLFreshM :: LFreshM a -> a

Run a LFreshM computation in an empty context.

contLFreshM :: LFreshM a -> Set AnyName -> a

Run a LFreshM computation given a set of names to avoid.

newtype LFreshMT m a

The LFresh monad transformer. Keeps track of a set of names to avoid, and when asked for a fresh one will choose the first numeric prefix of the given name which is currently unused.

Constructors

LFreshMT

Fields

• unLFreshMT :: ReaderT (Set AnyName) m a

Instances

MonadTrans LFreshMT

Defined in Unbound.LocallyNameless.Fresh

Methods

lift :: Monad m => m a -> LFreshMT m a

MonadWriter w m => MonadWriter w (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

writer :: (a, w) -> LFreshMT m a

tell :: w -> LFreshMT m ()

listen :: LFreshMT m a -> LFreshMT m (a, w)

pass :: LFreshMT m (a, w -> w) -> LFreshMT m a

MonadState s m => MonadState s (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

get :: LFreshMT m s

put :: s -> LFreshMT m ()

state :: (s -> (a, s)) -> LFreshMT m a

MonadReader r m => MonadReader r (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

ask :: LFreshMT m r

local :: (r -> r) -> LFreshMT m a -> LFreshMT m a

reader :: (r -> a) -> LFreshMT m a

MonadError e m => MonadError e (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

throwError :: e -> LFreshMT m a

catchError :: LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a

Monad m => Monad (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

(>>=) :: LFreshMT m a -> (a -> LFreshMT m b) -> LFreshMT m b

(>>) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m b

return :: a -> LFreshMT m a

fail :: String -> LFreshMT m a

Functor m => Functor (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

fmap :: (a -> b) -> LFreshMT m a -> LFreshMT m b

(<$) :: a -> LFreshMT m b -> LFreshMT m a

MonadFix m => MonadFix (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

mfix :: (a -> LFreshMT m a) -> LFreshMT m a

Applicative m => Applicative (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

pure :: a -> LFreshMT m a

(<*>) :: LFreshMT m (a -> b) -> LFreshMT m a -> LFreshMT m b

liftA2 :: (a -> b -> c) -> LFreshMT m a -> LFreshMT m b -> LFreshMT m c

(*>) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m b

(<*) :: LFreshMT m a -> LFreshMT m b -> LFreshMT m a

MonadIO m => MonadIO (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

liftIO :: IO a -> LFreshMT m a

Alternative m => Alternative (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

empty :: LFreshMT m a

(<|>) :: LFreshMT m a -> LFreshMT m a -> LFreshMT m a

some :: LFreshMT m a -> LFreshMT m [a]

many :: LFreshMT m a -> LFreshMT m [a]

MonadPlus m => MonadPlus (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

mzero :: LFreshMT m a

mplus :: LFreshMT m a -> LFreshMT m a -> LFreshMT m a

MonadCont m => MonadCont (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

callCC :: ((a -> LFreshMT m b) -> LFreshMT m a) -> LFreshMT m a

Monad m => LFresh (LFreshMT m)

Defined in Unbound.LocallyNameless.Fresh

Methods

lfresh :: Rep a => Name a -> LFreshMT m (Name a)

avoid :: [AnyName] -> LFreshMT m a -> LFreshMT m a

getAvoids :: LFreshMT m (Set AnyName)

runLFreshMT :: LFreshMT m a -> m a

Run an LFreshMT computation in an empty context.

contLFreshMT :: LFreshMT m a -> Set AnyName -> m a

Run an LFreshMT computation given a set of names to avoid.