bound-1.0.2: Making de Bruijn Succ Less

MaintainerEdward Kmett <>
Safe HaskellTrustworthy



The problem with locally nameless approaches is that original names are often useful for error reporting, or to allow for the user in an interactive theorem prover to convey some hint about the domain. A Name n b is a value b supplemented with a (discardable) name that may be useful for error reporting purposes. In particular, this name does not participate in comparisons for equality.

This module is not exported from Bound by default. You need to explicitly import it, due to the fact that Name is a pretty common term in other people's code.



data Name n b Source

We track the choice of Name n as a forgettable property that does not affect the result of (==) or compare.

To compare names rather than values, use (on compare name) instead.


Name n b 


Typeable2 Name 
Bitraversable Name 
Bifunctor Name 
Bifoldable Name 
Serial2 Name 
Hashable2 Name 
Eq2 Name 
Ord2 Name 
Show2 Name 
Read2 Name 
Functor (Name n) 
Foldable (Name n) 
Traversable (Name n) 
Serial b => Serial1 (Name b) 
Comonad (Name n) 
Hashable1 (Name n) 
Eq1 (Name b) 
Ord1 (Name b) 
Show b => Show1 (Name b) 
Read b => Read1 (Name b) 
Eq b => Eq (Name n b) 
(Data n, Data b) => Data (Name n b) 
Ord b => Ord (Name n b) 
(Read n, Read b) => Read (Name n b) 
(Show n, Show b) => Show (Name n b) 
Generic (Name n b) 
(Binary b, Binary a) => Binary (Name b a) 
(Serial b, Serial a) => Serial (Name b a) 
(Serialize b, Serialize a) => Serialize (Name b a) 
Hashable a => Hashable (Name n a) 

_Name :: (Profunctor p, Functor f) => p (n, a) (f (m, b)) -> p (Name n a) (f (Name m b))Source

This provides an Iso that can be used to access the parts of a Name.

 _Name :: Iso (Name n a) (Name m b) (n, a) (m, b)

name :: Name n b -> nSource

Extract the name.

abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f aSource

Abstraction, capturing named bound variables.

abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f aSource

Abstract over a single variable

instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f aSource

Enter a scope, instantiating all bound variables, but discarding (comonadic) meta data, like its name

instantiate1Name :: Monad f => f a -> Scope n f a -> f aSource

Enter a Scope that binds one (named) variable, instantiating it.

instantiate1Name = instantiate1