Nominal-flavoured implementation of data in a context of local names, designed following the ideas in a new approach to abstract syntax with variable binding (see also author's pdfs).

The interaction of name-binding and alpha-equivalence with data can be tricky. Examples include:

• Inductively defining syntax and reductions of a syntax with binding, e.g. lambda-calculus. An example is in Language.Nominal.Examples.SystemF.
• Graph-like structures, especially if they have dangling pointers. An example is in Language.Nominal.Examples.IdealisedEUTxO.

This package implements a solution in Haskell, based on names and swappings.

Features include:

• This is a package; no need to use a modified compiler.
• No state monad is imposed. Binding environments like KNom and Abs are available, but they track local scope not global scope and are relatively easy to escape.
• No distinction is imposed between free names and bound names. Names are just another datatype whose values can be freely passed around. Binding operators are just datatype constructors.
• Capture-avoidance is taken care of in the background.
• A well-understood mathematical reference model is available, in nominal techniques as referenced in a new approach to abstract syntax with variable binding (see also author's pdfs).

Worked examples

• Language.Nominal.Examples.Tutorial: We explore some basic concepts.
• Language.Nominal.Examples.UntypedLambda: Untyped lambda-calculus syntax and reductions (short example).
• Language.Nominal.Examples.Assembly1: A simple assembly language, with binding (short example).
• Language.Nominal.Examples.Assembly2: A simple assembly language, with binding and a swap-variable primitive (short example).
• Language.Nominal.Examples.Style: Some basic comments on recommended programming style using this package.
• Language.Nominal.Examples.SystemF: System F syntax and reductions (longer example).
• Language.Nominal.Examples.IdealisedEUTxO: A EUTxO-style blockchain system, following the ideas in mathematical idealisation of the Extended UTxO model (longer example).

Links and references

• This package's GitHub page.
• The underlying mathematical model is described in a new approach to abstract syntax with variable binding (author's pdfs).
• The paper on closed nominal rewriting (author's pdfs) is pertinent to the design of Language.Nominal.Unify.
• The paper on the mathematical idealisation of the Extended UTxO model is pertinent Language.Nominal.Examples.IdealisedEUTxO.
• This draft book on orbit-finite sets may be of interest.
• The Bound package, from which the worked examples Language.Nominal.Examples.Assembly1 and Language.Nominal.Examples.Assembly2 are adapted.

Related work

• bound: Making de Bruijn Succ less
• unbound: Generic support for programming with names and binders
• unbound-generics: Support for programming with names and binders using GHC Generics
• nominal: Binders and alpha-equivalence made easy
• NLambda: computations over infinite structures using logical formulas and SMT solving

(Something I should put on this list? Let me know.)

Here is an overview of some core typeclasses:

• KAtom and KAtom: Types of atomic freshly generatable identifiers.
• KName and KName: Types of labelled atoms.
• KSwappable and Swappable: Typeclasses of types with a swapping action by atoms and names.
• KSupport and Support: Typeclasses of types with a structural notion of the atoms in this object. In the mathematics, "support" coincides with "atoms for which the object may be asymmetric under swappings", but in this package support means something much stricter: that it is possible to traverse the data and pick out the atoms in its support. Note: "having empty support" does not mean "having no atoms". It means "symmetric under swapping atoms", which is not at all the same idea.
• Nameless: types like Int, String, and () that are guaranteed atoms-free.
• KNom and KNom: An atoms-binding monad.
• Binder: A typeclass for functions acting on binding types.
• KAbs and Abs: A name-abstracting functor.
• KRestrict and Restrict: A typeclass of types with an inherent notion of atoms-binding.
• KUnifyPerm and UnifyPerm: Typeclasses of types with a notion of unification by injective partial functions on atoms.