Safe Haskell	None
Language	Haskell2010

Nominal.Atomic

Contents

The Atomic class
Multiple atom types

Description

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.

Synopsis

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

Minimal complete definition

to_atom, from_atom, names

Methods

to_atom :: a -> Atom Source #

from_atom :: Atom -> a Source #

names :: a -> NameGen Source #

The default variable names for the atom type.

Instances

Atomic Atom Source #
Methods to_atom :: Atom -> Atom Source # from_atom :: Atom -> Atom Source # names :: Atom -> NameGen Source #
AtomKind a => Atomic (AtomOfKind a) Source #
Methods to_atom :: AtomOfKind a -> Atom Source # from_atom :: Atom -> AtomOfKind a Source # names :: AtomOfKind a -> NameGen Source #

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 :: Atomic a => IO a Source #

Generate a globally fresh atom of the given atomic type.

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.

Methods

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

Constructors

AtomOfKind Atom