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

Bitraversable Name

Defined in Bound.Name

Methods

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

Bifoldable Name

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

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

Defined in Bound.Name

Methods

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

Ord2 Name

Defined in Bound.Name

Methods

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

Read2 Name

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

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

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

Defined in Bound.Name

Methods

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

Functor (Name n)

Defined in Bound.Name

Methods

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

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

Foldable (Name n)

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)

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)

Defined in Bound.Name

Methods

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

Ord1 (Name b)

Defined in Bound.Name

Methods

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

Read b => Read1 (Name b)

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)

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)

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)

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)

Defined in Bound.Name

Methods

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

Generic1 (Name n :: Type -> Type)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Bound.Name

Methods

put :: Putter (Name b a)

get :: Get (Name b a)

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

Defined in Bound.Name

Methods

rnf :: Name b a -> ()

Hashable a => Hashable (Name n a)

Defined in Bound.Name

Methods

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

hash :: Name n a -> Int

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

Defined in Bound.Name

type Rep1 (Name n :: Type -> Type) = D1 (MetaData "Name" "Bound.Name" "bound-2.0.1-AtZsY3yZaEKLBfeR1JA5NI" False) (C1 (MetaCons "Name" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) Par1))

type Rep (Name n b)

Defined in Bound.Name

type Rep (Name n b) = D1 (MetaData "Name" "Bound.Name" "bound-2.0.1-AtZsY3yZaEKLBfeR1JA5NI" False) (C1 (MetaCons "Name" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n) :*: S1 (MetaSel (Nothing :: Maybe 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

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

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

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

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