bound-2.0.1: Making de Bruijn Succ Less

Copyright(C) 2012 Edward Kmett
LicenseBSD-style (see the file LICENSE)
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilityportable
Safe HaskellTrustworthy
LanguageHaskell98

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 Source # 
Instance details

Defined in Bound.Name

Methods

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

Bifoldable Name Source # 
Instance details

Defined in Bound.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 #

Bifunctor Name Source # 
Instance details

Defined in Bound.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 #

Eq2 Name Source # 
Instance details

Defined in Bound.Name

Methods

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

Ord2 Name Source # 
Instance details

Defined in Bound.Name

Methods

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

Read2 Name Source # 
Instance details

Defined in Bound.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] #

liftReadPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec (Name a b) #

liftReadListPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec [Name a b] #

Show2 Name Source # 
Instance details

Defined in Bound.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 #

Serial2 Name Source # 
Instance details

Defined in Bound.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 Source # 
Instance details

Defined in Bound.Name

Methods

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

Functor (Name n) Source # 
Instance details

Defined in Bound.Name

Methods

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

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

Foldable (Name n) Source # 
Instance details

Defined in Bound.Name

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) Source # 
Instance details

Defined in Bound.Name

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) Source # 
Instance details

Defined in Bound.Name

Methods

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

Ord1 (Name b) Source # 
Instance details

Defined in Bound.Name

Methods

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

Read b => Read1 (Name b) Source # 
Instance details

Defined in Bound.Name

Methods

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

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

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Name b a) #

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Name b a] #

Show b => Show1 (Name b) Source # 
Instance details

Defined in Bound.Name

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) Source # 
Instance details

Defined in Bound.Name

Methods

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

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

Comonad (Name n) Source # 
Instance details

Defined in Bound.Name

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) Source # 
Instance details

Defined in Bound.Name

Methods

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

Generic1 (Name n :: Type -> Type) Source # 
Instance details

Defined in Bound.Name

Associated Types

type Rep1 (Name n) :: k -> Type #

Methods

from1 :: Name n a -> Rep1 (Name n) a #

to1 :: Rep1 (Name n) a -> Name n a #

Eq b => Eq (Name n b) Source # 
Instance details

Defined in Bound.Name

Methods

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

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

(Data n, Data b) => Data (Name n b) Source # 
Instance details

Defined in Bound.Name

Methods

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

gunfold :: (forall b0 r. Data b0 => c (b0 -> 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 b0. Data b0 => b0 -> b0) -> 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) Source # 
Instance details

Defined in Bound.Name

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 n, Read b) => Read (Name n b) Source # 
Instance details

Defined in Bound.Name

Methods

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

readList :: ReadS [Name n b] #

readPrec :: ReadPrec (Name n b) #

readListPrec :: ReadPrec [Name n b] #

(Show n, Show b) => Show (Name n b) Source # 
Instance details

Defined in Bound.Name

Methods

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

show :: Name n b -> String #

showList :: [Name n b] -> ShowS #

Generic (Name n b) Source # 
Instance details

Defined in Bound.Name

Associated Types

type Rep (Name n b) :: Type -> Type #

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) Source # 
Instance details

Defined in Bound.Name

Methods

put :: Name b a -> Put #

get :: Get (Name b a) #

putList :: [Name b a] -> Put #

(Serial b, Serial a) => Serial (Name b a) Source # 
Instance details

Defined in Bound.Name

Methods

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

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

(Serialize b, Serialize a) => Serialize (Name b a) Source # 
Instance details

Defined in Bound.Name

Methods

put :: Putter (Name b a) #

get :: Get (Name b a) #

(NFData b, NFData a) => NFData (Name b a) Source # 
Instance details

Defined in Bound.Name

Methods

rnf :: Name b a -> () #

Hashable a => Hashable (Name n a) Source # 
Instance details

Defined in Bound.Name

Methods

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

hash :: Name n a -> Int #

type Rep1 (Name n :: Type -> Type) Source # 
Instance details

Defined in Bound.Name

type Rep (Name n b) Source # 
Instance details

Defined in Bound.Name

_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

abstractEitherName :: Monad f => (a -> Either b c) -> f a -> Scope (Name a b) f c Source #

Capture some free variables in an expression to yield a Scope with named bound variables. Optionally change the types of the remaining free variables.

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

instantiateEitherName :: (Monad f, Comonad n) => (Either b a -> f c) -> Scope (n b) f a -> f c Source #