Language.Nominal.Nom

Nominal-flavoured implementation of data in a context of local names

The Nom monad

Broadly speaking there are three kinds of functions involving KNom:

• KNom-specific functions that may involve creating fresh atoms, but do not involve swappings.
• More general functions involving the Binder typeclass (defined using KNom, and of which KNom is the canonical instance). These functions tend to impose Swappable and Typeable constraints on their type parameters.
• KNom-specific functions in which, for various reasons (elegance, avoiding code duplication, necessity) we make use of both classes of functions above.

This file deals with the first class above. The second and third are in Language.Nominal.Binder.

Remark: KNom is more basic than Binder, though it's the canonical instance. This creates a design tension: is a function on KNom best viewed as a function directly on Nom, or as an instance of a more general function involving Binder?

newtype KNom s a

Data in local KAtom s-binding context.

Constructors

Nom

Fields

• getNom :: IO (XRes s a)

  Recover a name-generating IO action from a KNom binding. If you execute one of these using unsafePerformIO, you get the data in a (the body of the binding), with some actual freshly-generated atoms. See also unNom.

Instances

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

Defined in Language.Nominal.Nom

Methods

restrict :: [KAtom t] -> KNom s a -> KNom s a

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

KRestrict atms in a, inside KNom monad.

Defined in Language.Nominal.Nom

Methods

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

(KSupport t a, Typeable s) => KSupport t (KNom s a)

Defined in Language.Nominal.Nom

Methods

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

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

Unify KNom abstractions. Unpack, unify, clean out fresh names

Defined in Language.Nominal.Unify

Methods

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

ren :: KRen s -> KNom s a -> KNom s a

Monad (KNom s)

Defined in Language.Nominal.Nom

Methods

(>>=) :: KNom s a -> (a -> KNom s b) -> KNom s b

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

return :: a -> KNom s a

fail :: String -> KNom s a

Functor (KNom s)

Defined in Language.Nominal.Nom

Methods

fmap :: (a -> b) -> KNom s a -> KNom s b

(<$) :: a -> KNom s b -> KNom s a

Applicative (KNom s)

Defined in Language.Nominal.Nom

Methods

pure :: a -> KNom s a

(<*>) :: KNom s (a -> b) -> KNom s a -> KNom s b

liftA2 :: (a -> b -> c) -> KNom s a -> KNom s b -> KNom s c

(*>) :: KNom s a -> KNom s b -> KNom s b

(<*) :: KNom s a -> KNom s b -> KNom s a

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

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Nom a -> [Position]

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

Eq a => Eq (KNom s a)

Fresh names are generated when name contexts are opened for equality test

Defined in Language.Nominal.Nom

Methods

(==) :: KNom s a -> KNom s a -> Bool

(/=) :: KNom s a -> KNom s a -> Bool

Show a => Show (KNom s a)

Show a nom by unpacking it

Defined in Language.Nominal.Nom

Methods

showsPrec :: Int -> KNom s a -> ShowS

show :: KNom s a -> String

showList :: [KNom s a] -> ShowS

Generic (KNom s a)

Defined in Language.Nominal.Nom

Associated Types

type Rep (KNom s a) :: Type -> Type

Methods

from :: KNom s a -> Rep (KNom s a) x

to :: Rep (KNom s a) x -> KNom s a

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

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen (KNom s a)

shrink :: KNom s a -> [KNom s 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

(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

Alternative f => Alternative (KNom s :. f)

Alternatives are composed in a capture-avoiding manner

Defined in Language.Nominal.Nom

Methods

empty :: (KNom s :. f) a

(<|>) :: (KNom s :. f) a -> (KNom s :. f) a -> (KNom s :. f) a

some :: (KNom s :. f) a -> (KNom s :. f) [a]

many :: (KNom s :. f) a -> (KNom s :. f) [a]

type Rep (KNom s a)

Defined in Language.Nominal.Nom

type Rep (KNom s a) = D1 (MetaData "KNom" "Language.Nominal.Nom" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" True) (C1 (MetaCons "Nom" PrefixI True) (S1 (MetaSel (Just "getNom") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (IO (XRes s a)))))

type Nom = KNom Tom

Data in a local atom-binding context at Toms.

Creating a KNom

res :: (Typeable s, Swappable a) => [KAtom s] -> a -> KNom s a

Constructor for KNom s.

kres :: (Typeable s, Swappable a) => proxy s -> [KAtom s] -> a -> KNom s a

Constructor for KNom s (proxy version).

resN :: (Typeable s, Swappable a) => [KName s t] -> a -> KNom s a

A version of res on KNom that takes names, not atoms (it just strips the labels of the names and acts on their atoms).

reRes :: (Typeable s, Swappable a) => KNom s a -> KNom s a

Make sure restricted atoms will alpha-convert to avoid capture, if e.g. they were created using enter and not res.

Destroying a KNom

unNom :: KRestrict s a => KNom s a -> a

Use this to safely exit a KNom monad. It works by binding the KNom-bound s-atoms using a's native instance of KRestrict. See Language.Nominal.Examples.Tutorial for examples.

unNom = resAppC id

Note: The less versions of unNom are the exit and exitWith instances of KNom as an instance of SMonad. See also @@.

nomToIO :: KNom s a -> IO a

Another way to safely exit KNom: convert it to an IO action (the IO may generate fresh names)

Creating fresh ids in a KNom

freshKAtom :: KNom s (KAtom s)

Create a fresh atom-in-nominal-context

freshAtom :: Nom Atom

Canonical version for unit atoms sort.

freshKAtoms :: Traversable m => m t -> KNom s (m (KAtom s))

Fresh Traversable m of atoms (e.g. m is list or stream)

freshAtoms :: Traversable m => m t -> Nom (m Atom)

Fresh Traversable m of atoms (e.g. m is list or stream). | Tom instance.

freshKName :: t -> KNom s (KName s t)

Create a fresh name-in-a-nominal-context with label t

freshName :: t -> Nom (Name t)

Canonical version of freshKName for Tom name.

freshKNames :: Traversable m => m t -> KNom s (m (KName s t))

Create fresh names-in-a-nominal-context

freshNames :: Traversable m => m t -> Nom (m (Name t))

Canonical version of freshKNames for Tom names.

freshKNameIO :: t -> IO (KName s t)

Create a fresh name-in-a-nominal-context with label t

freshNameIO :: t -> IO (Name t)

Canonical version of freshKName for Tom name.

freshKNamesIO :: Traversable m => m t -> IO (m (KName s t))

Create fresh names-in-a-nominal-context

freshNamesIO :: Traversable m => m t -> IO (m (Name t))

Canonical version of freshKNames for Tom names.

KNom and other functors

There are three functions that will commute KNom with some other f:

• transposeNomF
• transposeMF
• transposeFM

Taken together, these functions are making a point that KNom is compatible with your favourite container type. Because KNom commutes, there is no need to wonder whether (for example) a graph-with-binding should be a graph with binding on the vertices, or on the edges, or on the graph overall, or any combination. All of these are valid design decisions and one may be more convenient than the other, but we know we can isomorphically commute to a single top-level KNom binding.

In that sense, KNom captures a general theory of binding. This also mathematically justifies why the Binder typeclass is so useful.

transposeNomF :: (Functor f, Typeable s, Swappable a) => KNom s (f a) -> f (KNom s a)

KNom commutes down through functors.

transposeNomF is a version of transposeMF where bindings are have added capture-avoidance (for inverse, see transposeFM).

Tests

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

module Language.Nominal.SMonad