Language.Nominal.Name

The basic framework: a nominal theory of names and swappings

Documentation

newtype KAtom s

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)

Defined in Language.Nominal.NameSet

Methods

ksupp :: proxy s -> KAtom t -> Set (KAtom s)

(Typeable s, Typeable t) => KUnifyPerm s (KAtom t)

Unify atoms

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> KAtom t -> KAtom t -> KRen s

ren :: KRen s -> KAtom t -> KAtom t

Eq (KAtom s)

Defined in Language.Nominal.Name

Methods

(==) :: KAtom s -> KAtom s -> Bool

(/=) :: KAtom s -> KAtom s -> Bool

Data s => Data (KAtom s)

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)

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)

Display an atom by showing (the hash of) its unique id.

Defined in Language.Nominal.Name

Methods

showsPrec :: Int -> KAtom s -> ShowS

show :: KAtom s -> String

showList :: [KAtom s] -> ShowS

Generic (KAtom s)

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)

Pick an atom

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen (KAtom s)

shrink :: KAtom s -> [KAtom s]

Typeable s => Swappable (KAtom s)

Base case for swapping: atoms acting on atoms.

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KAtom s -> KAtom s

SMonad [KAtom s] (KNom s)

Defined in Language.Nominal.Nom

Methods

(>>+) :: KNom s a -> ([KAtom s] -> a -> KNom s b) -> KNom s b

enter :: [KAtom s] -> a -> KNom s a

exit :: KNom s a -> a

(Typeable s, Swappable a) => Binder (KNom s a) [KAtom s] a s

Acts on a KNom binder by applying a function to the body and the context of locally bound names. Local names are preserved.

Defined in Language.Nominal.Binder

Methods

(@@) :: KNom s a -> ([KAtom s] -> a -> b) -> KNom s b

(@>) :: [KAtom s] -> a -> KNom s a

resMay :: [KAtom s] -> a -> Maybe (KNom s a)

(Typeable s, Swappable a, KRestrict s a) => BinderConc (KNom s a) [KAtom s] a s ()

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

Defined in Language.Nominal.Binder

Methods

conc :: KNom s a -> () -> a

cnoc :: () -> KNom s a -> a

(Typeable s, Swappable a) => BinderConc (KNom s a) [KAtom s] a s [KAtom s]

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.

Defined in Language.Nominal.Binder

Methods

conc :: KNom s a -> [KAtom s] -> a

cnoc :: [KAtom s] -> KNom s a -> a

(Typeable s, Swappable a) => BinderConc (KNom s a) [KAtom s] a s (Proxy s)

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 

Defined in Language.Nominal.Binder

Methods

conc :: KNom s a -> Proxy s -> a

cnoc :: Proxy s -> KNom s a -> a

Validator r d v => Binder (Chunk r d v) [Atom] [Transaction r d v] Tom

Acts on a Chunk by unpacking it as a transaction-list and a list of locally bound atoms, and applying a function.

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(@@) :: Chunk r d v -> ([Atom] -> [Transaction r d v] -> b) -> KNom Tom b

(@>) :: [Atom] -> [Transaction r d v] -> Chunk r d v

resMay :: [Atom] -> [Transaction r d v] -> Maybe (Chunk r d v)

type Rep (KAtom s)

Defined in Language.Nominal.Name

