nom-0.1.0.2: Name-binding & alpha-equivalence

Copyright(c) Murdoch J. Gabbay 2020
LicenseGPL-3
Maintainermurdoch.gabbay@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellNone
LanguageHaskell2010

Language.Nominal

Contents

Description

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

Synopsis

Introduction

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

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

Quick links

Worked examples

Links and references

Related work

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

Type(class) overview

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.