Nominal.Bindable

This module provides a type class Bindable. It contains things (such as atoms, tuples of atoms, etc.) that can be abstracted by binders (sometimes also called patterns). Moreover, for each bindable type a and nominal type t, it defines a type Bind a t of abstractions.

We also provide some generic programming so that instances of Bindable can be automatically derived in many cases.

For example, (x,y).t binds a pair of atoms in t. It is roughly equivalent to x.y.t, except that it is of type Bind (Atom, Atom) t instead of Bind Atom (Bind Atom t).

If a binder contains repeated atoms, they are regarded as distinct. The binder is treated as if one atom occurrence was bound at a time, in some fixed but unspecified order. For example, (x,x).(x,x) is equivalent to either (x,y).(x,x) or (x,y).(y,y). Which of the two alternatives is chosen is implementation specific and user code should not rely on the order of abstractions in such cases.

Binding lists of atoms

data BindAtomList t

The type of abstractions of a list of atoms. It is equivalent to Bind [Atom] t, but has a more low-level implementation.

Constructors

BindNil t

BindCons (BindAtom (BindAtomList t))

Instances

Generic (BindAtomList t)

Associated Types

type Rep (BindAtomList t) :: * -> *

Methods

from :: BindAtomList t -> Rep (BindAtomList t) x

to :: Rep (BindAtomList t) x -> BindAtomList t

Nominal t => Nominal (BindAtomList t)

Methods

(•) :: NominalPermutation -> BindAtomList t -> BindAtomList t

type Rep (BindAtomList t)

type Rep (BindAtomList t) = D1 * (MetaData "BindAtomList" "Nominal.Bindable" "nominal-0.1.0.0-AMwVAaTlUVUE19PvBCEVWv" False) ((:+:) * (C1 * (MetaCons "BindNil" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t))) (C1 * (MetaCons "BindCons" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (BindAtom (BindAtomList t))))))

atomlist_abst :: [Atom] -> t -> BindAtomList t

Abstract a list of atoms in a term.

atomlist_open :: Nominal t => BindAtomList t -> ([Atom] -> t -> s) -> s

Open a list abstraction.

atomlist_open_for_printing :: Nominal t => Support -> BindAtomList t -> ([Atom] -> t -> Support -> s) -> s

Open a list abstraction for printing.

atomlist_merge :: (Nominal t, Nominal s) => BindAtomList t -> BindAtomList s -> Maybe (BindAtomList (t, s))

Merge a pair of list abstractions. If the lists are of different lengths, return Nothing.

Binder combinators

data NominalPattern a

A representation of patterns of type a. This is an abstract type with no exposed structure. The only way to construct a value of type NominalPattern a is through the Applicative interface and by using the functions binding and nobinding.

Constructors

NominalPattern [Atom] ([Atom] -> (a, [Atom]))

Instances

Functor NominalPattern

Methods

fmap :: (a -> b) -> NominalPattern a -> NominalPattern b

(<$) :: a -> NominalPattern b -> NominalPattern a

Applicative NominalPattern

Methods

pure :: a -> NominalPattern a

(<*>) :: NominalPattern (a -> b) -> NominalPattern a -> NominalPattern b

liftA2 :: (a -> b -> c) -> NominalPattern a -> NominalPattern b -> NominalPattern c

(*>) :: NominalPattern a -> NominalPattern b -> NominalPattern b

(<*) :: NominalPattern a -> NominalPattern b -> NominalPattern a

Implementation note: The behavior of a pattern is determined by two things: the list of bound atom occurrences (binding sites), and a renaming function that takes such a list of atoms and returns a term. For efficiency, the renaming function is stateful: it also returns a list of atoms not yet used.

The binding sites must be serialized in some deterministic order, and must be accepted in the same corresponding order by the renaming function.

If an atom occurs at multiple binding sites of the pattern, it must be serialized multiple times. The corresponding renaming function must accept fresh atoms and put them into the respective binding sites.

Examples:

binding x = NominalPattern [x] (\(x:zs) -> (x, zs))

binding (x, y) = NominalPattern [x, y] (\(x:y:zs) -> ((x, y), zs))

binding (x, NoBind y) = NominalPattern [x] (\(x:zs) -> ((x, NoBind y), zs))

