nominal-0.2.0.0: Binders and alpha-equivalence made easy

Nominal.Nominal

Description

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.

Synopsis

# 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.

Methods

(•) :: 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.

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Nominal () Source # Methods(•) :: NominalPermutation -> () -> () Source # Source # Methods Source # Methods Nominal t => Nominal [t] Source # Methods(•) :: NominalPermutation -> [t] -> [t] Source # Nominal a => Nominal (Maybe a) Source # Methods (Ord k, Nominal k) => Nominal (Set k) Source # Methods(•) :: NominalPermutation -> Set k -> Set k Source # Nominal (Basic t) Source # Methods Nominal t => Nominal (BindAtom t) Source # Methods Nominal (Defer t) Source # Methods Nominal t => Nominal (NoBind t) Source # Methods Nominal t => Nominal (BindAtomList t) Source # Methods AtomKind a => Nominal (AtomOfKind a) Source # Methods (Nominal t, Nominal s) => Nominal (t -> s) Source # Methods(•) :: NominalPermutation -> (t -> s) -> t -> s Source # (Nominal a, Nominal b) => Nominal (Either a b) Source # Methods(•) :: NominalPermutation -> Either a b -> Either a b Source # (Nominal t, Nominal s) => Nominal (t, s) Source # Methods(•) :: NominalPermutation -> (t, s) -> (t, s) Source # (Ord k, Nominal k, Nominal v) => Nominal (Map k v) Source # Methods(•) :: NominalPermutation -> Map k v -> Map k v Source # (Bindable a, Nominal t) => Nominal (Bind a t) Source # Methods(•) :: NominalPermutation -> Bind a t -> Bind a t Source # (Nominal t, Nominal s, Nominal r) => Nominal (t, s, r) Source # Methods(•) :: NominalPermutation -> (t, s, r) -> (t, s, r) Source # (Nominal t, Nominal s, Nominal r, Nominal q) => Nominal (t, s, r, q) Source # Methods(•) :: NominalPermutation -> (t, s, r, q) -> (t, s, r, q) Source # (Nominal t, Nominal s, Nominal r, Nominal q, Nominal p) => Nominal (t, s, r, q, p) Source # Methods(•) :: NominalPermutation -> (t, s, r, q, p) -> (t, s, r, q, p) Source # (Nominal t, Nominal s, Nominal r, Nominal q, Nominal p, Nominal o) => Nominal (t, s, r, q, p, o) Source # Methods(•) :: NominalPermutation -> (t, s, r, q, p, o) -> (t, s, r, q, p, o) Source # (Nominal t, Nominal s, Nominal r, Nominal q, Nominal p, Nominal o, Nominal n) => Nominal (t, s, r, q, p, o, n) Source # Methods(•) :: NominalPermutation -> (t, s, r, q, p, o, n) -> (t, s, r, q, p, o, n) Source #

# Deferred permutation

data Defer t Source #

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.

Constructors

 Defer NominalPermutation t

Instances

 Nominal (Defer t) Source # Methods Source # Methods NominalShow t => NominalShow (Defer t) Source # MethodsshowsPrecSup :: Support -> Int -> Defer t -> ShowS Source #nominal_showList :: Support -> [Defer t] -> ShowS Source #

force :: Nominal t => Defer t -> t Source #

Apply a deferred permutation.

# Atom abstraction

data BindAtom t Source #

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.

Constructors

 BindAtom NameGen (Atom -> Defer t)

Instances

 (Nominal t, Eq t) => Eq (BindAtom t) Source # Methods(==) :: BindAtom t -> BindAtom t -> Bool #(/=) :: BindAtom t -> BindAtom t -> Bool # Nominal t => Nominal (BindAtom t) Source # Methods Source # Methods

atom_abst :: Atom -> t -> BindAtom t Source #

Atom abstraction: atom_abst a t represents the equivalence class of pairs (a,t) modulo alpha-equivalence. We first define this for Atom and later generalize to other Atomic types.

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

newtype Basic t Source #

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 [Integer] or Bool -> Bool. On such types, the nominal structure is trivial, i.e., π • x = x for all 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, Basic String is a more efficient 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.

Constructors

 Basic t

Instances

 Eq t => Eq (Basic t) Source # Methods(==) :: Basic t -> Basic t -> Bool #(/=) :: Basic t -> Basic t -> Bool # Ord t => Ord (Basic t) Source # Methodscompare :: Basic t -> Basic t -> Ordering #(<) :: Basic t -> Basic t -> Bool #(<=) :: Basic t -> Basic t -> Bool #(>) :: Basic t -> Basic t -> Bool #(>=) :: Basic t -> Basic t -> Bool #max :: Basic t -> Basic t -> Basic t #min :: Basic t -> Basic t -> Basic t # Show t => Show (Basic t) Source # MethodsshowsPrec :: Int -> Basic t -> ShowS #show :: Basic t -> String #showList :: [Basic t] -> ShowS # Nominal (Basic t) Source # Methods Source # Methods Source # Methods Show t => NominalShow (Basic t) Source # MethodsshowsPrecSup :: Support -> Int -> Basic t -> ShowS Source #nominal_showList :: Support -> [Basic t] -> ShowS Source #

# 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.

# Generic programming for Nominal

class GNominal f where Source #

A version of the Nominal class suitable for generic programming.

Minimal complete definition

gbullet

Methods

gbullet :: NominalPermutation -> f a -> f a Source #

Instances

 Source # Methods Source # Methods Nominal a => GNominal (K1 * i a) Source # Methodsgbullet :: NominalPermutation -> K1 * i a a -> K1 * i a a Source # (GNominal a, GNominal b) => GNominal ((:+:) * a b) Source # Methodsgbullet :: NominalPermutation -> (* :+: a) b a -> (* :+: a) b a Source # (GNominal a, GNominal b) => GNominal ((:*:) * a b) Source # Methodsgbullet :: NominalPermutation -> (* :*: a) b a -> (* :*: a) b a Source # GNominal a => GNominal (M1 * i c a) Source # Methodsgbullet :: NominalPermutation -> M1 * i c a a -> M1 * i c a a Source #