Safe Haskell | None |
---|---|

Language | Haskell2010 |

This module provides a type class `Bindable`

. It contains things
(such as atoms, tuples of atoms, etc.) that can be abstracted by
binders. 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, `(`

binds a pair of atoms in *x*,*y*).*t**t*. It is
roughly equivalent to

, except that it is of type
*x*.*y*.*t*`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,
`(`

is equivalent to either *x*,*x*).(*x*,*x*)`(`

or *x*,*y*).(*x*,*x*)`(`

. Which of the two alternatives is chosen
is implementation specific and user code should not rely on the
order of abstractions in such cases.*x*,*y*).(*y*,*y*)

This module exposes implementation details of the Nominal library, and should not normally be imported. Users of the library should only import the top-level module Nominal.

- data BindAtomList t
- = BindNil t
- | BindCons (BindAtom (BindAtomList t))

- atomlist_abst :: [Atom] -> t -> BindAtomList t
- atomlist_open :: Nominal t => BindAtomList t -> ([Atom] -> t -> s) -> s
- atomlist_open_for_printing :: Nominal t => Support -> BindAtomList t -> ([Atom] -> t -> Support -> s) -> s
- atomlist_merge :: (Nominal t, Nominal s) => BindAtomList t -> BindAtomList s -> Maybe (BindAtomList (t, s))
- data NominalBinder a = NominalBinder [Atom] ([Atom] -> (a, [Atom]))
- nobinding :: a -> NominalBinder a
- atom_binding :: Atom -> NominalBinder Atom
- binder_map :: (a -> b) -> NominalBinder a -> NominalBinder b
- binder_app :: NominalBinder (a -> b) -> NominalBinder a -> NominalBinder b
- data Bind a t = Bind ([Atom] -> a) (BindAtomList t)
- class Nominal a => Bindable a where
- (.) :: (Bindable a, Nominal t) => a -> t -> Bind a t
- pattern (:.) :: (Nominal b, Bindable a) => a -> b -> Bind a b
- abst :: (Bindable a, Nominal t) => a -> t -> Bind a t
- open :: (Bindable a, Nominal t) => Bind a t -> (a -> t -> s) -> s
- open_for_printing :: (Bindable a, Nominal t) => Support -> Bind a t -> (a -> t -> Support -> s) -> s
- newtype NoBind t = NoBind t
- basic_binding :: a -> NominalBinder a
- binder_gpair :: NominalBinder (a x) -> NominalBinder (b x) -> ((a :*: b) x -> c) -> NominalBinder c
- class GBindable f where
- (∘) :: (b -> c) -> (a -> b) -> a -> c

# Binding lists of atoms

data BindAtomList t Source #

The type of abstractions of a list of atoms. It is equivalent to

, but has a more low-level implementation.`Bind`

[`Atom`

] *t*

BindNil t | |

BindCons (BindAtom (BindAtomList t)) |

Generic (BindAtomList t) Source # | |

Nominal t => Nominal (BindAtomList t) Source # | |

type Rep (BindAtomList t) Source # | |

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

Abstract a list of atoms in a term.

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

Open a list abstraction.

The correct use of this function is subject to Pitts's freshness condition.

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

Open a list abstraction for printing.

The correct use of this function is subject to Pitts's freshness condition.

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

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

.

# Binder combinators

data NominalBinder a Source #

A representation of binders of type *a*. This is an abstract
type with no exposed structure. The only way to construct a value
of type `NominalBinder`

*a* is through the `Applicative`

interface and by
using the functions `binding`

and `nobinding`

.

NominalBinder [Atom] ([Atom] -> (a, [Atom])) |

Implementation note: The behavior of a binders 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, 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 = NominalBinder [x] (\(x:zs) -> (x, zs)) binding (x, y) = NominalBinder [x, y] (\(x:y:zs) -> ((x, y), zs)) binding (x, NoBind y) = NominalBinder [x] (\(x:zs) -> ((x, NoBind y), zs)) binding (x, x, y) = NominalBinder [x, x, y] (\(x:x':y:zs) -> ((x, x', y), zs))

nobinding :: a -> NominalBinder a Source #

Constructor for non-binding binders. This can be used to mark
non-binding subterms when defining a `Bindable`

instance. See
"Defining custom instances" for examples.

atom_binding :: Atom -> NominalBinder Atom Source #

Constructor for a binder binding a single atom.

binder_map :: (a -> b) -> NominalBinder a -> NominalBinder b Source #

Map a function over a `NominalBinder`

.

binder_app :: NominalBinder (a -> b) -> NominalBinder a -> NominalBinder b Source #

Combinator giving `NominalBinder`

an applicative structure. This
is used for constructing tuple binders.

# The Bindable class

`Bind`

*a* *t* is the type of *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 2003].

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

(Nominal a, Nominal t, Eq a, Eq t) => Eq (Bind a t) Source # | |

(Bindable a, Nominal t) => Nominal (Bind a t) Source # | |

(Bindable a, NominalSupport a, NominalSupport t) => NominalSupport (Bind a t) Source # | |

(Bindable a, NominalShow a, NominalShow t) => NominalShow (Bind a t) Source # | |

class Nominal a => Bindable a where Source #

A type is `Bindable`

if its elements can be abstracted. Such
elements are also called *binders*, or sometimes *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.

binding :: a -> NominalBinder a Source #

A function that maps a term to a binder. New binders can be
constructed using the `Applicative`

structure of `NominalBinder`

.
See "Defining custom instances" for examples.

binding :: (Generic a, GBindable (Rep a)) => a -> NominalBinder a Source #

A function that maps a term to a binder. New binders can be
constructed using the `Applicative`

structure of `NominalBinder`

.
See "Defining custom instances" for examples.

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

Constructor for abstractions. The term *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 abstraction operator 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 the variable *a* is already defined to be a
particular atom. Thus, abstractions are often used in the context
of a scoped operation such as `with_fresh`

or on the
right-hand side of an abstraction pattern match, as in the
following examples:

with_fresh (\a -> a.a) subst m z (Abs (x :. t)) = Abs (x . subst m z t)

For building an abstraction by using a binder of the metalanguage,
see also the function `bind`

.

pattern (:.) :: (Nominal b, Bindable a) => a -> b -> Bind a b infixr 5 Source #

A pattern matching syntax for abstractions. The pattern
`(x :. t)`

is called an *abstraction pattern*. It matches any term
of type `(`

. The result of matching the pattern
`Bind`

*a* *b*)`(x :. t)`

against a value *y*`.`

*s* is to bind *x* to a fresh name
and *t* to a value such that *x*`.`

*t* = *y*`.`

*s*.
Note that a different fresh *x* is chosen each time an abstraction
patterns is used.
Here are some examples:

foo (x :. t) = body let (x :. t) = s in body case t of Var v -> body1 App m n -> body2 Abs (x :. t) -> body3

Like all patterns, abstraction patterns can be nested. For example:

foo1 (a :. b :. t) = ... foo2 (x :. (s,t)) = (x.s, x.t) foo3 (Abs (x :. Var y)) | x == y = ... | otherwise = ...

The correct use of abstraction patterns is subject to Pitts's freshness condition. Thus, for example, the following are permitted

let (x :. t) = s in x.t, let (x :. t) = s in f x t == g x t,

whereas the following is not permitted:

let (x :. t) = s in (x,t).

See "Pitts's freshness condition" for more details.

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

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

An alternative notation for abstraction patterns.

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

is precisely equivalent to

f (x :. s) = body.

The correct use of this function is subject to Pitts's freshness condition.

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

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.

The correct use of this function is subject to Pitts's freshness condition.

# Non-binding binders

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

is alpha-equivalent to
*x*.(*x*,
`NoBind`

*x*)

. Another way to say this is that *y*.(*y*, `NoBind`

*y*)`NoBind`

has a special behavior on the left, but not on the right of a dot.

NoBind 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, an abstraction (*x*.*t*) is equivalent to an ordinary
pair (*x*,*t*), since there is no bound atom that could be renamed.

basic_binding :: a -> NominalBinder a Source #

A helper function for defining `Bindable`

instances
for non-nominal types.

# Generic programming for Bindable

binder_gpair :: NominalBinder (a x) -> NominalBinder (b x) -> ((a :*: b) x -> c) -> NominalBinder c Source #

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

A version of the `Bindable`

class suitable for generic programming.

gbinding :: f a -> (f a -> b) -> NominalBinder b Source #