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

Contents

The Binder typeclass
new quantifier
Detecting trivial KNoms, that bind no atoms in their argument
KNom and supp
Binder isomorphism
Binder with concretion
Tests
Orphan instances

Description

Typeclass theory of binders

Synopsis

class (Typeable s, Swappable ctx, Swappable body, Swappable ctxbody) => Binder ctxbody ctx body s | ctxbody -> ctx body s where
- (@@) :: ctxbody -> (ctx -> body -> b) -> KNom s b
- (@>) :: ctx -> body -> ctxbody
- resMay :: ctx -> body -> Maybe ctxbody
(@@!) :: Binder ctxbody ctx body s => ctxbody -> (ctx -> body -> b) -> b
(@@.) :: (Binder ctxbody ctx body s, KRestrict s b) => ctxbody -> (ctx -> body -> b) -> b
pattern (:@@!) :: Binder ctxbody ctx body s => ctx -> body -> ctxbody
nomApp :: Binder ctxbody ctx body s => (ctx -> body -> b) -> ctxbody -> KNom s b
nomAppC :: Binder ctxbody ctx body s => (body -> b) -> ctxbody -> KNom s b
genApp :: Binder ctxbody ctx body s => (ctx -> body -> b) -> ctxbody -> b
genAppC :: Binder ctxbody ctx body s => (body -> b) -> ctxbody -> b
resApp :: (Binder ctxbody ctx body s, KRestrict s b) => (ctx -> body -> b) -> ctxbody -> b
resAppC :: (Binder ctxbody ctx body s, KRestrict s b) => (body -> b) -> ctxbody -> b
resAppC' :: (Binder ctxbody ctx body s, KRestrict s b) => ctxbody -> (body -> b) -> b
newA :: KRestrict s b => (KAtom s -> b) -> b
new :: (KRestrict s b, Swappable t) => t -> (KName s t -> b) -> b
freshForA :: (Typeable s, Swappable a, Eq a) => KAtom s -> a -> Bool
freshFor :: (Typeable s, Swappable t, Swappable a, Eq a) => KName s t -> a -> Bool
isTrivialNomBySupp :: forall s a. KSupport s a => KNom s a -> Bool
isTrivialNomByEq :: (Typeable s, Swappable a, Eq a) => KNom s a -> Bool
kfreshen :: KSupport s a => proxy s -> a -> KNom s a
freshen :: Support a => a -> Nom a
newtype BinderSupp a = BinderSupp {
- getBinderSupp :: a
}
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
class Binder ctxbody ctx body s => BinderConc ctxbody ctx body s a where
- conc :: ctxbody -> a -> body
- cnoc :: a -> ctxbody -> body

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

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

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

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

A partial constructor for the binder, if preferred.

Instances

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

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

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

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

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

Unpacks a binder and maps into a KNom environment.

nomApp = flip '(@@)'

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

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

Unpacks a binder. New names are generated and released.

genApp = flip '(@@!)'

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

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

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

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

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

Evaluate predicate on fresh atom.

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

Evaluate predicate on fresh name with label t.

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

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

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 `KNom`s, that bind no atoms in their argument

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

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

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

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

Freshen all atoms, if we have Support.

newtype BinderSupp a Source #

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) Source #
Instance details Defined in Language.Nominal.Binder Methods ksupp :: proxy s -> BinderSupp ctxbody -> Set (KAtom s) Source #
Generic (BinderSupp a) Source #
Instance details 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) Source #
Instance details Defined in Language.Nominal.Binder Methods kswp :: Typeable s => KAtom s -> KAtom s -> BinderSupp a -> BinderSupp a Source #
type Rep (BinderSupp a) Source #
Instance details Defined in Language.Nominal.Binder type Rep (BinderSupp a) = D1 (MetaData "BinderSupp" "Language.Nominal.Binder" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" 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) Source #

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

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

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

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

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

Binder with concretion

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

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

cnoc :: a -> ctxbody -> body Source #

Instances

Binder (KAbs n a) n a s => BinderConc (KAbs n a) n a s n Source #	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
Instance details Defined in Language.Nominal.Abs Methods conc :: KAbs n a -> n -> a Source # cnoc :: n -> KAbs n a -> 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 #
(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 #

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

Instance details

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 #

The Binder typeclass

new quantifier

Detecting trivial KNoms, that bind no atoms in their argument

KNom and supp

Binder isomorphism

Binder with concretion

Tests

Orphan instances

The `Binder` typeclass

`new` quantifier

Detecting trivial `KNom`s, that bind no atoms in their argument

`KNom` and `supp`