Copyright	(c) Murdoch J. Gabbay 2020
License	GPL-3
Maintainer	murdoch.gabbay@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Language.Nominal.Name

Contents

Creating atoms
Atom swapping
Permutations
Names
Name swapping
Nameless types
Tests

Description

The basic framework: a nominal theory of names and swappings

Synopsis

newtype KAtom s = Atom Unique
type Atom = KAtom Tom
data Tom
atTom :: Proxy Tom
freshKAtomsIO :: Traversable m => m a -> IO (m (KAtom s))
freshAtomsIO :: Traversable m => m a -> IO (m Atom)
freshKAtomIO :: IO (KAtom s)
freshAtomIO :: IO Atom
class Swappable a where
- kswp :: Typeable s => KAtom s -> KAtom s -> a -> a
swp :: Swappable a => Atom -> Atom -> a -> a
type KPerm s = [(KAtom s, KAtom s)]
type Perm = KPerm Tom
perm :: (Typeable s, Swappable a) => KPerm s -> a -> a
data KName s t = Name {
- nameLabel :: t
- nameAtom :: KAtom s
}
type Name = KName Tom
withLabel :: KName s t -> t -> KName s t
withLabelOf :: KName s t -> KName s t -> KName s t
justALabel :: t -> KName s t
justAnAtom :: KAtom s -> KName s t
kswpN :: (Typeable s, Swappable a) => KName s t -> KName s t -> a -> a
swpN :: Swappable a => Name t -> Name t -> a -> a
newtype Nameless a = Nameless {
- getNameless :: a
}

Documentation

newtype KAtom s Source #

An atom is a unique atomic token.

The argument s of KAtom is part of facilities offered by this package for declaring types of atom s ranging over kinds k. For usage see ATyp, and ATrm in Language.Nominal.Examples.SystemF.

If your development requires just a single type of atomic tokens, ignore KAtom and use KAtom.

Constructors

Atom Unique

Instances

