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

Contents

Description

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

Synopsis

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

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.