Copyright	(c) Murdoch J. Gabbay 2020
License	GPL-3
Maintainer	murdoch.gabbay@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Language.Nominal.Sub

Contents

Substitution
Test
Orphan instances

Description

Typeclass for types that support a substitution action. Capture-avoidance is automatic, provided you used Nom or Abs types for binding, of course.

See Language.Nominal.Examples.SystemF for usage examples.

Synopsis

class KSub n x y where
- sub :: n -> x -> y -> y
type Sub n x y = KSub (KName Tom n) x y

Substitution

class KSub n x y where Source #

Substitution. sub n x y corresponds to "substitute the name n for the datum x in y".

We intend that n should be a type of names KName k n.

Minimal complete definition

Nothing

Methods

sub :: n -> x -> y -> y Source #

sub :: (Generic y, GSub n x (Rep y)) => n -> x -> y -> y Source #

Instances

KSub n x Char Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> Char -> Char Source #
KSub n x () Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> () -> () Source #
KSub n x Int Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> Int -> Int Source #
KSub n x Bool Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> Bool -> Bool Source #
KSub Var Exp Exp Source #	Substitution. Capture-avoidance is automatic.
Instance details Defined in Language.Nominal.Examples.UntypedLambda Methods sub :: Var -> Exp -> Exp -> Exp Source #
KSub NTrm Trm Trm Source #	Substitute term variable with term in term
Instance details Defined in Language.Nominal.Examples.SystemF Methods sub :: NTrm -> Trm -> Trm -> Trm Source #
KSub NTyp Typ Trm Source #
Instance details Defined in Language.Nominal.Examples.SystemF Methods sub :: NTyp -> Typ -> Trm -> Trm Source #
KSub NTyp Typ NTrm Source #	Substitute type variables with type in term variable. Non-trivial because a term variable carries a label which contains a type. Action is functorial, descending into the type label.
Instance details Defined in Language.Nominal.Examples.SystemF Methods sub :: NTyp -> Typ -> NTrm -> NTrm Source #
KSub NTyp Typ Typ Source #	Substitution acts on type variables. Capture-avoidance is automagical.
Instance details Defined in Language.Nominal.Examples.SystemF Methods sub :: NTyp -> Typ -> Typ -> Typ Source #
KSub V Operand Prog Source #	Substitution on `Prog`rams is generic
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Prog -> Prog Source #
KSub V Operand Operand Source #	Substitution as standard on `Operand`
Instance details Defined in Language.Nominal.Examples.Assembly2 Methods sub :: V -> Operand -> Operand -> Operand Source #
KSub V Operand Prog Source #	Substitution on `Prog`rams is generic
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods sub :: V -> Operand -> Prog -> Prog Source #
KSub V Operand Operand Source #	Substitution as standard on `Operand`
Instance details Defined in Language.Nominal.Examples.Assembly1 Methods sub :: V -> Operand -> Operand -> Operand Source #
KSub n x a => KSub n x (Maybe a) Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> Maybe a -> Maybe a Source #
KSub n x a => KSub n x (NonEmpty a) Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> NonEmpty a -> NonEmpty a Source #
KSub n x a => KSub n x [a] Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> [a] -> [a] Source #
KSub n x (Nameless a) Source #	sub on nameless type is trivial
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> Nameless a -> Nameless a Source #
(KSub n x a, KSub n x b) => KSub n x (Either a b) Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> Either a b -> Either a b Source #
(KSub n x a, KSub n x b) => KSub n x (a, b) Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> (a, b) -> (a, b) Source #
(KSub n x a, KSub n x b, KSub n x c) => KSub n x (a, b, c) Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> (a, b, c) -> (a, b, c) Source #
(KSub n x a, KSub n x b, KSub n x c, KSub n x d) => KSub n x (a, b, c, d) Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> (a, b, c, d) -> (a, b, c, d) Source #
(KSub n x a, KSub n x b, KSub n x c, KSub n x d, KSub n x e) => KSub n x (a, b, c, d, e) Source #
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> x -> (a, b, c, d, e) -> (a, b, c, d, e) Source #
Eq n => KSub n ((n -> a) -> a) ((n -> a) -> a) Source #	Placeholder for future development. A general maths behind this definition is given in Section 8.1 of Definition 8.12 of Semantics Out Of Context (author's pdf).
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> ((n -> a) -> a) -> ((n -> a) -> a) -> (n -> a) -> a Source #
Eq n => KSub n ((n -> a) -> a) (n -> a) Source #	Placeholder for future development. A general maths behind this definition is given in Section 8.1 of Semantics Out Of Context (author's pdf).
Instance details Defined in Language.Nominal.Sub Methods sub :: n -> ((n -> a) -> a) -> (n -> a) -> n -> a Source #
(Typeable s, Typeable u, KSub (KName s n) x t, KSub (KName s n) x y, Swappable t, Swappable y) => KSub (KName s n) x (KAbs (KName u t) y) Source #	sub on a nominal abstraction substitutes in the label, and substitutes capture-avoidingly in the body
Instance details Defined in Language.Nominal.Sub Methods sub :: KName s n -> x -> KAbs (KName u t) y -> KAbs (KName u t) y Source #
KSub (KName s n) (KName s n) (KName s n) Source #	sub on names
Instance details Defined in Language.Nominal.Sub Methods sub :: KName s n -> KName s n -> KName s n -> KName s n Source #

type Sub n x y = KSub (KName Tom n) x y Source #

Canonical instance for the unit atom sort

Test

Orphan instances

(Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => BinderConc (KAbs (KName s n) y) (KName s n) y s x Source #	Nameless form of substitution, where the name for which we substitute is packaged in a `KAbs` abstraction.
Instance details Methods conc :: KAbs (KName s n) y -> x -> y Source # cnoc :: x -> KAbs (KName s n) y -> y Source #