Zabt

Abstract binding trees with a nameless internal representation.

Abstract binding tree terms

Abstract binding trees take the form Term v f a, or, more commonly, Flat v f. These types are abstract—you will never construct or analyze them directly.

data Term v f a

An abstract Term v f is an abstract binding tree of the shape described by the pattern functor f augmented with variables named by v. Equality is alpha-equivalence. In particular, Term v f is (morally) equivalent to the fixed-point of the pattern-algebra View respecting the binding properties of 'Zabt.View.VAbs and VVar.

Instances

(Eq v, Eq (f (Term v f)), Eq (Term v f a)) => Eq (Term v f (B a))

Methods

(==) :: Term v f (B a) -> Term v f (B a) -> Bool

(/=) :: Term v f (B a) -> Term v f (B a) -> Bool

(Eq v, Eq (f (Term v f))) => Eq (Term v f G)

Methods

(==) :: Term v f G -> Term v f G -> Bool

(/=) :: Term v f G -> Term v f G -> Bool

(Ord v, Ord (f (Term v f)), Ord (Term v f a)) => Ord (Term v f (B a))

Methods

compare :: Term v f (B a) -> Term v f (B a) -> Ordering

(<) :: Term v f (B a) -> Term v f (B a) -> Bool

(<=) :: Term v f (B a) -> Term v f (B a) -> Bool

(>) :: Term v f (B a) -> Term v f (B a) -> Bool

(>=) :: Term v f (B a) -> Term v f (B a) -> Bool

max :: Term v f (B a) -> Term v f (B a) -> Term v f (B a)

min :: Term v f (B a) -> Term v f (B a) -> Term v f (B a)

(Ord v, Ord (f (Term v f))) => Ord (Term v f G)

Methods

compare :: Term v f G -> Term v f G -> Ordering

(<) :: Term v f G -> Term v f G -> Bool

(<=) :: Term v f G -> Term v f G -> Bool

(>) :: Term v f G -> Term v f G -> Bool

(>=) :: Term v f G -> Term v f G -> Bool

max :: Term v f G -> Term v f G -> Term v f G

min :: Term v f G -> Term v f G -> Term v f G

(Show v, Show (Nameless v f (Term v f) a)) => Show (Term v f a)

Methods

showsPrec :: Int -> Term v f a -> ShowS

show :: Term v f a -> String

showList :: [Term v f a] -> ShowS

type Flat v f = Term v f G

A Flat Term is one which is not immediately binding any variables.

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 Var :: forall f v a. (Visits f, Freshen v, Ord v) => (~#) Arity Arity a G => v -> Term v f a

Var v creates and matches a Term value corresponding to a free variable.

pattern Abs :: forall f v a. (Visits f, Freshen v, Ord v) => forall a1. (~#) Arity Arity a (B a1) => v -> Term v f a1 -> Term v f a

Abs v t creates and matches a Term value where the free variable v has been abstracted over, becoming bound.

pattern Pat :: forall f v a. (Visits f, Freshen v, Ord v) => (~#) Arity Arity a G => f (Term v f) -> Term v f a

Pat f creates and matches a Term value built from a layer of the pattern functor f.

Basic arities

When defining a pattern functor for Terms you have to declare the arities of each recursive use.

data Arity

Constructors

G

B Arity

type B a = B a

type G = G

type A0 = G

type A1 = B G

type A2 = B A1

type A3 = B A2

type family DownTo (c :: * -> Constraint) (x :: Arity -> *) (a :: Arity) :: Constraint where ...

The DownTo type family makes it easier to declare type constraints over families of arities.

Equations

DownTo c x G = c (x G)

DownTo c x (B a) = (c (x (B a)), DownTo c x a)

class Visits t where

A type f :: Arity -> * instantiating Visits f essentially is Traversable, but we define a new typeclass to handle the difference in types.

Minimal complete definition

visit

Methods

visit :: Applicative f => (forall a. x a -> f (y a)) -> t x -> f (t y)

vmap :: (forall a. x a -> y a) -> t x -> t y

vfoldMap :: Monoid m => (forall a. x a -> m) -> t x -> m

Working with free variables

Abstract binding trees take the form Term v f a, or, more commonly, Flat v f. These types are abstract---you will never construct or analyze them directly.

subst :: forall v f a. (Visits f, Ord v) => (v -> Maybe (Flat v f)) -> Term v f a -> Term v f a

Substitute some free variables.

substMap :: forall v f a. (Visits f, Ord v) => Map v (Flat v f) -> Term v f a -> Term v f a

Substitute some free variables from a finite map.

subst1 :: forall v f a. (Visits f, Ord v) => (v, Flat v f) -> Term v f a -> Term v f a

Substitute just one free variable.

freeVars :: Term v f a -> Set v

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

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.

Minimal complete definition

freshen

Methods

freshen :: v -> v

Instances

Freshen Int

Methods

freshen :: Int -> Int

Freshen Index

Methods

freshen :: Index -> Index

Freshen Name

Methods

freshen :: Name -> Name

View in detail

data View v f x a where

Constructors

VVar :: !v -> View v f x G

VPat :: f x -> View v f x G

VAbs :: !v -> x a -> View v f x (B a)

Instances

(Eq (x a), Eq (f x)) => Eq (View v f x (B a))

Alpha-equivalence

Methods

(==) :: View v f x (B a) -> View v f x (B a) -> Bool

(/=) :: View v f x (B a) -> View v f x (B a) -> Bool

(Eq v, Eq (f x)) => Eq (View v f x G)

Alpha-equivalence

Methods

(==) :: View v f x G -> View v f x G -> Bool

(/=) :: View v f x G -> View v f x G -> Bool

(Ord v, Ord (x a), Ord (f x)) => Ord (View v f x (B a))

Methods

compare :: View v f x (B a) -> View v f x (B a) -> Ordering

(<) :: View v f x (B a) -> View v f x (B a) -> Bool

(<=) :: View v f x (B a) -> View v f x (B a) -> Bool

(>) :: View v f x (B a) -> View v f x (B a) -> Bool

(>=) :: View v f x (B a) -> View v f x (B a) -> Bool

max :: View v f x (B a) -> View v f x (B a) -> View v f x (B a)

min :: View v f x (B a) -> View v f x (B a) -> View v f x (B a)

(Ord v, Ord (f x)) => Ord (View v f x G)

Methods

compare :: View v f x G -> View v f x G -> Ordering

(<) :: View v f x G -> View v f x G -> Bool

(<=) :: View v f x G -> View v f x G -> Bool

(>) :: View v f x G -> View v f x G -> Bool

(>=) :: View v f x G -> View v f x G -> Bool

max :: View v f x G -> View v f x G -> View v f x G

min :: View v f x G -> View v f x G -> View v f x G

(Show v, Show (x a), Show (f x)) => Show (View v f x (B a))

Methods

showsPrec :: Int -> View v f x (B a) -> ShowS

show :: View v f x (B a) -> String

showList :: [View v f x (B a)] -> ShowS

(Show v, Show (x G), Show (f x)) => Show (View v f x G)

Methods

showsPrec :: Int -> View v f x G -> ShowS

show :: View v f x G -> String

showList :: [View v f x G] -> ShowS

fold :: (Visits f, Ord v) => View v f (Term v f) a -> Term v f a

unfold :: (Visits f, Ord v, Freshen v) => Term v f a -> View v f (Term v f) a