Unbound.Generics.LocallyNameless.Subst

A typeclass for types that may participate in capture-avoiding substitution

The minimal definition is empty, provided your type is an instance of Generic

 type Var = Name Factor
 data Expr = SumOf [Summand]
           deriving (Show, Generic)
 data Summand = ProductOf [Factor]
           deriving (Show, Generic)
 instance Subst Var Expr
 instance Subst Var Summand

The default instance just propagates the substitution into the constituent factors.

If you identify the variable occurrences by implementing the isvar function, the derived subst function will be able to substitute a factor for a variable.

 data Factor = V Var
             | C Int
             | Subexpr Expr
           deriving (Show, Generic)
 instance Subst Var Factor where
   isvar (V v) = Just (SubstName v)
   isvar _     = Nothing

Documentation

data SubstName a b where

See isVar

Constructors

SubstName :: a ~ b => Name a -> SubstName a b

data SubstCoerce a b where

See isCoerceVar

Constructors

SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b

class Subst b a where

Instances of Subst b a are terms of type a that may contain variables of type b that may participate in capture-avoiding substitution.

Methods

isvar :: a -> Maybe (SubstName a b)

This is the only method that must be implemented

isCoerceVar :: a -> Maybe (SubstCoerce a b)

This is an alternative version to isvar, useable in the case that the substituted argument doesn't have *exactly* the same type as the term it should be substituted into. The default implementation always returns Nothing.

subst :: Name b -> b -> a -> a

subst nm e tm substitutes e for nm in tm. It has a default generic implementation in terms of isvar

substs :: [(Name b, b)] -> a -> a

Instances

Subst b AnyName

Subst b Integer

Subst b Double

Subst b Float

Subst b Char

Subst b ()

Subst b Bool

Subst b Int

(Alpha p, Subst c p) => Subst c (TRec p)

Subst c p => Subst c (Rec p)

Subst c a => Subst c (Embed a)

Generic a => Subst b (Name a)

Subst c a => Subst c (Maybe a)

Subst c a => Subst c [a]

(Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)

(Subst c a, Subst c b) => Subst c (Either a b)

(Subst c a, Subst c b) => Subst c (a, b)

(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d)

(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e)

(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f)