nominal-0.2.0.0: Binders and alpha-equivalence made easy

Nominal.NominalSupport

Description

This module provides the NominalSupport type class. It consists of those types for which the support can be calculated. With the exception of function types, most Nominal types are also in NominalSupport.

We also provide some generic programming so that instances of NominalSupport 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

# Literal strings

newtype Literal Source #

A wrapper around strings. This is used to denote any literal strings whose values should not clash with the names of bound variables. For example, if a term contains a constant symbol c, the name c should not also be used as the name of a bound variable. This can be achieved by marking the string with Literal, like this

data Term = Var Atom | Const (Literal String) | ...

Another way to use Literal is in the definition of custom NominalSupport instances. See "Defining custom instances" for an example.

Constructors

 Literal String

Instances

 Source # MethodsshowList :: [Literal] -> ShowS # Source # Methods Source # Methods Source # Methods Source # Methods

# Support

data Avoidee Source #

Something to be avoided can be an atom or a string.

Constructors

 A Atom S String

Instances

 Source # Methods(==) :: Avoidee -> Avoidee -> Bool #(/=) :: Avoidee -> Avoidee -> Bool # Source # Methods(<) :: Avoidee -> Avoidee -> Bool #(<=) :: Avoidee -> Avoidee -> Bool #(>) :: Avoidee -> Avoidee -> Bool #(>=) :: Avoidee -> Avoidee -> Bool # Source # MethodsshowList :: [Avoidee] -> ShowS #

newtype Support Source #

This type provides an internal representation for the support of a nominal term, i.e., the set of atoms (and constants) occurring in it. This is an abstract type with no exposed structure. The only way to construct a value of type Support is to use the function support.

Constructors

 Support (Set Avoidee)

The empty support.

The union of a list of supports.

The union of two supports.

Add an atom to the support.

A singleton support.

Delete an atom from the support.

support_deletes :: [Atom] -> Support -> Support Source #

Delete a list of atoms from the support.

Add a literal string to the support.

Convert the support to a list of strings.

# The NominalSupport class

class Nominal t => NominalSupport t where Source #

NominalSupport is a subclass of Nominal consisting of those types for which the support can be calculated. With the notable exception of function types, most Nominal types are also instances of NominalSupport.

In most cases, instances of NominalSupport 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

support :: t -> Support Source #

Compute a set of atoms and strings that should not be used as the names of bound variables.

support :: (Generic t, GNominalSupport (Rep t)) => t -> Support Source #

Compute a set of atoms and strings that should not be used as the names of bound variables.

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methodssupport :: () -> Support Source # Source # Methods Source # Methods NominalSupport t => NominalSupport [t] Source # Methodssupport :: [t] -> Support Source # Source # Methods (Ord k, NominalSupport k) => NominalSupport (Set k) Source # Methodssupport :: Set k -> Support Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods (NominalSupport a, NominalSupport b) => NominalSupport (Either a b) Source # Methodssupport :: Either a b -> Support Source # (NominalSupport t, NominalSupport s) => NominalSupport (t, s) Source # Methodssupport :: (t, s) -> Support Source # (Ord k, NominalSupport k, NominalSupport v) => NominalSupport (Map k v) Source # Methodssupport :: Map k v -> Support Source # (Bindable a, NominalSupport a, NominalSupport t) => NominalSupport (Bind a t) Source # Methodssupport :: Bind a t -> Support Source # (NominalSupport t, NominalSupport s, NominalSupport r) => NominalSupport (t, s, r) Source # Methodssupport :: (t, s, r) -> Support Source # (NominalSupport t, NominalSupport s, NominalSupport r, NominalSupport q) => NominalSupport (t, s, r, q) Source # Methodssupport :: (t, s, r, q) -> Support Source # (NominalSupport t, NominalSupport s, NominalSupport r, NominalSupport q, NominalSupport p) => NominalSupport (t, s, r, q, p) Source # Methodssupport :: (t, s, r, q, p) -> Support Source # (NominalSupport t, NominalSupport s, NominalSupport r, NominalSupport q, NominalSupport p, NominalSupport o) => NominalSupport (t, s, r, q, p, o) Source # Methodssupport :: (t, s, r, q, p, o) -> Support Source # (NominalSupport t, NominalSupport s, NominalSupport r, NominalSupport q, NominalSupport p, NominalSupport o, NominalSupport n) => NominalSupport (t, s, r, q, p, o, n) Source # Methodssupport :: (t, s, r, q, p, o, n) -> Support Source #

# Open for printing

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

A variant of open which moreover chooses a name for the bound atom that does not clash with any free name in its scope. This function is mostly useful for building custom pretty-printers for nominal terms. Except in pretty-printers, it is equivalent to open.

Usage:

open_for_printing sup t (\x s sup' -> body)

Here, sup = support t. For printing to be efficient (roughly O(n)), the support must be pre-computed in a bottom-up fashion, and then passed into each subterm in a top-down fashion (rather than re-computing it at each level, which would be O(n²)). For this reason, open_for_printing takes the support of t as an additional argument, and provides sup', the support of s, as an additional parameter to the body.

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

# NominalSupport instances

Most of the time, instances of NominalSupport should be derived using deriving (Generic, NominalSupport), as in this example:

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}

data Term = Var Atom | App Term Term | Abs (Bind Atom Term)
deriving (Generic, NominalSupport)

In the case of non-nominal types (typically base types such as Double), a NominalSupport instance can be defined using basic_support:

instance NominalSupport MyType where
support = basic_support

basic_support :: t -> Support Source #

A helper function for defining NominalSupport instances for non-nominal types.

# Generic programming for NominalSupport

class GNominalSupport f where Source #

A version of the NominalSupport class suitable for generic programming.

Minimal complete definition

gsupport

Methods

gsupport :: f a -> Support Source #

Instances

 Source # Methods Source # Methods NominalSupport a => GNominalSupport (K1 * i a) Source # Methodsgsupport :: K1 * i a a -> Support Source # (GNominalSupport a, GNominalSupport b) => GNominalSupport ((:+:) * a b) Source # Methodsgsupport :: (* :+: a) b a -> Support Source # (GNominalSupport a, GNominalSupport b) => GNominalSupport ((:*:) * a b) Source # Methodsgsupport :: (* :*: a) b a -> Support Source # GNominalSupport a => GNominalSupport (M1 * i c a) Source # Methodsgsupport :: M1 * i c a a -> Support Source #