| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Nominal.Nominal
Contents
Description
- 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.
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 # | |
| 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 #
Pattern matching for atom abstraction. In an ideal programming idiom, we would be able to define a function on atom abstractions like this:
f (x.s) = body.
Haskell doesn't let us provide this syntax, but the open function
provides the equivalent syntax
f t = open t (\x s -> body).
To be referentially transparent and equivariant, the body is
subject to the same restriction as with_fresh, namely,
x must be fresh for the body (in symbols x # body).
atom_merge :: (Nominal t, Nominal s) => BindAtom t -> BindAtom s -> BindAtom (t, s) Source #
Sometimes, it is necessary to open two abstractions, using the same fresh name for both of them. An example of this is the typing rule for lambda abstraction in dependent type theory:
Gamma, x:t |- e : s
------------------------------------
Gamma |- Lam (x.e) : Pi t (x.s)In the bottom-up reading of this rule, we are given the terms Lam
body and Pi t body', and we require a fresh name x and
terms e, s such that body = (x.e) and body' =
(x.s). Crucially, the same atom x should be used in both e
and s, because we subsequently need to check that e has type
s in some scope that is common to e and s.
The merge primitive permits us to deal with such situations. Its
defining property is
merge (x.e) (x.s) = (x.(e,s)).
We can therefore solve the above problem:
open (merge body body') (\x (e,s) -> .....)
Moreover, the merge primitive can be used to define other
merge-like functionality. For example, it is easy to define a
function
merge_list :: (Atomic a, Nominal t) => [Bind a t] -> Bind a [t]
in terms of it.
Semantically, the merge operation implements the isomorphism of
nominal sets [A]T x [A]S = [A](T x S).
If x and y are atoms with user-suggested concrete names and
(z.(t',s')) = merge (x.t) (y.s),
then z will be preferably given the concrete name of x, but the concrete name of y will be used if the name of x would cause a clash.
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, and Float, 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 |
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.