binding (x, x, y) = NominalPattern [x, x, y] (\(x:x':y:zs) -> ((x, x', y), zs))

nobinding :: a -> NominalPattern a

Constructor for non-binding patterns. This can be used to mark non-binding subterms when defining a Bindable instance. See "Defining custom instances" for examples.

atom_binding :: Atom -> NominalPattern Atom

Constructor for a pattern binding a single atom.

pattern_map :: (a -> b) -> NominalPattern a -> NominalPattern b

Map a function over a NominalPattern.

pattern_app :: NominalPattern (a -> b) -> NominalPattern a -> NominalPattern b

Combinator giving NominalPattern an applicative structure. This is used for constructing tuple binders.

The Bindable class

data Bind a t

Bind a t is the type of atom abstractions, denoted [A]T in the nominal logic literature. Its elements are pairs (a,t) modulo alpha-equivalence. We also write a.t for such an equivalence class of pairs. For full technical details on what this means, see Definition 4 of [Pitts 2002].

Constructors

Bind ([Atom] -> a) (BindAtomList t)

Instances

(Nominal a, Nominal t, Eq a, Eq t) => Eq (Bind a t)

Methods

(==) :: Bind a t -> Bind a t -> Bool

(/=) :: Bind a t -> Bind a t -> Bool

(Bindable a, Nominal t) => Nominal (Bind a t)

Methods

(•) :: NominalPermutation -> Bind a t -> Bind a t

(Bindable a, NominalSupport a, NominalSupport t) => NominalSupport (Bind a t)

Methods

support :: Bind a t -> Support

(Bindable a, NominalShow a, NominalShow t) => NominalShow (Bind a t)

Methods

showsPrecSup :: Support -> Int -> Bind a t -> ShowS

nominal_showList :: Support -> [Bind a t] -> ShowS

class Nominal a => Bindable a where

A type is Bindable if its elements can be abstracted by binders. Such elements are also called patterns. Examples include atoms, tuples of atoms, list of atoms, etc.

In most cases, instances of Nominal can be automatically derived. See "Deriving generic instances" for information on how to do so, and "Defining custom instances" for how to write custom instances.

Methods

binding :: a -> NominalPattern a

A function that maps a term to a pattern. New patterns can be constructed using the Applicative structure of NominalPattern. See "Defining custom instances" for examples.

binding :: (Generic a, GBindable (Rep a)) => a -> NominalPattern a

A function that maps a term to a pattern. New patterns can be constructed using the Applicative structure of NominalPattern. See "Defining custom instances" for examples.

Instances

Bindable Bool

Methods

binding :: Bool -> NominalPattern Bool

Bindable Char

Methods

binding :: Char -> NominalPattern Char

Bindable Double

Methods

binding :: Double -> NominalPattern Double

Bindable Float

Methods

binding :: Float -> NominalPattern Float

Bindable Int

Methods

binding :: Int -> NominalPattern Int

Bindable Integer

Methods

binding :: Integer -> NominalPattern Integer

Bindable ()

Methods

binding :: () -> NominalPattern ()

Bindable Atom

Methods

binding :: Atom -> NominalPattern Atom

Bindable Literal

Methods

binding :: Literal -> NominalPattern Literal

Bindable a => Bindable [a]

Methods

binding :: [a] -> NominalPattern [a]

Bindable (Basic t)

Methods

binding :: Basic t -> NominalPattern (Basic t)

Nominal t => Bindable (NoBind t)

Methods

binding :: NoBind t -> NominalPattern (NoBind t)

AtomKind a => Bindable (AtomOfKind a)

Methods

binding :: AtomOfKind a -> NominalPattern (AtomOfKind a)

(Bindable a, Bindable b) => Bindable (a, b)

Methods

binding :: (a, b) -> NominalPattern (a, b)

(Bindable a, Bindable b, Bindable c) => Bindable (a, b, c)

Methods

binding :: (a, b, c) -> NominalPattern (a, b, c)

(Bindable a, Bindable b, Bindable c, Bindable d) => Bindable (a, b, c, d)

Methods

binding :: (a, b, c, d) -> NominalPattern (a, b, c, d)

(Bindable a, Bindable b, Bindable c, Bindable d, Bindable e) => Bindable (a, b, c, d, e)

Methods

