nominal-0.2.0.0: Binders and alpha-equivalence made easy

Safe HaskellNone
LanguageHaskell2010

Nominal.Bindable

Contents

Description

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, (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.

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.

Synopsis

Binding lists of atoms

data BindAtomList t Source #

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

Constructors

BindNil t 
BindCons (BindAtom (BindAtomList t)) 

Instances

Generic (BindAtomList t) Source # 

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) Source # 
type Rep (BindAtomList t) Source # 
type Rep (BindAtomList t) = D1 * (MetaData "BindAtomList" "Nominal.Bindable" "nominal-0.2.0.0-GZ6w56NCfcED1WEKXzjIsV" 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 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.

Constructors

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

data Bind a t Source #

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

Constructors

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

Instances

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

Methods

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

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

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

Methods

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

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

Methods

support :: Bind a t -> Support 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.

Methods

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.

Instances

Bindable Bool Source # 
Bindable Char Source # 
Bindable Double Source # 
Bindable Float Source # 
Bindable Int Source # 
Bindable Integer Source # 
Bindable Ordering Source # 
Bindable () Source # 

Methods

binding :: () -> NominalBinder () Source #

Bindable Atom Source # 
Bindable Literal Source # 
Bindable a => Bindable [a] Source # 

Methods

binding :: [a] -> NominalBinder [a] Source #

Bindable a => Bindable (Maybe a) Source # 
Bindable (Basic t) Source # 
Nominal t => Bindable (NoBind t) Source # 
AtomKind a => Bindable (AtomOfKind a) Source # 
(Bindable a, Bindable b) => Bindable (Either a b) Source # 

Methods

binding :: Either a b -> NominalBinder (Either a b) Source #

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

Methods

binding :: (a, b) -> NominalBinder (a, b) Source #

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

Methods

binding :: (a, b, c) -> NominalBinder (a, b, c) Source #

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

Methods

binding :: (a, b, c, d) -> NominalBinder (a, b, c, d) Source #

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

Methods

binding :: (a, b, c, d, e) -> NominalBinder (a, b, c, d, e) Source #

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

Methods

binding :: (a, b, c, d, e, f) -> NominalBinder (a, b, c, d, e, f) Source #

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

Methods

binding :: (a, b, c, d, e, f, g) -> NominalBinder (a, b, c, d, e, f, g) Source #

(.) :: (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 (Bind a b). The result of matching the pattern (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

newtype NoBind t Source #

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.(yNoBind 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) Source # 

Methods

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

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

Ord t => Ord (NoBind t) Source # 

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

Methods

showsPrec :: Int -> NoBind t -> ShowS #

show :: NoBind t -> String #

showList :: [NoBind t] -> ShowS #

Generic (NoBind t) Source # 

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) Source # 
NominalSupport t => NominalSupport (NoBind t) Source # 

Methods

support :: NoBind t -> Support Source #

Nominal t => Bindable (NoBind t) Source # 
type Rep (NoBind t) Source # 
type Rep (NoBind t) = D1 * (MetaData "NoBind" "Nominal.Bindable" "nominal-0.2.0.0-GZ6w56NCfcED1WEKXzjIsV" 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, 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.

Minimal complete definition

gbinding

Methods

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

Instances

GBindable (V1 *) Source # 

Methods

gbinding :: V1 * a -> (V1 * a -> b) -> NominalBinder b Source #

GBindable (U1 *) Source # 

Methods

gbinding :: U1 * a -> (U1 * a -> b) -> NominalBinder b Source #

Bindable a => GBindable (K1 * i a) Source # 

Methods

gbinding :: K1 * i a a -> (K1 * i a a -> b) -> NominalBinder b Source #

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

Methods

gbinding :: (* :+: a) b a -> ((* :+: a) b a -> b) -> NominalBinder b Source #

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

Methods

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

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

Methods

gbinding :: M1 * i c a a -> (M1 * i c a a -> b) -> NominalBinder b Source #

Miscellaneous

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

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.