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

Bound.Name

Description

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.

Synopsis

Documentation

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.

Constructors

Name n b

Instances

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)
Typeable (* -> * -> *) Name
type Rep (Name n b)

_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 -> n Source

Extract the name.

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