binding :: (a, b, c, d, e) -> NominalPattern (a, b, c, d, e)

(Bindable a, Bindable b, Bindable c, Bindable d, Bindable e, Bindable f) => Bindable (a, b, c, d, e, f)

Methods

binding :: (a, b, c, d, e, f) -> NominalPattern (a, b, c, d, e, f)

(Bindable a, Bindable b, Bindable c, Bindable d, Bindable e, Bindable f, Bindable g) => Bindable (a, b, c, d, e, f, g)

Methods

binding :: (a, b, c, d, e, f, g) -> NominalPattern (a, b, c, d, e, f, g)

(.) :: (Bindable a, Nominal t) => a -> t -> Bind a t infixr 5

Atom abstraction: a.t represents the equivalence class of pairs (a,t) modulo alpha-equivalence.

We use the infix operator (.), which is normally bound to function composition in the standard Haskell library. Thus, nominal programs should import the standard library like this:

import Prelude hiding ((.))

Note that (.) is a binder of the object language (i.e., whatever datatype you are defining), not of the metalanguage (i.e., Haskell). A term such as a.t only makes sense if a is already defined to be some atom. Thus, binders are often used in a context of with_fresh or open, such as the following:

with_fresh (\a -> a.a)

abst :: (Bindable a, Nominal t) => a -> t -> Bind a t

An alternative non-infix notation for (.). This can be useful when using qualified module names, because "̈Nominal.." is not valid syntax.

open :: (Bindable a, Nominal t) => Bind a t -> (a -> t -> s) -> s

Destructor for atom abstraction. In an ideal programming idiom, we would be able to define a function on atom abstractions by pattern matching like this:

f (a.s) = body.

Haskell doesn't let us provide this syntax, but using the open function, we can equivalently write:

f t = open t (\a s -> body).

Each time an abstraction is opened, a is guaranteed to be a fresh atom. To guarantee soundness (referential transparency and equivariance), the body is subject to the same restriction as with_fresh, namely, a must be fresh for the body (in symbols a # body).

open_for_printing :: (Bindable a, Nominal t) => Support -> Bind a t -> (a -> t -> Support -> s) -> s

A variant of open which moreover chooses a name for the bound atom that does not clash with any free name in its scope. This function is mostly useful for building custom pretty-printers for nominal terms. Except in pretty-printers, it is equivalent to open.

Usage:

open_for_printing sup t (\x s sup' -> body)

Here, sup = support t (this requires a NominalSupport instance). For printing to be efficient (roughly O(n)), the support must be pre-computed in a bottom-up fashion, and then passed into each subterm in a top-down fashion (rather than re-computing it at each level, which would be O(n²)). For this reason, open_for_printing takes the support of t as an additional argument, and provides sup', the support of s, as an additional parameter to the body.

open2 :: (Bindable a, Bindable b, Nominal t) => Bind a (Bind b t) -> (a -> b -> t -> s) -> s

Open two abstractions at once. So

f t = open t (\x y s -> body)

is equivalent to the nominal pattern matching

f (x.y.s) = body

open2_for_printing :: (Bindable a, Bindable b, Nominal t) => Support -> Bind a (Bind b t) -> (a -> b -> t -> Support -> s) -> s

Like open2, but open two abstractions for printing.

Non-binding patterns

newtype NoBind t

The type constructor NoBind permits data of arbitrary types (including nominal types) to be embedded in binders without becoming bound. For example, in the term

m = (a, NoBind b).(a,b),

the atom a is bound, but the atom b remains free. Thus, m is alpha-equivalent to (x, NoBind b).(x,b), but not to (x, NoBind c).(x,c).

A typical use case is using contexts as binders. A context is a map from atoms to some data (for example, a typing context is a map from atoms to types, and an evaluation context is a map from atoms to values). If we define contexts like this:

type Context t = [(Atom, NoBind t)]

then we can use contexts as binders. Specifically, if Γ = {x₁ ↦ A₁, …, xₙ ↦ Aₙ} is a context, then (Γ . t) binds the context to a term t. This means, x₁,…,xₙ are bound in t, but not any atoms that occur in A₁,…,Aₙ. Without the use of NoBind, any atoms occurring on A₁,…,Aₙ would have been bound as well.

Even though atoms under NoBind are not binding, they can still be bound by other binders. For example, the term x.(x, NoBind x) is alpha-equivalent to y.(y, NoBind y). Another way to say this is that NoBind has a special behavior on the left, but not on the right of a dot.

Constructors

NoBind t

Instances

Eq t => Eq (NoBind t)

Methods

(==) :: NoBind t -> NoBind t -> Bool

(/=) :: NoBind t -> NoBind t -> Bool

Ord t => Ord (NoBind t)

Methods

compare :: NoBind t -> NoBind t -> Ordering

(<) :: NoBind t -> NoBind t -> Bool

(<=) :: NoBind t -> NoBind t -> Bool

(>) :: NoBind t -> NoBind t -> Bool

(>=) :: NoBind t -> NoBind t -> Bool

max :: NoBind t -> NoBind t -> NoBind t

min :: NoBind t -> NoBind t -> NoBind t

Show t => Show (NoBind t)

Methods

showsPrec :: Int -> NoBind t -> ShowS

show :: NoBind t -> String

showList :: [NoBind t] -> ShowS

Generic (NoBind t)

Associated Types

type Rep (NoBind t) :: * -> *

Methods

from :: NoBind t -> Rep (NoBind t) x

to :: Rep (NoBind t) x -> NoBind t

Nominal t => Nominal (NoBind t)

Methods

(•) :: NominalPermutation -> NoBind t -> NoBind t

NominalSupport t => NominalSupport (NoBind t)

Methods

support :: NoBind t -> Support

Nominal t => Bindable (NoBind t)

Methods

binding :: NoBind t -> NominalPattern (NoBind t)

type Rep (NoBind t)

type Rep (NoBind t) = D1 * (MetaData "NoBind" "Nominal.Bindable" "nominal-0.1.0.0-AMwVAaTlUVUE19PvBCEVWv" True) (C1 * (MetaCons "NoBind" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)))

Bindable instances

Most of the time, instances of Bindable should be derived using deriving (Generic, Nominal, Bindable), as in this example:

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}

