Bound.Name

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.

Documentation

data Name n b

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

Eq2 Name

Methods

liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Name a c -> Name b d -> Bool

Ord2 Name

Methods

liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> Name a c -> Name b d -> Ordering

Read2 Name

Methods

liftReadsPrec2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> Int -> ReadS (Name a b)

liftReadList2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> ReadS [Name a b]

Show2 Name

Methods

liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> Name a b -> ShowS

liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Name a b] -> ShowS

Bifunctor Name

Methods

bimap :: (a -> b) -> (c -> d) -> Name a c -> Name b d

first :: (a -> b) -> Name a c -> Name b c

second :: (b -> c) -> Name a b -> Name a c

Bitraversable Name

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Name a b -> f (Name c d)

Bifoldable Name

Methods

bifold :: Monoid m => Name m m -> m

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Name a b -> m

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Name a b -> c

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Name a b -> c

Serial2 Name

Methods

serializeWith2 :: MonadPut m => (a -> m ()) -> (b -> m ()) -> Name a b -> m ()

deserializeWith2 :: MonadGet m => m a -> m b -> m (Name a b)

Hashable2 Name

Methods

liftHashWithSalt2 :: (Int -> a -> Int) -> (Int -> b -> Int) -> Int -> Name a b -> Int

Functor (Name n)

Methods

fmap :: (a -> b) -> Name n a -> Name n b

(<$) :: a -> Name n b -> Name n a

Foldable (Name n)

Methods

fold :: Monoid m => Name n m -> m

foldMap :: Monoid m => (a -> m) -> Name n a -> m

foldr :: (a -> b -> b) -> b -> Name n a -> b

foldr' :: (a -> b -> b) -> b -> Name n a -> b

foldl :: (b -> a -> b) -> b -> Name n a -> b

foldl' :: (b -> a -> b) -> b -> Name n a -> b

foldr1 :: (a -> a -> a) -> Name n a -> a

foldl1 :: (a -> a -> a) -> Name n a -> a

toList :: Name n a -> [a]

null :: Name n a -> Bool

length :: Name n a -> Int

elem :: Eq a => a -> Name n a -> Bool

maximum :: Ord a => Name n a -> a

minimum :: Ord a => Name n a -> a

sum :: Num a => Name n a -> a

product :: Num a => Name n a -> a

Traversable (Name n)

Methods

traverse :: Applicative f => (a -> f b) -> Name n a -> f (Name n b)

sequenceA :: Applicative f => Name n (f a) -> f (Name n a)

mapM :: Monad m => (a -> m b) -> Name n a -> m (Name n b)

sequence :: Monad m => Name n (m a) -> m (Name n a)

Eq1 (Name b)

Methods

liftEq :: (a -> b -> Bool) -> Name b a -> Name b b -> Bool

Ord1 (Name b)

Methods

liftCompare :: (a -> b -> Ordering) -> Name b a -> Name b b -> Ordering

Read b => Read1 (Name b)

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Name b a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Name b a]

Show b => Show1 (Name b)

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Name b a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Name b a] -> ShowS

Serial b => Serial1 (Name b)

Methods

serializeWith :: MonadPut m => (a -> m ()) -> Name b a -> m ()

deserializeWith :: MonadGet m => m a -> m (Name b a)

Comonad (Name n)

Methods

extract :: Name n a -> a

duplicate :: Name n a -> Name n (Name n a)

extend :: (Name n a -> b) -> Name n a -> Name n b

Hashable1 (Name n)

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> Name n a -> Int

Eq b => Eq (Name n b)

Methods

(==) :: Name n b -> Name n b -> Bool

(/=) :: Name n b -> Name n b -> Bool

(Data b, Data n) => Data (Name n b)

Methods

gfoldl :: (forall d a. Data d => c (d -> a) -> d -> c a) -> (forall g. g -> c g) -> Name n b -> c (Name n b)

gunfold :: (forall a r. Data a => c (a -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Name n b)

toConstr :: Name n b -> Constr

dataTypeOf :: Name n b -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Name n b))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Name n b))

gmapT :: (forall a. Data a => a -> a) -> Name n b -> Name n b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name n b -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name n b -> r

gmapQ :: (forall d. Data d => d -> u) -> Name n b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Name n b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name n b -> m (Name n b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name n b -> m (Name n b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name n b -> m (Name n b)

Ord b => Ord (Name n b)

Methods

compare :: Name n b -> Name n b -> Ordering

(<) :: Name n b -> Name n b -> Bool

(<=) :: Name n b -> Name n b -> Bool

(>) :: Name n b -> Name n b -> Bool

(>=) :: Name n b -> Name n b -> Bool

max :: Name n b -> Name n b -> Name n b

min :: Name n b -> Name n b -> Name n b

(Read b, Read n) => Read (Name n b)

Methods

readsPrec :: Int -> ReadS (Name n b)

readList :: ReadS [Name n b]

readPrec :: ReadPrec (Name n b)

readListPrec :: ReadPrec [Name n b]

(Show b, Show n) => Show (Name n b)

Methods

showsPrec :: Int -> Name n b -> ShowS

show :: Name n b -> String

showList :: [Name n b] -> ShowS

Generic (Name n b)

Associated Types

type Rep (Name n b) :: * -> *

Methods

from :: Name n b -> Rep (Name n b) x

to :: Rep (Name n b) x -> Name n b

(Binary b, Binary a) => Binary (Name b a)

Methods

put :: Name b a -> Put

get :: Get (Name b a)

putList :: [Name b a] -> Put

(Serial b, Serial a) => Serial (Name b a)

Methods

serialize :: MonadPut m => Name b a -> m ()

deserialize :: MonadGet m => m (Name b a)

(Serialize b, Serialize a) => Serialize (Name b a)

Methods

put :: Putter (Name b a)

get :: Get (Name b a)

(NFData b, NFData a) => NFData (Name b a)

Methods

rnf :: Name b a -> ()

Hashable a => Hashable (Name n a)

Methods

hashWithSalt :: Int -> Name n a -> Int

hash :: Name n a -> Int

type Rep (Name n b)

type Rep (Name n b) = D1 (MetaData "Name" "Bound.Name" "bound-2-7IewuMnEPFmDtWuvR0VXbb" False) (C1 (MetaCons "Name" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 b))))

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

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

Extract the name.

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

Abstraction, capturing named bound variables.

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

Abstract over a single variable

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

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

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

instantiate1Name = instantiate1