Language.Nominal.Binder

Typeclass theory of binders

The Binder typeclass

Binder is a typeclass for creating and unpacking local bindings. The current development contains three instances of Binder:

• KNom itself: the primitive binding construct of this package.
• KAbs: abstraction by a single name.
• Chunk: a (generalisation of) EUTxO-style blockchains (the binding is in essence the names of edges connecting input-output pairs).

The simplest way to make a binder is to wrap a KNom in further structure:

• Chunk has this design. Its internal representation is structurally just a KNom (what makes it interesting is that it is wrapped in some smart contructors that validate nontrivial extra structure, involving binding and more).

However, it is possible to design a binder without explicitly mentioning KNom in its underlying representation:

• KAbs is an instance. For technical reasons its underlying representation uses functions, although a bijection does exist with a KNom-based structure (see absToNom and nomToAbs).

What makes Binder interesting is a rich array of destructors (e.g. @@, @@!, @@., nomApp, nomAppC, genApp, genAppC, resApp, resAppC, resAppC'). These correspond to common patterns of unpacking a binder and mapping to other types, and provide a consistent interface across different binding constructs.

class (Typeable s, Swappable ctx, Swappable body, Swappable ctxbody) => Binder ctxbody ctx body s | ctxbody -> ctx body s where

A typeclass for unpacking local binding.

Provides a function to unpack a binder, giving access to its locally bound names. Examples of binders include KNom, KAbs, and Chunk.

A Binder comes with a rich array of destructors, like @@, @@!, @@., nomApp, nomAppC, genApp, genAppC, resApp, resAppC, resAppC'. These correspond to common patterns of unpacking a binder and mapping to other types.

Below:

• ctxbody is the type of the datum in its name-binding context, which consists intuitively of data wrapped in a local name binding. (Canonical example: KNom.)
• ctx is the type of a concrete name-carrying representation of the local binding (atom, names, list of atoms, etc). (Canonical examples: KAtom and [KAtom].)
• body is the type of the body of the data.
• s is the type of atoms output. Output will be wrapped in KNom s.

For example the KAbs instance of Binder has type Binder (KAbs (KName s t) a) (KName s t) s a; and this means that

• a datum in ctxbody = KAbs (KName s t) a can be unpacked as
• something in ctx = KName s t and something in body = a, and
• mapped by a function of type KName s t -> a -> b using @@,
• to obtain something in KNom s b.

The other destructors (@@!, @@., nomApp, nomAppC, genApp, genAppC, resApp, resAppC, resAppC') are variations on this basic pattern which the wider development shows are empirically useful.

See also kbinderToNom and nomToMaybeBinder.

Minimal complete definition

(@@)

Methods

(@@) infixr 9

Arguments

:: ctxbody

the data in its local binding

-> (ctx -> body -> b)

function that inputs an explicit name context ctx and a body for that context, and outputs a b.

-> KNom s b

Result is a b in a binding context.

A destructor for the binder (required)

(@>) :: ctx -> body -> ctxbody infixr 1

A constructor for the binder (optional, since e.g. your instance may impose additional well-formedness constraints on the input). Call this res.

resMay :: ctx -> body -> Maybe ctxbody

A partial constructor for the binder, if preferred.

Instances

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

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)

(@@!) :: Binder ctxbody ctx body s => ctxbody -> (ctx -> body -> b) -> b infixr 9

Use this to map a binder to a type b, generating fresh atoms for any local bindings, and allowing them to escape.

(@@.) :: (Binder ctxbody ctx body s, KRestrict s b) => ctxbody -> (ctx -> body -> b) -> b infixr 9

Use this to map a binder to a type b with its own notion of restriction. Bindings do not escape.

pattern (:@@!) :: Binder ctxbody ctx body s => ctx -> body -> ctxbody infixr 0

This pattern is not quite as useful as it could be, because it's too polymorphic to use a COMPLETE pragma on. You can use it, but you may get incomplete pattern match errors.

nomApp :: Binder ctxbody ctx body s => (ctx -> body -> b) -> ctxbody -> KNom s b

Unpacks a binder and maps into a KNom environment.

nomApp = flip '(@@)'

nomAppC :: Binder ctxbody ctx body s => (body -> b) -> ctxbody -> KNom s b

Unpacks a binder and maps into a KNom environment. Local bindings are not examined, and get carried over to the KNom.

nomAppC = nomApp . const

genApp :: Binder ctxbody ctx body s => (ctx -> body -> b) -> ctxbody -> b

Unpacks a binder. New names are generated and released.

genApp = flip '(@@!)'

genAppC :: Binder ctxbody ctx body s => (body -> b) -> ctxbody -> b

Unpacks a binder. New names are generated and released. Local bindings are not examined.

genAppC = genApp . const

resApp :: (Binder ctxbody ctx body s, KRestrict s b) => (ctx -> body -> b) -> ctxbody -> b

Unpacks a binder and maps to a type with its own restrict operation.

resApp = flip '(@@.)'

resAppC :: (Binder ctxbody ctx body s, KRestrict s b) => (body -> b) -> ctxbody -> b

Unpacks a binder and maps to a type with its own restrict operation. Local bindings are not examined, and get carried over and restricted in the target type.

A common type instance is (a -> Bool) -> KNom s a -> Bool, in which case resAppC acts to capture-avoidingly apply a predicate under a binder, and return the relevant truth-value. See for example the code for transposeNomFunc.

resAppC = resApp . const

resAppC' :: (Binder ctxbody ctx body s, KRestrict s b) => ctxbody -> (body -> b) -> b

Unpacks a binder and maps to a type with its own restrict operation. Flipped version, for convenience.

A common type instance is KNom s a -> (a -> Bool) -> Bool , in which case resAppC' acts to apply a predicate inside a binder and return the relevant truth-value. See for example the code for transposeNomMaybe.

resAppC' = flip resApp

new quantifier

newA :: KRestrict s b => (KAtom s -> b) -> b

Evaluate predicate on fresh atom.

new :: (KRestrict s b, Swappable t) => t -> (KName s t -> b) -> b

Evaluate predicate on fresh name with label t.

freshForA :: (Typeable s, Swappable a, Eq a) => KAtom s -> a -> Bool

n is freshFor a when swp n' n a == a for a new n'. Straight out of the paper (publisher and author's pdfs).

/Note: In practice we mostly need this for names. This version is for atoms.

freshFor :: (Typeable s, Swappable t, Swappable a, Eq a) => KName s t -> a -> Bool

n is freshFor a when swp n' n a == a for a new n'. Straight out of the paper (publisher and author's pdfs).

Detecting trivial KNoms, that bind no atoms in their argument

isTrivialNomBySupp :: forall s a. KSupport s a => KNom s a -> Bool

Is the KNom binding trivial?

This is the KSupport version, for highly structured data that we can traverse (think: lists, tuples, sums, and maps).

See also isTrivialNomByEq, for less structured data when we have equality Eq and swapping KSwappable.

isTrivialNomByEq :: (Typeable s, Swappable a, Eq a) => KNom s a -> Bool

Is the KNom binding trivial?

This is the Eq version, using freshFor. Use this when we do have equality and swapping, but can't (or don't want to) traverse the type (think: sets).

See also isTrivialNomBySupp, for when we have KSupport.

KNom and supp

kfreshen :: KSupport s a => proxy s -> a -> KNom s a

Freshen all s-atoms, if we have KSupport. Returns result inside KNom binding to store the freshly-generated atoms.

freshen :: Support a => a -> Nom a

Freshen all atoms, if we have Support.

newtype BinderSupp a

Wrapper for generic method of deriving support of binder

Constructors

BinderSupp

Fields

• getBinderSupp :: a

Instances

(Binder ctxbody ctx body s, KSupport s ctx, KSupport s body) => KSupport s (BinderSupp ctxbody)

Defined in Language.Nominal.Binder

Methods

ksupp :: proxy s -> BinderSupp ctxbody -> Set (KAtom s)

Generic (BinderSupp a)

Defined in Language.Nominal.Binder

Associated Types

type Rep (BinderSupp a) :: Type -> Type

Methods

from :: BinderSupp a -> Rep (BinderSupp a) x

to :: Rep (BinderSupp a) x -> BinderSupp a

Swappable a => Swappable (BinderSupp a)

Defined in Language.Nominal.Binder

Methods

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

type Rep (BinderSupp a)

Defined in Language.Nominal.Binder

type Rep (BinderSupp a) = D1 (MetaData "BinderSupp" "Language.Nominal.Binder" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" True) (C1 (MetaCons "BinderSupp" PrefixI True) (S1 (MetaSel (Just "getBinderSupp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))

Binder isomorphism

The Binder class has two functions pointing in opposite directions. This suggests a standard isomorphism. We expect:

binderToNom <$> nomToMaybeBinder x == Just x
nomToBinder . binderToNom == id

For KNom and KAbs it's safe to use knomToBinder. For others, like Chunk, you would need knomToMaybeBinder, because additional well-formedness conditions are imposed on the constructor.

kbinderToNom :: Binder ctxbody ctx body s => proxy ctxbody -> ctxbody -> KNom s (ctx, body)

knomToBinder :: (Typeable s, Swappable ctx, Swappable body, Binder ctxbody ctx body s) => proxy ctxbody -> KNom s (ctx, body) -> ctxbody

knomToMaybeBinder :: (Typeable s, Swappable ctx, Swappable body, Binder ctxbody ctx body s) => proxy ctxbody -> KNom s (ctx, body) -> Maybe ctxbody

binderToNom :: Binder ctxbody ctx body s => ctxbody -> KNom s (ctx, body)

nomToBinder :: (Typeable s, Swappable ctx, Swappable body, Binder ctxbody ctx body s) => KNom s (ctx, body) -> ctxbody

nomToMaybeBinder :: (Typeable s, Swappable ctx, Swappable body, Binder ctxbody ctx body s) => KNom s (ctx, body) -> Maybe ctxbody

Binder with concretion

class Binder ctxbody ctx body s => BinderConc ctxbody ctx body s a where

Sometimes we can concrete a bound entity ctxbody at a datum a (where it need not be the case that a == ctx), to return a body body. In the case that a == ctx, we expect

(a @> x) `conc` a == x
a @> (x' `conc` a) == x

Minimal complete definition

conc | cnoc

Methods

conc :: ctxbody -> a -> body

cnoc :: a -> ctxbody -> body

Instances

Binder (KAbs n a) n a s => BinderConc (KAbs n a) n a s n

Concretes an abstraction at a particular name. Unsafe if the name is not fresh.

(abst a x) `conc` a == x

abst a (x `conc` a) == x -- provided a is suitably fresh. 

new' $ \a -> abst a (x `conc` a) == x  

Defined in Language.Nominal.Abs

Methods

conc :: KAbs n a -> n -> a

cnoc :: n -> KAbs n a -> 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

(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

Tests

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

Orphan instances

(Binder ctxbody ctx body s, Typeable ctxbody, Data ctx, Data body) => Data ctxbody

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ctxbody -> c ctxbody

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ctxbody

toConstr :: ctxbody -> Constr

dataTypeOf :: ctxbody -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ctxbody)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ctxbody)

gmapT :: (forall b. Data b => b -> b) -> ctxbody -> ctxbody

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ctxbody -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ctxbody -> r

gmapQ :: (forall d. Data d => d -> u) -> ctxbody -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ctxbody -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ctxbody -> m ctxbody

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ctxbody -> m ctxbody

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ctxbody -> m ctxbody