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

Language | Haskell2010 |

This module provides the `Nominal`

type class. A type is
`Nominal`

if the group of finitely supported permutations of atoms
acts on it. We can abstract over an atom in such a type.

We also provide some generic programming so that instances of
`Nominal`

can be automatically derived in most 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.

- class Nominal t where
- data Defer t = Defer NominalPermutation t
- force :: Nominal t => Defer t -> t
- data BindAtom t = BindAtom NameGen (Atom -> Defer t)
- atom_abst :: Atom -> t -> BindAtom t
- atom_open :: Nominal t => BindAtom t -> (Atom -> t -> s) -> s
- atom_merge :: (Nominal t, Nominal s) => BindAtom t -> BindAtom s -> BindAtom (t, s)
- newtype Basic t = Basic t
- basic_action :: NominalPermutation -> t -> t
- class GNominal f where

# The Nominal class

class Nominal t where Source #

A type is nominal if the group of finitely supported permutations of atoms acts on it.

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.

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

Apply a permutation of atoms to a term.

(•) :: (Generic t, GNominal (Rep t)) => NominalPermutation -> t -> t Source #

Apply a permutation of atoms to a term.

# Deferred permutation

`Defer`

*t* is the type *t*, but equipped with an explicit substitution.
This is used to cache substitutions so that they can be optimized
and applied all at once.

Nominal (Defer t) Source # | |

NominalSupport t => NominalSupport (Defer t) Source # | |

NominalShow t => NominalShow (Defer t) Source # | |

# Atom abstraction

`BindAtom`

*t* is the type of atom abstractions, denoted [a]t in
the nominal logic literature. Its elements are of the form (a.v)
modulo alpha-equivalence. For full technical details on what this
means, see Definition 4 of [Pitts 2002].

Implementation note: we currently use an HOAS encoding, as this
turns out to be far more efficient (both in time and memory usage)
than the alternatives. An important invariant of the HOAS encoding
is that the underlying function must only be applied to *fresh*
atoms.

atom_open :: Nominal t => BindAtom t -> (Atom -> t -> s) -> s Source #

Destructor for atom abstractions. If *m* = *y*.*s*, the term

open m (\x t -> body)

binds *x* to a fresh name and *t* to a term such that *x*.*t* = *y*.*s*.

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

atom_merge :: (Nominal t, Nominal s) => BindAtom t -> BindAtom s -> BindAtom (t, s) Source #

Merge two abstractions. The defining property is

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

# Basic types

A *basic* or *non-nominal* type is a type whose elements cannot
contain any atoms. Typical examples are base types, such as `Integer`

or `Bool`

, and other types constructed exclusively from them,
such as `[`

or `Integer`

]

. On such types, the
nominal structure is trivial, i.e., `Bool`

-> `Bool`

`π • `

for all *x* = *x**x*.

For convenience, we define `Basic`

as a wrapper around such types,
which will automatically generate appropriate instances of
`Nominal`

, `NominalSupport`

, `NominalShow`

, and `Bindable`

. You can
use it, for example, like this:

type Term = Var Atom | Const (Basic Int) | App Term Term

Some common base types, including `Bool`

, `Char`

, `Int`

, `Integer`

,
`Double`

, `Float`

, and `Ordering`

are already instances of the
relevant type classes, and do not need to be wrapped in `Basic`

.

The use of `Basic`

can sometimes have a performance advantage. For
example,

is a more efficient `Basic`

`String`

`Nominal`

instance
than `String`

. Although they are semantically equivalent, the use
of `Basic`

prevents having to traverse the string to check each
character for atoms that are clearly not there.

Basic t |

# Nominal instances

Most of the time, instances of `Nominal`

should be derived using
`deriving (Generic, Nominal)`

, as in this example:

{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} data Term = Var Atom | App Term Term | Abs (Bind Atom Term) deriving (Generic, Nominal)

In the case of non-nominal types (typically base types such as
`Double`

), a `Nominal`

instance can be defined using
`basic_action`

:

instance Nominal MyType where (•) = basic_action

basic_action :: NominalPermutation -> t -> t Source #

A helper function for defining `Nominal`

instances
for non-nominal types.