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.

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. For soundness, the programmer must ensure that the atom created does not escape the body of the with_fresh block. Thus, 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)

Technically, the correctness condition is that in an application

with_fresh (\a -> body),

we must have a # body (see [Pitts 2002] for more details on what this means). Haskell does not enforce this restriction, but if a program violates it, referential transparency may not hold, which may, in the worst case, lead to unsound compiler optimizations and undefined behavior.

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.

This function is subject to the same correctness condition as with_fresh.

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.

This function is subject to the same correctness condition as with_fresh.

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 atom 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:

open (merge body body') (\x (e,s) -> .....)

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 x [A]S = [A](T x 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