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

Eq2 Name Source # 

Methods

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

Ord2 Name Source # 

Methods

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

Read2 Name Source # 

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

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

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

Methods

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

Bifoldable Name Source # 

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

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 # 

Methods

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

Functor (Name n) Source # 

Methods

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

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

Foldable (Name n) Source # 

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 # 

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) #

Generic1 (Name n) Source # 

Associated Types

type Rep1 (Name n :: * -> *) :: * -> * #

Methods

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

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

Eq1 (Name b) Source # 

Methods

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

Ord1 (Name b) Source # 

Methods

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

Read b => Read1 (Name b) Source # 

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

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 # 

Methods

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

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

Comonad (Name n) Source # 

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 # 

Methods

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

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

Methods

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

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

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

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

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

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

Methods

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

show :: Name n b -> String #

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

Generic (Name n b) Source # 

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

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 # 

Methods

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

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

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

Methods

put :: Putter (Name b a) #

get :: Get (Name b a) #

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

Methods

rnf :: Name b a -> () #

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

Methods

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

hash :: Name n a -> Int #

type Rep1 (Name n) Source # 
type Rep (Name n b) Source # 

_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 #