data Term = Var Atom | App Term Term | Abs (Bind Atom Term)
  deriving (Generic, Nominal, Bindable)

In the case of non-nominal types (typically base types such as Double), a Bindable instance can be defined using basic_binding:

instance Bindable MyType where
  binding = basic_binding

In this case, a binder (x.t) is equivalent to an ordinary pair (x,t), since there is no bound atom that could be renamed.

basic_binding :: a -> NominalPattern a

A helper function for defining Bindable instances for non-nominal types.

Generic programming for Bindable

pattern_gpair :: NominalPattern (a x) -> NominalPattern (b x) -> ((a :*: b) x -> c) -> NominalPattern c

A specialized combinator. Although this functionality is expressible in terms of the applicative structure, we give a custom CPS-based implementation for performance reasons. It improves the overall performance by 14% (time) and 16% (space) in a typical benchmark.

class GBindable f where

A version of the Bindable class suitable for generic programming.

Minimal complete definition

gbinding

Methods

gbinding :: f a -> (f a -> b) -> NominalPattern b

Instances

GBindable (V1 *)

Methods

gbinding :: V1 * a -> (V1 * a -> b) -> NominalPattern b

GBindable (U1 *)

Methods

gbinding :: U1 * a -> (U1 * a -> b) -> NominalPattern b

Bindable a => GBindable (K1 * i a)

Methods

gbinding :: K1 * i a a -> (K1 * i a a -> b) -> NominalPattern b

(GBindable a, GBindable b) => GBindable ((:+:) * a b)

Methods

gbinding :: (* :+: a) b a -> ((* :+: a) b a -> b) -> NominalPattern b

(GBindable a, GBindable b) => GBindable ((:*:) * a b)

Methods

gbinding :: (* :*: a) b a -> ((* :*: a) b a -> b) -> NominalPattern b

GBindable a => GBindable (M1 * i c a)

Methods

gbinding :: M1 * i c a a -> (M1 * i c a a -> b) -> NominalPattern b

Miscellaneous

(∘) :: (b -> c) -> (a -> b) -> a -> c

Function composition.

Since we hide (.) from the standard library, and the fully qualified name of the Prelude's dot operator, "̈Prelude..", is not legal syntax, we provide '∘' as an alternate notation for composition.