(Typeable s, Typeable t) => KSupport s (KAtom t) Source #
Instance details Defined in Language.Nominal.NameSet Methods ksupp :: proxy s -> KAtom t -> Set (KAtom s) Source #
(Typeable s, Typeable t) => KUnifyPerm s (KAtom t) Source #	Unify atoms
Instance details Defined in Language.Nominal.Unify Methods kunifyPerm :: proxy s -> KAtom t -> KAtom t -> KRen s Source # ren :: KRen s -> KAtom t -> KAtom t Source #
Eq (KAtom s) Source #
Instance details Defined in Language.Nominal.Name Methods (==) :: KAtom s -> KAtom s -> Bool # (/=) :: KAtom s -> KAtom s -> Bool #
Data s => Data (KAtom s) Source #
Instance details Defined in Language.Nominal.Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KAtom s -> c (KAtom s) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (KAtom s) # toConstr :: KAtom s -> Constr # dataTypeOf :: KAtom s -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (KAtom s)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (KAtom s)) # gmapT :: (forall b. Data b => b -> b) -> KAtom s -> KAtom s # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KAtom s -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KAtom s -> r # gmapQ :: (forall d. Data d => d -> u) -> KAtom s -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> KAtom s -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> KAtom s -> m (KAtom s) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KAtom s -> m (KAtom s) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KAtom s -> m (KAtom s) #
Ord (KAtom s) Source #
Instance details Defined in Language.Nominal.Name Methods compare :: KAtom s -> KAtom s -> Ordering # (<) :: KAtom s -> KAtom s -> Bool # (<=) :: KAtom s -> KAtom s -> Bool # (>) :: KAtom s -> KAtom s -> Bool # (>=) :: KAtom s -> KAtom s -> Bool # max :: KAtom s -> KAtom s -> KAtom s # min :: KAtom s -> KAtom s -> KAtom s #
Show (KAtom s) Source #	Display an atom by showing (the hash of) its unique id.
Instance details Defined in Language.Nominal.Name Methods showsPrec :: Int -> KAtom s -> ShowS # show :: KAtom s -> String # showList :: [KAtom s] -> ShowS #
Generic (KAtom s) Source #
Instance details Defined in Language.Nominal.Name Associated Types type Rep (KAtom s) :: Type -> Type # Methods from :: KAtom s -> Rep (KAtom s) x # to :: Rep (KAtom s) x -> KAtom s #
Arbitrary (KAtom s) Source #	Pick an atom
Instance details Defined in Language.Nominal.Properties.SpecUtilities Methods arbitrary :: Gen (KAtom s) # shrink :: KAtom s -> [KAtom s] #
Typeable s => Swappable (KAtom s) Source #	Base case for swapping: atoms acting on atoms.
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KAtom s -> KAtom s Source #
SMonad [KAtom s] (KNom s) Source #
Instance details Defined in Language.Nominal.Nom Methods (>>+) :: KNom s a -> ([KAtom s] -> a -> KNom s b) -> KNom s b Source # enter :: [KAtom s] -> a -> KNom s a Source # exit :: KNom s a -> a Source #
(Typeable s, Swappable a) => Binder (KNom s a) [KAtom s] a s Source #	Acts on a `KNom` binder by applying a function to the body and the context of locally bound names. Local names are preserved.
Instance details Defined in Language.Nominal.Binder Methods (@@) :: KNom s a -> ([KAtom s] -> a -> b) -> KNom s b Source # (@>) :: [KAtom s] -> a -> KNom s a Source # resMay :: [KAtom s] -> a -> Maybe (KNom s a) Source #
(Typeable s, Swappable a, KRestrict s a) => BinderConc (KNom s a) [KAtom s] a s () Source #	Suppose we have a nominal abstraction `x' :: KNom s a` where `a` has its own internal notion of name restriction. Then `cnoc () x'` folds the `KNom`-bound names down into `x'` to return a concrete element of `a`. cnoc () = unNom
Instance details Defined in Language.Nominal.Binder Methods conc :: KNom s a -> () -> a Source # cnoc :: () -> KNom s a -> a Source #
(Typeable s, Swappable a) => BinderConc (KNom s a) [KAtom s] a s [KAtom s] Source #	Concrete a nominal abstraction at a particular list of atoms. Dangerous for two reasons: The list needs to be long enough. There are no guarantees about the order the bound atoms come out in.
Instance details Defined in Language.Nominal.Binder Methods conc :: KNom s a -> [KAtom s] -> a Source # cnoc :: [KAtom s] -> KNom s a -> a Source #
(Typeable s, Swappable a) => BinderConc (KNom s a) [KAtom s] a s (Proxy s) Source #	Suppose we have a nominal abstraction `x' :: KNom s a`. Then `x' conc (Proxy :: Proxy s)` triggers an IO action to strip the `KNom` context and concrete `x'` at some choice of fresh atoms. cnoc (Proxy :: Proxy s) = exit
Instance details Defined in Language.Nominal.Binder Methods conc :: KNom s a -> Proxy s -> a Source # cnoc :: Proxy s -> KNom s a -> a Source #
Validator r d v => Binder (Chunk r d v) [Atom] [Transaction r d v] Tom Source #	Acts on a `Chunk` by unpacking it as a transaction-list and a list of locally bound atoms, and applying a function.
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods (@@) :: Chunk r d v -> ([Atom] -> [Transaction r d v] -> b) -> KNom Tom b Source # (@>) :: [Atom] -> [Transaction r d v] -> Chunk r d v Source # resMay :: [Atom] -> [Transaction r d v] -> Maybe (Chunk r d v) Source #
type Rep (KAtom s) Source #
Instance details Defined in Language.Nominal.Name type Rep (KAtom s) = D1 (MetaData "KAtom" "Language.Nominal.Name" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" True) (C1 (MetaCons "Atom" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Unique)))

type Atom = KAtom Tom Source #

A distinguished type of atoms.

It is populated by Toms (below), thus an element of KAtom is "a Tom".

We provide KAtom as primitive for convenience. If you need more than one type of atom (e.g. term atoms and type atoms), look at KAtom.

data Tom Source #

We provide a stock datatype Tom.

Using the DataKinds package, this is then used to provide a stock type of atoms KAtom.

Instances

Eq Tom Source #
Instance details Defined in Language.Nominal.Name Methods (==) :: Tom -> Tom -> Bool # (/=) :: Tom -> Tom -> Bool #
Data Tom Source #
Instance details Defined in Language.Nominal.Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Tom -> c Tom # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Tom # toConstr :: Tom -> Constr # dataTypeOf :: Tom -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Tom) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Tom) # gmapT :: (forall b. Data b => b -> b) -> Tom -> Tom # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tom -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tom -> r # gmapQ :: (forall d. Data d => d -> u) -> Tom -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Tom -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Tom -> m Tom # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Tom -> m Tom # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Tom -> m Tom #
Ord Tom Source #
Instance details Defined in Language.Nominal.Name Methods compare :: Tom -> Tom -> Ordering # (<) :: Tom -> Tom -> Bool # (<=) :: Tom -> Tom -> Bool # (>) :: Tom -> Tom -> Bool # (>=) :: Tom -> Tom -> Bool # max :: Tom -> Tom -> Tom # min :: Tom -> Tom -> Tom #
Generic Tom Source #
Instance details Defined in Language.Nominal.Name Associated Types type Rep Tom :: Type -> Type # Methods from :: Tom -> Rep Tom x # to :: Rep Tom x -> Tom #
KSub Var Exp Exp Source #	Substitution. Capture-avoidance is automatic.
Instance details Defined in Language.Nominal.Examples.UntypedLambda Methods sub :: Var -> Exp -> Exp -> Exp Source #
KSub V Operand Prog Source #	Substitution on `Prog`rams is generic
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Prog -> Prog Source #
KSub V Operand Operand Source #	Substitution as standard on `Operand`
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Operand -> Operand Source #
KSub V Operand Prog Source #	Substitution on `Prog`rams is generic
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods sub :: V -> Operand -> Prog -> Prog Source #
KSub V Operand Operand Source #	Substitution as standard on `Operand`
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods sub :: V -> Operand -> Operand -> Operand Source #
Support r => KSupport Tom (Input r) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> Input r -> Set (KAtom Tom) Source #
UnifyPerm r => KUnifyPerm Tom (Input r) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kunifyPerm :: proxy Tom -> Input r -> Input r -> KRen Tom Source # ren :: KRen Tom -> Input r -> Input r Source #
KRestrict Tom (ValFin r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods restrict :: [KAtom Tom] -> ValFin r d -> ValFin r d Source #
KRestrict Tom (Val r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods restrict :: [KAtom Tom] -> Val r d -> Val r d Source #
KSupport Tom (ValFin r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> ValFin r d -> Set (KAtom Tom) Source #
KSupport Tom (Val r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> Val r d -> Set (KAtom Tom) Source #
KSupport Tom (ValTriv r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> ValTriv r d -> Set (KAtom Tom) Source #
(Support d, Support v) => KSupport Tom (Output d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> Output d v -> Set (KAtom Tom) Source #
(UnifyPerm r, UnifyPerm d) => KUnifyPerm Tom (ValFin r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kunifyPerm :: proxy Tom -> ValFin r d -> ValFin r d -> KRen Tom Source # ren :: KRen Tom -> ValFin r d -> ValFin r d Source #
KUnifyPerm Tom (ValTriv r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kunifyPerm :: proxy Tom -> ValTriv r d -> ValTriv r d -> KRen Tom Source # ren :: KRen Tom -> ValTriv r d -> ValTriv r d Source #
(UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Output d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kunifyPerm :: proxy Tom -> Output d v -> Output d v -> KRen Tom Source # ren :: KRen Tom -> Output d v -> Output d v Source #
(Swappable r, Swappable d, Swappable v) => KRestrict Tom (Chunk r d v) Source #	Restrict atoms in a `Chunk`.
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods restrict :: [KAtom Tom] -> Chunk r d v -> Chunk r d v Source #
(Support r, Support d, Support v) => KSupport Tom (Blockchain r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> Blockchain r d v -> Set (KAtom Tom) Source #
(Support r, Support d, Support v) => KSupport Tom (Chunk r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> Chunk r d v -> Set (KAtom Tom) Source #
(Support d, Support r, Support v) => KSupport Tom (Context r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> Context r d v -> Set (KAtom Tom) Source #
(Support d, Support r, Support v) => KSupport Tom (Transaction r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods ksupp :: proxy Tom -> Transaction r d v -> Set (KAtom Tom) Source #
(UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Blockchain r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kunifyPerm :: proxy Tom -> Blockchain r d v -> Blockchain r d v -> KRen Tom Source # ren :: KRen Tom -> Blockchain r d v -> Blockchain r d v Source #
(UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Chunk r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kunifyPerm :: proxy Tom -> Chunk r d v -> Chunk r d v -> KRen Tom Source # ren :: KRen Tom -> Chunk r d v -> Chunk r d v Source #
(UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Context r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kunifyPerm :: proxy Tom -> Context r d v -> Context r d v -> KRen Tom Source # ren :: KRen Tom -> Context r d v -> Context r d v Source #
(UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Transaction r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kunifyPerm :: proxy Tom -> Transaction r d v -> Transaction r d v -> KRen Tom Source # ren :: KRen Tom -> Transaction r d v -> Transaction r d v Source #
Arbitrary (Name String) Source #
Instance details Defined in Language.Nominal.Properties.SpecUtilities Methods arbitrary :: Gen (Name String) # shrink :: Name String -> [Name String] #
(Swappable a, HasOutputPositions a) => HasOutputPositions (Nom a) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods outputPositions :: Nom a -> [Position] Source #
(Arbitrary a, UnifyPerm a, Eq a, Arbitrary b, Eq b) => Arbitrary (EvFinMap a b) Source #
Instance details Defined in Language.Nominal.Properties.SpecUtilities Methods arbitrary :: Gen (EvFinMap a b) # shrink :: EvFinMap a b -> [EvFinMap a b] #
Validator r d v => Binder (Chunk r d v) [Atom] [Transaction r d v] Tom Source #	Acts on a `Chunk` by unpacking it as a transaction-list and a list of locally bound atoms, and applying a function.
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods (@@) :: Chunk r d v -> ([Atom] -> [Transaction r d v] -> b) -> KNom Tom b Source # (@>) :: [Atom] -> [Transaction r d v] -> Chunk r d v Source # resMay :: [Atom] -> [Transaction r d v] -> Maybe (Chunk r d v) Source #
type Rep Tom Source #
Instance details Defined in Language.Nominal.Name type Rep Tom = D1 (MetaData "Tom" "Language.Nominal.Name" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" False) (V1 :: Type -> Type)

atTom :: Proxy Tom Source #

A proxy element for sort Tom. If we pass this, we tell the typechecker we are "at Tom".

Creating atoms

freshKAtomsIO :: Traversable m => m a -> IO (m (KAtom s)) Source #

Make a fresh atom for each element of some list (any list). If you just want one fresh atom, use e.g. [()].

This is an IO action; when executed, fresh identifiers get generated.

freshAtomsIO :: Traversable m => m a -> IO (m Atom) Source #

Make a fresh atom at Tom for each element of some list (any list).

freshKAtomIO :: IO (KAtom s) Source #

For convenience: generate a fresh katom

freshAtomIO :: IO Atom Source #

For convenience: generate a fresh atom

>>> a <- freshAtomIO
>>> b <- freshAtomIO
>>> a == b
False

Atom swapping

class Swappable a where Source #

Types that admit a swapping action.

A swapping (a b) maps

a to b and
b to a and
any other c to c.

Swappings are invertible, which allows them to commute through type-formers containing negative arities, e.g. the left-hand argument of function arrow. Swappings always distribute:

swp a b (x, y)       == (swp a b x, swp a b y)
swp a b [x1, x2, x3] == [swp a b x1, swp a b x2, swp a b x3] 
swp a b (f x)        == (swp a b f) (swp a b x)
swp a b (abst n x)   == abst (swp a b n) (swp a b x)
swp a b (res [n] x)  == res [swp a b n] (swp a b x)
swp a b (Name t x)   == Name (swp a b t) (swp a b x)

Technical note: The content of Swappable a is that a supports a swapping action by atoms of every s. Everything else, e.g. KSupport, just uses s. So k is a "world" of sorts of atoms, for a particular application. This is invisible at our default world Tom because Tom has only one inhabitant, 'Tom. See ASort and surrounding code for a more sophisticated atoms setup.

Minimal complete definition

Nothing

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> a -> a Source #

kswp :: (Typeable s, Generic a, GSwappable (Rep a)) => KAtom s -> KAtom s -> a -> a Source #

Instances

Swappable Bool Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Bool -> Bool Source #
Swappable Char Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Char -> Char Source #
Swappable Int Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Int -> Int Source #
Swappable () Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> () -> () Source #
Swappable Exp Source #
Instance details Defined in Language.Nominal.Examples.UntypedLambda Methods kswp :: Typeable s => KAtom s -> KAtom s -> Exp -> Exp Source #
Swappable Trm Source #
Instance details Defined in Language.Nominal.Examples.SystemF Methods kswp :: Typeable s => KAtom s -> KAtom s -> Trm -> Trm Source #
Swappable Typ Source #
Instance details Defined in Language.Nominal.Examples.SystemF Methods kswp :: Typeable s => KAtom s -> KAtom s -> Typ -> Typ Source #
Swappable Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods kswp :: Typeable s => KAtom s -> KAtom s -> Prog -> Prog Source #
Swappable Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods kswp :: Typeable s => KAtom s -> KAtom s -> Operand -> Operand Source #
Swappable Prog Source #
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods kswp :: Typeable s => KAtom s -> KAtom s -> Prog -> Prog Source #
Swappable Operand Source #
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods kswp :: Typeable s => KAtom s -> KAtom s -> Operand -> Operand Source #
Swappable a => Swappable [a] Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> [a] -> [a] Source #
Swappable a => Swappable (Maybe a) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Maybe a -> Maybe a Source #
Swappable a => Swappable (NonEmpty a) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> NonEmpty a -> NonEmpty a Source #
(Ord a, Swappable a) => Swappable (Set a) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Set a -> Set a Source #
Swappable (Nameless a) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Nameless a -> Nameless a Source #
Typeable s => Swappable (KAtom s) Source #	Base case for swapping: atoms acting on atoms.
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KAtom s -> KAtom s Source #
Swappable a => Swappable (BinderSupp a) Source #
Instance details Defined in Language.Nominal.Binder Methods kswp :: Typeable s => KAtom s -> KAtom s -> BinderSupp a -> BinderSupp a Source #
Typeable s => Swappable (KRen s) Source #
Instance details Defined in Language.Nominal.Unify Methods kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KRen s -> KRen s Source #
Swappable r => Swappable (Input r) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> Input r -> Input r Source #
(Swappable a, Swappable b) => Swappable (a -> b) Source #	Swap distributes over function types, because functions inherit swapping action pointwise (also called the conjugation action)
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> (a -> b) -> a -> b Source #
(Swappable a, Swappable b) => Swappable (Either a b) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Either a b -> Either a b Source #
(Swappable a, Swappable b) => Swappable (a, b) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> (a, b) -> (a, b) Source #
(Swappable a, Swappable b, Ord a) => Swappable (Map a b) Source #	Swap distributes over map types. Note that maps store their keys ordered for quick lookup, so a swapping acting on a map is not a noop and can provoke reorderings.
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Map a b -> Map a b Source #
(Typeable s, Swappable t) => Swappable (KName s t) Source #	Swapping atoms in names distributes normally; so we swap in the semantic label and also in the name's atom identifier. Operationally, it's just a tuple action: swp atm1 atm2 (Name t atm) = Name (swp atm1 atm2 t) (swp atm1 atm2 atm)
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KName s t -> KName s t Source #
(Swappable i, Swappable a) => Swappable (XSuspend i a) Source #
Instance details Defined in Language.Nominal.SMonad Methods kswp :: Typeable s => KAtom s -> KAtom s -> XSuspend i a -> XSuspend i a Source #
(Typeable s, Swappable a) => Swappable (KNom s a) Source #	Swap goes under name-binders. swp n1 n2 (ns @> x) = (swp n1 n2 ns) @> (swp n1 n2 x)
Instance details Defined in Language.Nominal.Nom Methods kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KNom s a -> KNom s a Source #
(Swappable n, Swappable a) => Swappable (KAbs n a) Source #	Spelling out the generic swapping action for clarity, where we write `KA` for the (internal) constructor for `KAbs`: `kswp n1 n2 (KA n f) = KA (kswp n1 n2 n) (kswp n1 n2 f)`
Instance details Defined in Language.Nominal.Abs Methods kswp :: Typeable s => KAtom s -> KAtom s -> KAbs n a -> KAbs n a Source #
Swappable (ValFin r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> ValFin r d -> ValFin r d Source #
Swappable (Val r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> Val r d -> Val r d Source #
Swappable (ValTriv r d) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> ValTriv r d -> ValTriv r d Source #
(Swappable d, Swappable v) => Swappable (Output d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> Output d v -> Output d v Source #
(Swappable a, Swappable b, Swappable c) => Swappable (a, b, c) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> (a, b, c) -> (a, b, c) Source #
Swappable a => Swappable (KEvFinMap s a b) Source #
Instance details Defined in Language.Nominal.Equivar Methods kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KEvFinMap s a b -> KEvFinMap s a b Source #
(Typeable s, Swappable a, Swappable b) => Swappable (KEvFun s a b) Source #
Instance details Defined in Language.Nominal.Equivar Methods kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KEvFun s a b -> KEvFun s a b Source #
(Swappable r, Swappable d, Swappable v) => Swappable (Blockchain r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> Blockchain r d v -> Blockchain r d v Source #
(Swappable r, Swappable d, Swappable v) => Swappable (Chunk r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> Chunk r d v -> Chunk r d v Source #
(Swappable r, Swappable d, Swappable v) => Swappable (Context r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> Context r d v -> Context r d v Source #
(Swappable r, Swappable d, Swappable v) => Swappable (Transaction r d v) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods kswp :: Typeable s => KAtom s -> KAtom s -> Transaction r d v -> Transaction r d v Source #
(Swappable a, Swappable b, Swappable c, Swappable d) => Swappable (a, b, c, d) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> (a, b, c, d) -> (a, b, c, d) Source #
(Swappable a, Swappable b, Swappable c, Swappable d, Swappable e) => Swappable (a, b, c, d, e) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> (a, b, c, d, e) -> (a, b, c, d, e) Source #

swp :: Swappable a => Atom -> Atom -> a -> a Source #

A Tom-swapping

Permutations

type KPerm s = [(KAtom s, KAtom s)] Source #

A permutation represented as a list of swappings (simple but inefficient).

type Perm = KPerm Tom Source #

A permutation at Tom.

perm :: (Typeable s, Swappable a) => KPerm s -> a -> a Source #

A permutation acts as a list of swappings. Rightmost/innermost swapping acts first.

>>> a <- freshAtomIO
>>> b <- freshAtomIO
>>> c <- freshAtomIO
>>> perm [(c,b), (b,a)] a == c
True

Names

data KName s t Source #

A name is a pair of

an atom, and
a label t.

t is intended to store semantic information about the atom. For instance, if implementing a simply-typed lambda-calculus then t might be a dataype of (object-level) types.

A similar effect could be achieved by maintaining a monadic lookup context relating atoms to their semantic information; the advantage of using a name is that this information is packaged up with the atom in a local datum of type KName.

Constructors

Name
Fields nameLabel :: t nameAtom :: KAtom s

Instances

PP NTrm Source #	Pretty-print term variable
Instance details Defined in Language.Nominal.Examples.SystemF Methods ppp :: NTrm -> String Source # pp :: NTrm -> IO () Source #
PP NTyp Source #	Pretty-print type variable
Instance details Defined in Language.Nominal.Examples.SystemF Methods ppp :: NTyp -> String Source # pp :: NTyp -> IO () Source #
KSub Var Exp Exp Source #	Substitution. Capture-avoidance is automatic.
Instance details Defined in Language.Nominal.Examples.UntypedLambda Methods sub :: Var -> Exp -> Exp -> Exp Source #
KSub NTrm Trm Trm Source #	Substitute term variable with term in term
Instance details Defined in Language.Nominal.Examples.SystemF Methods sub :: NTrm -> Trm -> Trm -> Trm Source #
KSub NTyp Typ Trm Source #
Instance details Defined in Language.Nominal.Examples.SystemF Methods sub :: NTyp -> Typ -> Trm -> Trm Source #
KSub NTyp Typ NTrm Source #	Substitute type variables with type in term variable. Non-trivial because a term variable carries a label which contains a type. Action is functorial, descending into the type label.
Instance details Defined in Language.Nominal.Examples.SystemF Methods sub :: NTyp -> Typ -> NTrm -> NTrm Source #
KSub NTyp Typ Typ Source #	Substitution acts on type variables. Capture-avoidance is automagical.
Instance details Defined in Language.Nominal.Examples.SystemF Methods sub :: NTyp -> Typ -> Typ -> Typ Source #
KSub V Operand Prog Source #	Substitution on `Prog`rams is generic
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Prog -> Prog Source #
KSub V Operand Operand Source #	Substitution as standard on `Operand`
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Operand -> Operand Source #
KSub V Operand Prog Source #	Substitution on `Prog`rams is generic
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods sub :: V -> Operand -> Prog -> Prog Source #
KSub V Operand Operand Source #	Substitution as standard on `Operand`
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods sub :: V -> Operand -> Operand -> Operand Source #
(Typeable s, Typeable u, KSupport s t) => KSupport s (KName u t) Source #
Instance details Defined in Language.Nominal.NameSet Methods ksupp :: proxy s -> KName u t -> Set (KAtom s) Source #
(KSupport s a, KSupport s t) => KSupport s (KAbs (KName s t) a) Source #	Support of a :@> x is the support of x minus a
Instance details Defined in Language.Nominal.Abs Methods ksupp :: proxy s -> KAbs (KName s t) a -> Set (KAtom s) Source #
(Typeable s, KUnifyPerm s t, KUnifyPerm s a) => KUnifyPerm s (KAbs (KName s t) a) Source #	Unify `Abs` name-abstraction
Instance details Defined in Language.Nominal.Unify Methods kunifyPerm :: proxy s -> KAbs (KName s t) a -> KAbs (KName s t) a -> KRen s Source # ren :: KRen s -> KAbs (KName s t) a -> KAbs (KName s t) a Source #
(Typeable s, Typeable u, KUnifyPerm s t) => KUnifyPerm s (KName u t) Source #	Unify names: they behave just an atom-label tuple
Instance details Defined in Language.Nominal.Unify Methods kunifyPerm :: proxy s -> KName u t -> KName u t -> KRen s Source # ren :: KRen s -> KName u t -> KName u t Source #
Functor (KName s) Source #
Instance details Defined in Language.Nominal.Name Methods fmap :: (a -> b) -> KName s a -> KName s b # (<$) :: a -> KName s b -> KName s a #
Default t => Applicative (KAbs (KName s t)) Source #
Instance details Defined in Language.Nominal.Abs Methods pure :: a -> KAbs (KName s t) a # (<>) :: KAbs (KName s t) (a -> b) -> KAbs (KName s t) a -> KAbs (KName s t) b # liftA2 :: (a -> b -> c) -> KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) c # (>) :: KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) b # (<*) :: KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) a #
Foldable (KName s) Source #
Instance details Defined in Language.Nominal.Name Methods fold :: Monoid m => KName s m -> m # foldMap :: Monoid m => (a -> m) -> KName s a -> m # foldr :: (a -> b -> b) -> b -> KName s a -> b # foldr' :: (a -> b -> b) -> b -> KName s a -> b # foldl :: (b -> a -> b) -> b -> KName s a -> b # foldl' :: (b -> a -> b) -> b -> KName s a -> b # foldr1 :: (a -> a -> a) -> KName s a -> a # foldl1 :: (a -> a -> a) -> KName s a -> a # toList :: KName s a -> [a] # null :: KName s a -> Bool # length :: KName s a -> Int # elem :: Eq a => a -> KName s a -> Bool # maximum :: Ord a => KName s a -> a # minimum :: Ord a => KName s a -> a # sum :: Num a => KName s a -> a # product :: Num a => KName s a -> a #
Traversable (KName s) Source #
Instance details Defined in Language.Nominal.Name Methods traverse :: Applicative f => (a -> f b) -> KName s a -> f (KName s b) # sequenceA :: Applicative f => KName s (f a) -> f (KName s a) # mapM :: Monad m => (a -> m b) -> KName s a -> m (KName s b) # sequence :: Monad m => KName s (m a) -> m (KName s a) #
Arbitrary (Name String) Source #
Instance details Defined in Language.Nominal.Properties.SpecUtilities Methods arbitrary :: Gen (Name String) # shrink :: Name String -> [Name String] #
Eq (KName s t) Source #	Names are equal when they refer to the same atom. WARNING: Labels are not considered! In particular, `t`-names always have `Eq`, even if the type of labels `t` does not.
Instance details Defined in Language.Nominal.Name Methods (==) :: KName s t -> KName s t -> Bool # (/=) :: KName s t -> KName s t -> Bool #
(Typeable s, Swappable t, Eq t, Eq a) => Eq (KAbs (KName s t) a) Source #	Abstractions are equal up to fusing their abstracted names.
Instance details Defined in Language.Nominal.Abs Methods (==) :: KAbs (KName s t) a -> KAbs (KName s t) a -> Bool # (/=) :: KAbs (KName s t) a -> KAbs (KName s t) a -> Bool #
(Data s, Data t) => Data (KName s t) Source #
Instance details Defined in Language.Nominal.Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KName s t -> c (KName s t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (KName s t) # toConstr :: KName s t -> Constr # dataTypeOf :: KName s t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (KName s t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (KName s t)) # gmapT :: (forall b. Data b => b -> b) -> KName s t -> KName s t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KName s t -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KName s t -> r # gmapQ :: (forall d. Data d => d -> u) -> KName s t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> KName s t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> KName s t -> m (KName s t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KName s t -> m (KName s t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KName s t -> m (KName s t) #
Ord (KName s t) Source #	Names are leq when their atoms are leq. WARNING: Labels are not considered! In particular, `t`-names are always ordered even if labels `t` are unordered.
Instance details Defined in Language.Nominal.Name Methods compare :: KName s t -> KName s t -> Ordering # (<) :: KName s t -> KName s t -> Bool # (<=) :: KName s t -> KName s t -> Bool # (>) :: KName s t -> KName s t -> Bool # (>=) :: KName s t -> KName s t -> Bool # max :: KName s t -> KName s t -> KName s t # min :: KName s t -> KName s t -> KName s t #
Show (KName s ()) Source #
Instance details Defined in Language.Nominal.Name Methods showsPrec :: Int -> KName s () -> ShowS # show :: KName s () -> String # showList :: [KName s ()] -> ShowS #
Show t => Show (KName s t) Source #
Instance details Defined in Language.Nominal.Name Methods showsPrec :: Int -> KName s t -> ShowS # show :: KName s t -> String # showList :: [KName s t] -> ShowS #
(Typeable s, Swappable t, Swappable a, Show t, Show a) => Show (KAbs (KName s t) a) Source #	We show an abstraction by evaluating the function inside `Abs` on a fresh name (with the default `Nothing` label)
Instance details Defined in Language.Nominal.Abs Methods showsPrec :: Int -> KAbs (KName s t) a -> ShowS # show :: KAbs (KName s t) a -> String # showList :: [KAbs (KName s t) a] -> ShowS #
Generic (KName s t) Source #
Instance details Defined in Language.Nominal.Name Associated Types type Rep (KName s t) :: Type -> Type # Methods from :: KName s t -> Rep (KName s t) x # to :: Rep (KName s t) x -> KName s t #
Arbitrary a => Arbitrary (KName s a) Source #
Instance details Defined in Language.Nominal.Properties.SpecUtilities Methods arbitrary :: Gen (KName s a) # shrink :: KName s a -> [KName s a] #
(Typeable s, Swappable t, Swappable a, Arbitrary (KName s t), Arbitrary a) => Arbitrary (KAbs (KName s t) a) Source #
Instance details Defined in Language.Nominal.Properties.SpecUtilities Methods arbitrary :: Gen (KAbs (KName s t) a) # shrink :: KAbs (KName s t) a -> [KAbs (KName s t) a] #
(Typeable s, Swappable t) => Swappable (KName s t) Source #	Swapping atoms in names distributes normally; so we swap in the semantic label and also in the name's atom identifier. Operationally, it's just a tuple action: swp atm1 atm2 (Name t atm) = Name (swp atm1 atm2 t) (swp atm1 atm2 atm)
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KName s t -> KName s t Source #
(Typeable s, Typeable u, KSub (KName s n) x t, KSub (KName s n) x y, Swappable t, Swappable y) => KSub (KName s n) x (KAbs (KName u t) y) Source #	sub on a nominal abstraction substitutes in the label, and substitutes capture-avoidingly in the body
Instance details Defined in Language.Nominal.Sub Methods sub :: KName s n -> x -> KAbs (KName u t) y -> KAbs (KName u t) y Source #
(Typeable s, Swappable t, Swappable a) => Binder (KAbs (KName s t) a) (KName s t) a s Source #	Acts on an abstraction `x'` by unpacking `x'` as `(n,x)` for a fresh name `n`, and calculating `f n x`.
Instance details Defined in Language.Nominal.Abs Methods (@@) :: KAbs (KName s t) a -> (KName s t -> a -> b) -> KNom s b Source # (@>) :: KName s t -> a -> KAbs (KName s t) a Source # resMay :: KName s t -> a -> Maybe (KAbs (KName s t) a) Source #
(Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => BinderConc (KAbs (KName s n) y) (KName s n) y s x Source #	Nameless form of substitution, where the name for which we substitute is packaged in a `KAbs` abstraction.
Instance details Defined in Language.Nominal.Sub Methods conc :: KAbs (KName s n) y -> x -> y Source # cnoc :: x -> KAbs (KName s n) y -> y Source #
KSub (KName s n) (KName s n) (KName s n) Source #	sub on names
Instance details Defined in Language.Nominal.Sub Methods sub :: KName s n -> KName s n -> KName s n -> KName s n Source #
type Rep (KName s t) Source #
Instance details Defined in Language.Nominal.Name type Rep (KName s t) = D1 (MetaData "KName" "Language.Nominal.Name" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" False) (C1 (MetaCons "Name" PrefixI True) (S1 (MetaSel (Just "nameLabel") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 t) :*: S1 (MetaSel (Just "nameAtom") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (KAtom s))))

type Name = KName Tom Source #

A Tom instance of KName.

withLabel :: KName s t -> t -> KName s t Source #

As the name suggests: overwrite the name's label

withLabelOf :: KName s t -> KName s t -> KName s t Source #

Overwrite the name's label. Intended to be read infix as n `withLabelOf n'

justALabel :: t -> KName s t Source #

Name with undefined atom, so really just a label. Use with care!

justAnAtom :: KAtom s -> KName s t Source #

Name with undefined label, so really just an atom. Use with care!

Name swapping

kswpN :: (Typeable s, Swappable a) => KName s t -> KName s t -> a -> a Source #

A name swap discards the names' labels and calls the atom-swap kswp.

swpN :: Swappable a => Name t -> Name t -> a -> a Source #

A name swap for a Tom-name. Discards the names' labels and calls a Tom-atom swapping.

Nameless types

newtype Nameless a Source #

Some types, like Bool and String, are Nameless. E.g. if we have a truth-value, we know it doesn't have any names in it; we might have used names to calculate the truth-value, but the truth-value itself True or False is nameless.

Constructors

Nameless
Fields getNameless :: a

Instances

KSub n x (Nameless a) Source #	sub on nameless type is trivial
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> Nameless a -> Nameless a Source #
Typeable s => KRestrict s (Nameless a) Source #	Restriction is trivial on elements of nameless types
Instance details Defined in Language.Nominal.NameSet Methods restrict :: [KAtom s] -> Nameless a -> Nameless a Source #
Typeable s => KSupport s (Nameless a) Source #
Instance details Defined in Language.Nominal.NameSet Methods ksupp :: proxy s -> Nameless a -> Set (KAtom s) Source #
(Typeable s, Eq a) => KUnifyPerm s (Nameless a) Source #
Instance details Defined in Language.Nominal.Unify Methods kunifyPerm :: proxy s -> Nameless a -> Nameless a -> KRen s Source # ren :: KRen s -> Nameless a -> Nameless a Source #
Eq a => Eq (Nameless a) Source #
Instance details Defined in Language.Nominal.Name Methods (==) :: Nameless a -> Nameless a -> Bool # (/=) :: Nameless a -> Nameless a -> Bool #
Ord a => Ord (Nameless a) Source #
Instance details Defined in Language.Nominal.Name Methods compare :: Nameless a -> Nameless a -> Ordering # (<) :: Nameless a -> Nameless a -> Bool # (<=) :: Nameless a -> Nameless a -> Bool # (>) :: Nameless a -> Nameless a -> Bool # (>=) :: Nameless a -> Nameless a -> Bool # max :: Nameless a -> Nameless a -> Nameless a # min :: Nameless a -> Nameless a -> Nameless a #
Read a => Read (Nameless a) Source #
Instance details Defined in Language.Nominal.Name Methods readsPrec :: Int -> ReadS (Nameless a) # readList :: ReadS [Nameless a] # readPrec :: ReadPrec (Nameless a) # readListPrec :: ReadPrec [Nameless a] #
Show a => Show (Nameless a) Source #
Instance details Defined in Language.Nominal.Name Methods showsPrec :: Int -> Nameless a -> ShowS # show :: Nameless a -> String # showList :: [Nameless a] -> ShowS #
Swappable (Nameless a) Source #
Instance details Defined in Language.Nominal.Name Methods kswp :: Typeable s => KAtom s -> KAtom s -> Nameless a -> Nameless a Source #

Tests

Property-based tests are in Language.Nominal.Properties.NameSpec.