Data.Comp.MultiParam.FreshM

This module defines a monad for generating fresh, abstract variables, useful e.g. for defining equality on terms.

Documentation

data FreshM a

Monad for generating fresh (abstract) variables.

Instances

Monad FreshM

data Var i

Abstract notion of a variable (the constructor is hidden).

Instances

PShow Var

PEq Var

POrd Var

(ShowHD f, PShow a) => PShow (Cxt h f Var a)

From an ShowHD higher-order difunctor an ShowHD instance of the corresponding term type can be derived.

(EqHD f, PEq a) => PEq (Cxt h f Var a)

(OrdHD f, POrd a) => POrd (Cxt h f Var a)

varEq :: Var i -> Var j -> Bool

Equality on variables.

varCompare :: Var i -> Var j -> Ordering

Ordering of variables.

varShow :: Var i -> String

Printing of variables.

genVar :: FreshM (Var i)

Generate a fresh variable.

varCoerce :: Var i -> Var j

Change the type of a variable.

evalFreshM :: FreshM a -> a

Evaluate a computation that uses fresh variables.