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

Language | Haskell2010 |

This module provides the class `Atomic`

, which generalizes the
type `Atom`

. The purpose of this is to allow users to define more
than one type of atoms.

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.

- class (Nominal a, NominalSupport a, Eq a, Ord a, Show a, Bindable a) => Atomic a where
- atomic_show :: Atomic a => a -> String
- with_fresh :: Atomic a => (a -> t) -> t
- with_fresh_named :: Atomic a => String -> (a -> t) -> t
- with_fresh_namelist :: Atomic a => NameSuggestion -> (a -> t) -> t
- fresh :: Atomic a => IO a
- fresh_named :: Atomic a => String -> IO a
- fresh_namelist :: Atomic a => NameSuggestion -> IO a
- bind :: (Atomic a, Nominal t) => (a -> t) -> Bind a t
- bind_named :: (Atomic a, Nominal t) => String -> (a -> t) -> Bind a t
- bind_namelist :: (Atomic a, Nominal t) => NameSuggestion -> (a -> t) -> Bind a t
- to_bindatom :: (Atomic a, Nominal t) => Bind a t -> BindAtom t
- from_bindatom :: (Atomic a, Nominal t) => BindAtom t -> Bind a t
- merge :: (Atomic a, Nominal t, Nominal s) => Bind a t -> Bind a s -> Bind a (t, s)
- class AtomKind a where
- newtype AtomOfKind a = AtomOfKind Atom
- atomofkind_names :: AtomKind a => AtomOfKind a -> NameGen

# The `Atomic`

class

class (Nominal a, NominalSupport a, Eq a, Ord a, Show a, Bindable a) => Atomic a where Source #

A type class for atom types.

The suggested way to define a type of atoms is to define a new
empty type *t* that is an instance of `AtomKind`

. Optionally, a
list of suggested names for the new atoms can be provided. (These
will be used as the names of bound variables unless otherwise
specified). Then `AtomOfKind`

*t* is a new type of atoms.

data VarName instance AtomKind VarName where suggested_names = ["x", "y", "z"] newtype Variable = AtomOfKind VarName

## Basic operations

atomic_show :: Atomic a => a -> String Source #

Return the name of an atom.

## Creation of fresh atoms in a scope

with_fresh :: Atomic a => (a -> t) -> t Source #

Perform a computation in the presence of a fresh atom.

The correct use of this function is subject to Pitts's freshness condition. Thus, for example, the following uses are permitted:

with_fresh (\a -> f a == g a) with_fresh (\a -> a . f a b c)

Here is an example of what is *not* permitted:

with_fresh (\a -> a)

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

with_fresh_named :: Atomic a => String -> (a -> t) -> t Source #

A version of `with_fresh`

that permits a suggested name to be
given to the atom. The name is only a suggestion, and will be
changed, if necessary, to avoid clashes.

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

with_fresh_namelist :: Atomic a => NameSuggestion -> (a -> t) -> t Source #

A version of `with_fresh`

that permits a list of suggested names
to be specified. The first suitable name in the list will be used
if possible.

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

## Creation of fresh atoms globally

fresh_named :: Atomic a => String -> IO a Source #

A version of `fresh`

that that permits a suggested name to be
given to the atom. The name is only a suggestion, and will be
changed, if necessary, when the atom is bound.

fresh_namelist :: Atomic a => NameSuggestion -> IO a Source #

A version of `with_fresh`

that permits a list of suggested names
to be specified. The first suitable name in the list will be used
if possible.

Implementation note: the implementation of `fresh_namelist`

differs slightly from that of `with_fresh_namelist`

. The function
`fresh_namelist`

generates a concrete name for the atom
immediately, whereas `with_fresh_namelist`

only does so on demand.
The idea is that most atoms generated by `with_fresh_namelist`

will
be bound immediately and their concrete name never displayed.

## Convenience functions for abstraction

bind :: (Atomic a, Nominal t) => (a -> t) -> Bind a t Source #

A convenience function for constructing binders. We can write

bind (\x -> t)

to denote the abstraction (x.t), where *x* is a fresh atom.

bind_named :: (Atomic a, Nominal t) => String -> (a -> t) -> Bind a t Source #

A version of `bind`

that also takes a suggested name for the bound atom.

bind_namelist :: (Atomic a, Nominal t) => NameSuggestion -> (a -> t) -> Bind a t Source #

