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

Contents

Description

Typeclass theory of binders

Synopsis

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 KNoms, 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

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 #