nom-0.1.0.1: Name-binding & alpha-equivalence

Copyright(c) Murdoch J. Gabbay 2020
LicenseGPL-3
Maintainermurdoch.gabbay@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellNone
LanguageHaskell2010

Language.Nominal.Name

Contents

Description

The basic framework: a nominal theory of names and swappings

Synopsis

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

(Swappable a, HasOutputPositions a) => HasOutputPositions (Nom a) Source # 
Instance details

Defined in Language.Nominal.Examples.IdealisedEUTxO

(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

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

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

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

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.