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.Nom

Contents

The Nom monad
Creating a KNom
Destroying a KNom
Creating fresh ids in a KNom
KNom and other functors
Tests

Description

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

Synopsis

newtype KNom s a = Nom {
- getNom :: IO (XRes s a)
}
type Nom = KNom Tom
res :: (Typeable s, Swappable a) => [KAtom s] -> a -> KNom s a
kres :: (Typeable s, Swappable a) => proxy s -> [KAtom s] -> a -> KNom s a
resN :: (Typeable s, Swappable a) => [KName s t] -> a -> KNom s a
reRes :: (Typeable s, Swappable a) => KNom s a -> KNom s a
unNom :: KRestrict s a => KNom s a -> a
nomToIO :: KNom s a -> IO a
freshKAtom :: Typeable s => KNom s (KAtom s)
freshAtom :: Nom Atom
freshKAtoms :: (Traversable m, Typeable s) => m t -> KNom s (m (KAtom s))
freshAtoms :: Traversable m => m t -> Nom (m Atom)
freshKName :: Typeable s => t -> KNom s (KName s t)
freshName :: t -> Nom (Name t)
freshKNames :: (Traversable m, Typeable s) => m t -> KNom s (m (KName s t))
freshNames :: Traversable m => m t -> Nom (m (Name t))
transposeNomF :: (Functor f, Typeable s, Swappable a) => KNom s (f a) -> f (KNom s a)
module Language.Nominal.SMonad

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

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) Source #
Instance details Defined in Language.Nominal.Nom Methods restrict :: [KAtom t] -> KNom s a -> KNom s a Source #
(Typeable s, Swappable a) => KRestrict s (KNom s a) Source #	`KRestrict` `atms` in `a`, inside `KNom` monad.
Instance details Defined in Language.Nominal.Nom Methods restrict :: [KAtom s] -> KNom s a -> KNom s a Source #
(KSupport t a, Typeable s) => KSupport t (KNom s a) Source #
Instance details Defined in Language.Nominal.Nom Methods ksupp :: proxy t -> KNom s a -> Set (KAtom t) Source #
(Typeable s, KUnifyPerm s a) => KUnifyPerm s (KNom s a) Source #	Unify `KNom` abstractions. Unpack, unify, clean out fresh names
Instance details Defined in Language.Nominal.Unify Methods kunifyPerm :: proxy s -> KNom s a -> KNom s a -> KRen s Source # ren :: KRen s -> KNom s a -> KNom s a Source #
Monad (KNom s) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Language.Nominal.Examples.IdealisedEUTxO Methods outputPositions :: Nom a -> [Position] 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 #
Eq a => Eq (KNom s a) Source #	Fresh names are generated when name contexts are opened for equality test
Instance details 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) Source #	Show a nom by unpacking it
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) 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 #
(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 #
Alternative f => Alternative (KNom s :. f) Source #	Alternatives are composed in a capture-avoiding manner
Instance details 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) Source #
Instance details Defined in Language.Nominal.Nom type Rep (KNom s a) = D1 (MetaData "KNom" "Language.Nominal.Nom" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" True) (C1 (MetaCons "Nom" PrefixI True) (S1 (MetaSel (Just "getNom") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (IO (XRes s a)))))

type Nom = KNom Tom Source #

Data in a local atom-binding context at Toms.

Creating a `KNom`

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

Constructor for KNom s.

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

Constructor for KNom s (proxy version).

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

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

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

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

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 :: Typeable s => KNom s (KAtom s) Source #

Create a fresh atom-in-nominal-context

freshAtom :: Nom Atom Source #

Canonical version for unit atoms sort.

freshKAtoms :: (Traversable m, Typeable s) => m t -> KNom s (m (KAtom s)) Source #

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

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

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

freshKName :: Typeable s => t -> KNom s (KName s t) Source #

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

freshName :: t -> Nom (Name t) Source #

Canonical version of freshKName for Tom name.

freshKNames :: (Traversable m, Typeable s) => m t -> KNom s (m (KName s t)) Source #

Create fresh names-in-a-nominal-context

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

Canonical version of freshKNames for Tom names.

`KNom` and other functors

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

Taken together, these functions are making a point that KNom is compatible with your favourite container type. Because KNom can commuted, 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 in the end we can isomorphically commute to a single top-level KNom binding.

In that sense, KNom captures a general theory of binding. It is also a mathematical justification for why the Binder typeclass turns out to be so useful.

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

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

The Nom monad

Creating a KNom

Destroying a KNom

Creating fresh ids in a KNom

KNom and other functors

Tests

Creating a `KNom`

Destroying a `KNom`

Creating fresh ids in a `KNom`

`KNom` and other functors