nominal-0.1.0.0: Binders and alpha-equivalence made easy

Safe HaskellNone
LanguageHaskell2010

Nominal.Atom

Contents

Description

This module provides a type of atoms. An atom is a globally unique identifier that also has a concrete name, as well as additional name suggestions (in case it must be renamed).

Synopsis

Atoms

data Atom Source #

An atom is a globally unique, opaque value.

Constructors

Atom Unique String NameGen

An atom consists of a unique identifier, a concrete name, and some optional name suggestions.

Instances

Eq Atom Source # 

Methods

(==) :: Atom -> Atom -> Bool #

(/=) :: Atom -> Atom -> Bool #

Ord Atom Source #

User code should not explicitly compare atoms for relative ordering, because this is not referentially transparent (can be unsound). However, we define an Ord instance for atoms anyway, because it permits atoms to be used as keys in Sets and Maps.

Methods

compare :: Atom -> Atom -> Ordering #

(<) :: Atom -> Atom -> Bool #

(<=) :: Atom -> Atom -> Bool #

(>) :: Atom -> Atom -> Bool #

(>=) :: Atom -> Atom -> Bool #

max :: Atom -> Atom -> Atom #

min :: Atom -> Atom -> Atom #

Show Atom Source # 

Methods

showsPrec :: Int -> Atom -> ShowS #

show :: Atom -> String #

showList :: [Atom] -> ShowS #

Nominal Atom Source # 
NominalSupport Atom Source # 

Methods

support :: Atom -> Support Source #

Bindable Atom Source # 
Atomic Atom Source # 
NominalShow Atom Source # 

Basic operations on atoms

atom_show :: Atom -> String Source #

Return the name of an atom.

atom_names :: Atom -> NameGen Source #

Return the suggested names of an atom.

Creation of fresh atoms globally

fresh_atom_named :: String -> NameGen -> IO Atom Source #

Globally create a fresh atom with the given name and name suggestions.

fresh_atom :: NameGen -> IO Atom Source #

Globally create a fresh atom with the given name suggestions.

Creation of fresh atoms in a scope

with_fresh_atom_named :: String -> NameGen -> (Atom -> a) -> a Source #

Create a fresh atom with the given name and name suggestions. To ensure soundness, the created atom must not escape the body of the with_fresh block. Otherwise, referential transparency may be violated. For example,

with_fresh id != with_fresh id.

See the documentation of with_fresh for more information on the correctness criterion.

with_fresh_atom :: NameGen -> (Atom -> a) -> a Source #

Create a fresh atom with the given name suggestion.

Here, the call to global_new is performed lazily (outside of the IO monad), so an actual concrete name will only be computed on demand.