A version of `bind`

that also take a list of suggested names for
the bound atom.

## Merging

to_bindatom :: (Atomic a, Nominal t) => Bind a t -> BindAtom t Source #

Convert an atomic binding to an atom binding.

from_bindatom :: (Atomic a, Nominal t) => BindAtom t -> Bind a t Source #

Convert an atom binding to an atomic binding.

merge :: (Atomic a, Nominal t, Nominal s) => Bind a t -> Bind a s -> Bind a (t, s) Source #

Sometimes, it is necessary to open two abstractions, using the
*same* fresh name for both of them. An example of this is the
typing rule for lambda abstraction in dependent type theory:

Gamma, x:t |- e : s ------------------------------------ Gamma |- Lam (x.e) : Pi t (x.s)

In the bottom-up reading of this rule, we are given the terms `Lam`

*body* and `Pi`

*t* *body'*, and we require a fresh name *x* and
terms *e*, *s* such that *body* = (*x*.*e*) and
*body'* = (*x*.*s*). Crucially, the same atom *x* should be used
in both *e* and *s*, because we subsequently need to check that *e*
has type *s* in some scope that is common to *e* and *s*.

The `merge`

primitive permits us to deal with such situations. Its
defining property is

merge (x.e) (x.s) = (x.(e,s)).

We can therefore solve the above problem:

let (x :. (e,s)) = merge body body' in ....

Moreover, the `merge`

primitive can be used to define other
merge-like functionality. For example, it is easy to define a
function

merge_list :: (Atomic a, Nominal t) => [Bind a t] -> Bind a [t]

in terms of it.

Semantically, the `merge`

operation implements the isomorphism of
nominal sets [*A*]*T* × [*A*]*S* = [*A*](*T* × *S*).

If *x* and *y* are atoms with user-suggested concrete names and

(z.(t',s')) = merge (x.t) (y.s),

then *z* will be preferably given the concrete name of *x*, but the
concrete name of *y* will be used if the name of *x* would cause a
clash.

# Multiple atom types

class AtomKind a where Source #

An atom kind is a type-level constant (typically an empty type)
that is an instance of the `AtomKind`

class. An atom kind is
optionally equipped with a list of suggested names for this kind of
atom. For example:

data VarName instance AtomKind VarName where suggested_names _ = ["x", "y", "z"]

data TypeName instance AtomKind TypeName where suggested_names _ = ["a", "b", "c"]

It is possible to have infinitely many atom kinds, for example:

data Zero data Succ a instance AtomKind Zero instance AtomKind (Succ a)

Then Zero, Succ Zero, Succ (Succ Zero), etc., will all be atom kinds.

suggested_names :: a -> NameSuggestion Source #

An optional list of default names for this kind of atom.

expand_names :: a -> NameSuggestion -> [String] Source #

An optional function for generating infinitely many distinct
names from a finite list of suggestions. The default behavior is
to append numerical subscripts. For example, the names
`[x, y, z]`

are by default expanded to ```
[x, y, z, x₁, y₁, z₁,
x₂, y₂, …]
```

, using Unicode for the subscripts. To use a a
different naming convention, redefine `expand_names`

.

It is not strictly necessary for all of the returned names to be distinct; it is sufficient that there are infinitely many distinct ones.

Example: the following generates new variable names by appending primes instead of subscripts:

expand_names _ xs = ys where ys = xs ++ map (++ "'") ys

newtype AtomOfKind a Source #

The type of atoms of a given kind. For example:

type Variable = AtomOfKind VarName type Type = AtomOfKind TypeName

Eq (AtomOfKind a) Source # | |

Ord (AtomOfKind a) Source # | |

AtomKind a => Show (AtomOfKind a) Source # | |

Generic (AtomOfKind a) Source # | |

AtomKind a => Nominal (AtomOfKind a) Source # | |

AtomKind a => NominalSupport (AtomOfKind a) Source # | |

AtomKind a => Bindable (AtomOfKind a) Source # | |

AtomKind a => Atomic (AtomOfKind a) Source # | |

AtomKind a => NominalShow (AtomOfKind a) Source # | |

type Rep (AtomOfKind a) Source # | |

atomofkind_names :: AtomKind a => AtomOfKind a -> NameGen Source #

Return the list of default names associated with the *kind* of
the given atom (not the name(s) of the atom itself).