Copyright | (C) 2012 Edward Kmett |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | experimental |
Portability | portable |
Safe Haskell | Trustworthy |
Language | Haskell98 |
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
is a value
Name
n bb
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 = Name n b
- _Name :: (Profunctor p, Functor f) => p (n, a) (f (m, b)) -> p (Name n a) (f (Name m b))
- name :: Name n b -> n
- abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a
- abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a
- instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a
- instantiate1Name :: Monad f => f a -> Scope n f a -> f a
Documentation
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 (
instead.on
compare
name
)
Name n b |
Eq2 Name Source # | |
Ord2 Name Source # | |
Read2 Name Source # | |
Show2 Name Source # | |
Bifunctor Name Source # | |
Bitraversable Name Source # | |
Bifoldable Name Source # | |
Serial2 Name Source # | |
Hashable2 Name Source # | |
Functor (Name n) Source # | |
Foldable (Name n) Source # | |
Traversable (Name n) Source # | |
Eq1 (Name b) Source # | |
Ord1 (Name b) Source # | |
Read b => Read1 (Name b) Source # | |
Show b => Show1 (Name b) Source # | |
Serial b => Serial1 (Name b) Source # | |
Comonad (Name n) Source # | |
Hashable1 (Name n) Source # | |
Eq b => Eq (Name n b) Source # | |
(Data b, Data n) => Data (Name n b) Source # | |
Ord b => Ord (Name n b) Source # | |
(Read b, Read n) => Read (Name n b) Source # | |
(Show b, Show n) => Show (Name n b) Source # | |
Generic (Name n b) Source # | |
(Binary b, Binary a) => Binary (Name b a) Source # | |
(Serial b, Serial a) => Serial (Name b a) Source # | |
(Serialize b, Serialize a) => Serialize (Name b a) Source # | |
(NFData b, NFData a) => NFData (Name b a) Source # | |
Hashable a => Hashable (Name n a) Source # | |
type Rep (Name n b) Source # | |
abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a Source #
Abstraction, capturing named bound variables.
abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a Source #
Abstract over a single variable
instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a Source #
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 a Source #
Enter a Scope
that binds one (named) variable, instantiating it.
instantiate1Name
=instantiate1