type Rep (KAtom s) = D1 (MetaData "KAtom" "Language.Nominal.Name" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" True) (C1 (MetaCons "Atom" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Unique)))

type Atom = KAtom Tom

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

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

Defined in Language.Nominal.Name

Methods

(==) :: Tom -> Tom -> Bool

(/=) :: Tom -> Tom -> Bool

Data Tom

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

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

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

Substitution. Capture-avoidance is automatic.

Defined in Language.Nominal.Examples.UntypedLambda

Methods

sub :: Var -> Exp -> Exp -> Exp

KSub V Operand Prog

Substitution on Programs is generic

Defined in Language.Nominal.Examples.Assembly2

Methods

sub :: V -> Operand -> Prog -> Prog

KSub V Operand Operand

Substitution as standard on Operand

Defined in Language.Nominal.Examples.Assembly2

Methods

sub :: V -> Operand -> Operand -> Operand

KSub V Operand Prog

Substitution on Programs is generic

Defined in Language.Nominal.Examples.Assembly1

Methods

sub :: V -> Operand -> Prog -> Prog

KSub V Operand Operand

Substitution as standard on Operand

Defined in Language.Nominal.Examples.Assembly1

Methods

sub :: V -> Operand -> Operand -> Operand

Swappable a => KRestrict Tom (Graph a)

Restriction action just passes the restriction on to the deep embedding

Defined in Language.Nominal.Examples.Graph

Methods

restrict :: [KAtom Tom] -> Graph a -> Graph a

Support r => KSupport Tom (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Input r -> Set (KAtom Tom)

UnifyPerm r => KUnifyPerm Tom (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Input r -> Input r -> KRen Tom

ren :: KRen Tom -> Input r -> Input r

KRestrict Tom (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

restrict :: [KAtom Tom] -> ValFin r d -> ValFin r d

KRestrict Tom (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

restrict :: [KAtom Tom] -> Val r d -> Val r d

KSupport Tom (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> ValFin r d -> Set (KAtom Tom)

KSupport Tom (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Val r d -> Set (KAtom Tom)

KSupport Tom (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> ValTriv r d -> Set (KAtom Tom)

(Support d, Support v) => KSupport Tom (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Output d v -> Set (KAtom Tom)

(UnifyPerm r, UnifyPerm d) => KUnifyPerm Tom (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> ValFin r d -> ValFin r d -> KRen Tom

ren :: KRen Tom -> ValFin r d -> ValFin r d

KUnifyPerm Tom (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> ValTriv r d -> ValTriv r d -> KRen Tom

ren :: KRen Tom -> ValTriv r d -> ValTriv r d

(UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Output d v -> Output d v -> KRen Tom

ren :: KRen Tom -> Output d v -> Output d v

(Swappable r, Swappable d, Swappable v) => KRestrict Tom (Chunk r d v)

Restrict atoms in a Chunk.

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

restrict :: [KAtom Tom] -> Chunk r d v -> Chunk r d v

(Support r, Support d, Support v) => KSupport Tom (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Blockchain r d v -> Set (KAtom Tom)

(Support r, Support d, Support v) => KSupport Tom (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Chunk r d v -> Set (KAtom Tom)

(Support d, Support r, Support v) => KSupport Tom (Context r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Context r d v -> Set (KAtom Tom)

(Support d, Support r, Support v) => KSupport Tom (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Transaction r d v -> Set (KAtom Tom)

(UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Blockchain r d v -> Blockchain r d v -> KRen Tom

ren :: KRen Tom -> Blockchain r d v -> Blockchain r d v

(UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Chunk r d v -> Chunk r d v -> KRen Tom

ren :: KRen Tom -> Chunk r d v -> Chunk r d v

(UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Context r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Context r d v -> Context r d v -> KRen Tom

ren :: KRen Tom -> Context r d v -> Context r d v

(UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Transaction r d v -> Transaction r d v -> KRen Tom

ren :: KRen Tom -> Transaction r d v -> Transaction r d v

Arbitrary (Name String)

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen (Name String)

shrink :: Name String -> [Name String]

(Swappable a, HasOutputPositions a) => HasOutputPositions (Nom a)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Nom a -> [Position]

(Arbitrary a, UnifyPerm a, Eq a, Arbitrary b, Eq b) => Arbitrary (EvFinMap a b)

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

Acts on a Chunk by unpacking it as a transaction-list and a list of locally bound atoms, and applying a function.

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(@@) :: Chunk r d v -> ([Atom] -> [Transaction r d v] -> b) -> KNom Tom b

(@>) :: [Atom] -> [Transaction r d v] -> Chunk r d v

resMay :: [Atom] -> [Transaction r d v] -> Maybe (Chunk r d v)

type Rep Tom

Defined in Language.Nominal.Name

type Rep Tom = D1 (MetaData "Tom" "Language.Nominal.Name" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) (V1 :: Type -> Type)

atTom :: Proxy Tom

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

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)

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

freshKAtomIO :: IO (KAtom s)

For convenience: generate a fresh katom

freshAtomIO :: IO Atom

For convenience: generate a fresh atom

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

Atom swapping

class Swappable a where

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

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

Instances

Swappable Bool

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Bool -> Bool

Swappable Char

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Char -> Char

Swappable Int

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Int -> Int

Swappable Integer

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Integer -> Integer

Swappable ()

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> () -> ()

Swappable Exp

Defined in Language.Nominal.Examples.UntypedLambda

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Exp -> Exp

Swappable Trm

Defined in Language.Nominal.Examples.SystemF

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Trm -> Trm

Swappable Typ

Defined in Language.Nominal.Examples.SystemF

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Typ -> Typ

Swappable Prog

Defined in Language.Nominal.Examples.Assembly2

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Prog -> Prog

Swappable Operand

Defined in Language.Nominal.Examples.Assembly2

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Operand -> Operand

Swappable Prog

Defined in Language.Nominal.Examples.Assembly1

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Prog -> Prog

Swappable Operand

Defined in Language.Nominal.Examples.Assembly1

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Operand -> Operand

Swappable a => Swappable [a]

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> [a] -> [a]

Swappable a => Swappable (Maybe a)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Maybe a -> Maybe a

Swappable a => Swappable (NonEmpty a)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> NonEmpty a -> NonEmpty a

(Ord a, Swappable a) => Swappable (Set a)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Set a -> Set a

Swappable (Nameless a)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Nameless a -> Nameless a

Typeable s => Swappable (KAtom s)

Base case for swapping: atoms acting on atoms.

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KAtom s -> KAtom s

Swappable a => Swappable (Graph a)

Defined in Language.Nominal.Examples.Graph

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Graph a -> Graph a

Swappable a => Swappable (BinderSupp a)

Defined in Language.Nominal.Binder

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> BinderSupp a -> BinderSupp a

Typeable s => Swappable (KRen s)

Defined in Language.Nominal.Unify

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KRen s -> KRen s

Swappable r => Swappable (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Input r -> Input r

(Swappable a, Swappable b) => Swappable (a -> b)

Swap distributes over function types, because functions inherit swapping action pointwise (also called the conjugation action)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> (a -> b) -> a -> b

(Swappable a, Swappable b) => Swappable (Either a b)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Either a b -> Either a b

(Swappable a, Swappable b) => Swappable (a, b)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> (a, b) -> (a, b)

(Swappable a, Swappable b, Ord a) => Swappable (Map a b)

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.

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Map a b -> Map a b

(Typeable s, Swappable t) => Swappable (KName s t)

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)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KName s t -> KName s t

(Swappable i, Swappable a) => Swappable (XSuspend i a)

Defined in Language.Nominal.SMonad

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> XSuspend i a -> XSuspend i a

(Typeable s, Swappable a) => Swappable (KNom s a)

Swap goes under name-binders.

swp n1 n2 (ns @> x) = (swp n1 n2 ns) @> (swp n1 n2 x)

Defined in Language.Nominal.Nom

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KNom s a -> KNom s a

(Swappable n, Swappable a) => Swappable (KAbs n a)

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)

Defined in Language.Nominal.Abs

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> KAbs n a -> KAbs n a

Swappable (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> ValFin r d -> ValFin r d

Swappable (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Val r d -> Val r d

Swappable (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> ValTriv r d -> ValTriv r d

(Swappable d, Swappable v) => Swappable (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Output d v -> Output d v

(Swappable a, Swappable b, Swappable c) => Swappable (a, b, c)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> (a, b, c) -> (a, b, c)

Swappable a => Swappable (KEvFinMap s a b)

Defined in Language.Nominal.Equivar

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KEvFinMap s a b -> KEvFinMap s a b

(Typeable s, Swappable a, Swappable b) => Swappable (KEvFun s a b)

Defined in Language.Nominal.Equivar

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KEvFun s a b -> KEvFun s a b

(Swappable r, Swappable d, Swappable v) => Swappable (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Blockchain r d v -> Blockchain r d v

(Swappable r, Swappable d, Swappable v) => Swappable (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Chunk r d v -> Chunk r d v

(Swappable r, Swappable d, Swappable v) => Swappable (Context r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Context r d v -> Context r d v

(Swappable r, Swappable d, Swappable v) => Swappable (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Transaction r d v -> Transaction r d v

(Swappable a, Swappable b, Swappable c, Swappable d) => Swappable (a, b, c, d)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> (a, b, c, d) -> (a, b, c, d)

(Swappable a, Swappable b, Swappable c, Swappable d, Swappable e) => Swappable (a, b, c, d, e)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> (a, b, c, d, e) -> (a, b, c, d, e)

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

A Tom-swapping

Permutations

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

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

type Perm = KPerm Tom

A permutation at Tom.

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

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

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

Pretty-print term variable

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTrm -> String

pp :: NTrm -> IO ()

PP NTyp

Pretty-print type variable

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTyp -> String

pp :: NTyp -> IO ()

KSub Var Exp Exp

Substitution. Capture-avoidance is automatic.

Defined in Language.Nominal.Examples.UntypedLambda

Methods

sub :: Var -> Exp -> Exp -> Exp

KSub NTrm Trm Trm

Substitute term variable with term in term

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTrm -> Trm -> Trm -> Trm

KSub NTyp Typ Trm

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Trm -> Trm

KSub NTyp Typ NTrm

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.

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> NTrm -> NTrm

KSub NTyp Typ Typ

Substitution acts on type variables. Capture-avoidance is automagical.

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Typ -> Typ

KSub V Operand Prog

Substitution on Programs is generic

Defined in Language.Nominal.Examples.Assembly2

Methods

sub :: V -> Operand -> Prog -> Prog

KSub V Operand Operand

Substitution as standard on Operand

Defined in Language.Nominal.Examples.Assembly2

Methods

sub :: V -> Operand -> Operand -> Operand

KSub V Operand Prog

Substitution on Programs is generic

Defined in Language.Nominal.Examples.Assembly1

Methods

sub :: V -> Operand -> Prog -> Prog

KSub V Operand Operand

Substitution as standard on Operand

Defined in Language.Nominal.Examples.Assembly1

Methods

sub :: V -> Operand -> Operand -> Operand

(Typeable s, Typeable u, KSupport s t) => KSupport s (KName u t)

Defined in Language.Nominal.NameSet

Methods

ksupp :: proxy s -> KName u t -> Set (KAtom s)

(KSupport s a, KSupport s t) => KSupport s (KAbs (KName s t) a)

Support of a :@> x is the support of x minus a

Defined in Language.Nominal.Abs

Methods

ksupp :: proxy s -> KAbs (KName s t) a -> Set (KAtom s)

(Typeable s, KUnifyPerm s t, KUnifyPerm s a) => KUnifyPerm s (KAbs (KName s t) a)

Unify Abs name-abstraction

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> KAbs (KName s t) a -> KAbs (KName s t) a -> KRen s

ren :: KRen s -> KAbs (KName s t) a -> KAbs (KName s t) a

(Typeable s, Typeable u, KUnifyPerm s t) => KUnifyPerm s (KName u t)

Unify names: they behave just an atom-label tuple

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> KName u t -> KName u t -> KRen s

ren :: KRen s -> KName u t -> KName u t

Functor (KName s)

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

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)

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)

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)

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen (Name String)

shrink :: Name String -> [Name String]

Eq (KName s t)

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.

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)

Abstractions are equal up to fusing their abstracted names.

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)

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)

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.

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

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)

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)

We show an abstraction by evaluating the function inside Abs on a fresh name (with the default Nothing label)

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)

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)

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)

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)

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)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KName s t -> KName s t

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

sub on a nominal abstraction substitutes in the label, and substitutes capture-avoidingly in the body

Defined in Language.Nominal.Sub

Methods

sub :: KName s n -> x -> KAbs (KName u t) y -> KAbs (KName u t) y

(Typeable s, Swappable t, Swappable a) => Binder (KAbs (KName s t) a) (KName s t) a s

Acts on an abstraction x' by unpacking x' as (n,x) for a fresh name n, and calculating f n x.

Defined in Language.Nominal.Abs

Methods

(@@) :: KAbs (KName s t) a -> (KName s t -> a -> b) -> KNom s b

(@>) :: KName s t -> a -> KAbs (KName s t) a

resMay :: KName s t -> a -> Maybe (KAbs (KName s t) a)

(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

Nameless form of substitution, where the name for which we substitute is packaged in a KAbs abstraction.

Defined in Language.Nominal.Sub

Methods

conc :: KAbs (KName s n) y -> x -> y

cnoc :: x -> KAbs (KName s n) y -> y

KSub (KName s n) (KName s n) (KName s n)

sub on names

Defined in Language.Nominal.Sub

Methods

sub :: KName s n -> KName s n -> KName s n -> KName s n

type Rep (KName s t)

Defined in Language.Nominal.Name

type Rep (KName s t) = D1 (MetaData "KName" "Language.Nominal.Name" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" 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

A Tom instance of KName.

withLabel :: KName s t -> t -> KName s t

As the name suggests: overwrite the name's label

withLabelOf :: KName s t -> KName s t -> KName s t

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

justALabel :: t -> KName s t

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

justAnAtom :: KAtom s -> KName s t

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

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

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

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

Nameless types

newtype Nameless a

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)

sub on nameless type is trivial

Defined in Language.Nominal.Sub

Methods

sub :: n -> x -> Nameless a -> Nameless a

Typeable s => KRestrict s (Nameless a)

Restriction is trivial on elements of nameless types

Defined in Language.Nominal.NameSet

Methods

restrict :: [KAtom s] -> Nameless a -> Nameless a

Typeable s => KSupport s (Nameless a)

Defined in Language.Nominal.NameSet

Methods

ksupp :: proxy s -> Nameless a -> Set (KAtom s)

(Typeable s, Eq a) => KUnifyPerm s (Nameless a)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> Nameless a -> Nameless a -> KRen s

ren :: KRen s -> Nameless a -> Nameless a

Eq a => Eq (Nameless a)

Defined in Language.Nominal.Name

Methods

(==) :: Nameless a -> Nameless a -> Bool

(/=) :: Nameless a -> Nameless a -> Bool

Ord a => Ord (Nameless a)

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)

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)

Defined in Language.Nominal.Name

Methods

showsPrec :: Int -> Nameless a -> ShowS

show :: Nameless a -> String

showList :: [Nameless a] -> ShowS

Swappable (Nameless a)

Defined in Language.Nominal.Name

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Nameless a -> Nameless a

Tests

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