| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Nominal.Nominal
Contents
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
- class Nominal t where
- (•) :: NominalPermutation -> t -> t
- 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
- gbullet :: NominalPermutation -> f a -> f a
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.
Minimal complete definition
Nothing
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
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.
Constructors
| Defer NominalPermutation t |
Instances
| Nominal (Defer t) Source # | |
Defined in Nominal.Nominal | |
| NominalSupport t => NominalSupport (Defer t) Source # | |
| NominalShow t => NominalShow (Defer t) Source # | |
Defined in Nominal.NominalShow | |
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]Bool -> Boolπ • 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 StringNominal 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 # | |
| Ord t => Ord (Basic t) Source # | |
| Show t => Show (Basic t) Source # | |
| Nominal (Basic t) Source # | |
Defined in Nominal.Nominal | |
| NominalSupport (Basic t) Source # | |
| Show t => NominalShow (Basic t) Source # | |
Defined in Nominal.NominalShow | |
| Bindable (Basic t) Source # | |
Defined in Nominal.Bindable | |
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.
Methods
gbullet :: NominalPermutation -> f a -> f a Source #
Instances
| GNominal (V1 :: Type -> Type) Source # | |
Defined in Nominal.Nominal | |
| GNominal (U1 :: Type -> Type) Source # | |
Defined in Nominal.Nominal | |
| Nominal a => GNominal (K1 i a :: Type -> Type) Source # | |
Defined in Nominal.Nominal | |
| (GNominal a, GNominal b) => GNominal (a :+: b) Source # | |
Defined in Nominal.Nominal | |
| (GNominal a, GNominal b) => GNominal (a :*: b) Source # | |
Defined in Nominal.Nominal | |
| GNominal a => GNominal (M1 i c a) Source # | |
Defined in Nominal.Nominal | |