Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

Abstract binding trees with a nameless internal representation.

- data Term v f
- pattern Var :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => v -> Term v f
- pattern Abs :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => v -> Term v f -> Term v f
- pattern Pat :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => f (Term v f) -> Term v f
- subst :: (Functor f, Foldable f, Ord v) => (v -> Maybe (Term v f)) -> Term v f -> Term v f
- substMap :: (Functor f, Foldable f, Ord v) => Map v (Term v f) -> Term v f -> Term v f
- subst1 :: (Functor f, Foldable f, Ord v) => (v, Term v f) -> Term v f -> Term v f
- freeVars :: Term v f -> Set v
- class Eq v => Freshen v where
- data View v f x
- fold :: (Foldable f, Functor f, Ord v) => View v f (Term v f) -> Term v f
- unfold :: (Foldable f, Functor f, Ord v, Freshen v) => Term v f -> View v f (Term v f)

# Abstract binding tree terms

Abstract binding trees take the form

, or, more commonly, `Term`

v f a

. These
types are abstract—you will never construct or analyze them directly.`Flat`

v f

An abstract

is an abstract binding tree of the shape described
by the pattern functor `Term`

v f`f`

augmented with variables named by `v`

. Equality is
alpha-equivalence. In particular,

is (morally) equivalent to the
fixed-point of the pattern-algebra `Term`

v f`View`

respecting the binding
properties of `VAbs`

and `VVar`

.

# Constructing terms with `View`

patterns

To construct or analyze a `Term`

, the `Var`

, `Abs`

, and `Pat`

pattern synonyms are useful.
These synonyms let you essentially treat `Term`

as if it weren't abstract and both construct
new terms and `case`

analyze them.

pattern Abs :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => v -> Term v f -> Term v f Source #

pattern Pat :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => f (Term v f) -> Term v f Source #

# Working with free variables

Abstract binding trees take the form

, or, more commonly, `Term`

v f a

. These
types are abstract---you will never construct or analyze them directly.`Flat`

v f

subst :: (Functor f, Foldable f, Ord v) => (v -> Maybe (Term v f)) -> Term v f -> Term v f Source #

Substitute some free variables.

substMap :: (Functor f, Foldable f, Ord v) => Map v (Term v f) -> Term v f -> Term v f Source #

Substitute some free variables from a finite map.

subst1 :: (Functor f, Foldable f, Ord v) => (v, Term v f) -> Term v f -> Term v f Source #

Substitute just one free variable.

freeVars :: Term v f -> Set v Source #

Returns the free variables used within a given `Term`

.

NOTE: We have to define a new function in order to not accidentally break
encapsulation. Just exporting `free`

direction would allow uses to manipulate
the Term value and break invariants (!).

# Freshen class

class Eq v => Freshen v where Source #

A type which can be freshened has an operation which attempts to find a
unique version of its input. The principal thing that must hold is that
`freshen n /= n`. It's not necessary that `freshen n` be totally fresh with
respect to a context---that's too much to ask of a value---but it is
necessary that `freshen`

*eventually* produces a fresh value.

Variable identifier types must be instances of Freshen.