Copyright | Copyright (c) 2016 the Hakaru team |
---|---|

License | BSD3 |

Maintainer | wren@community.haskell.org |

Stability | experimental |

Portability | GHC-only |

Safe Haskell | None |

Language | Haskell2010 |

The interface for abstract binding trees. Given the generating
functor `Term`

: the non-recursive `View`

type extends `Term`

by
adding variables and binding; and each `ABT`

type (1) provides
some additional annotations at each recursion site, and then (2)
ties the knot to produce the recursive trees. For an introduction
to this technique/approach, see:

- module Language.Hakaru.Syntax.Variable
- resolveVar :: (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), ABT syn abt) => abt '[] (a :: k) -> Assocs (abt '[]) -> Either (Variable a) (syn abt a)
- data View :: (k -> *) -> [k] -> k -> * where
- unviewABT :: ABT syn abt => View (syn abt) xs a -> abt xs a
- class ABT syn abt | abt -> syn where
- caseVarSyn :: ABT syn abt => abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
- binds :: ABT syn abt => List1 Variable xs -> abt ys b -> abt (xs ++ ys) b
- binds_ :: ABT syn abt => List1 Variable xs -> abt '[] b -> abt xs b
- caseBinds :: ABT syn abt => abt xs a -> (List1 Variable xs, abt '[] a)
- underBinders :: ABT syn abt => (abt '[] a -> abt '[] b) -> abt xs a -> abt xs b
- maxNextFree :: (ABT syn abt, Foldable f) => f (Some2 abt) -> Nat
- maxNextBind :: (ABT syn abt, Foldable f) => f (Some2 abt) -> Nat
- maxNextFreeOrBind :: (ABT syn abt, Foldable f) => f (Some2 abt) -> Nat
- rename :: forall syn abt a xs b. (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn, ABT syn abt) => Variable a -> Variable a -> abt xs b -> abt xs b
- renames :: forall syn abt xs a. (ABT syn abt, JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn) => Assocs (Variable :: k -> *) -> abt xs a -> abt xs a
- subst :: forall syn abt a xs b. (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn, ABT syn abt) => Variable a -> abt '[] a -> abt xs b -> abt xs b
- substs :: forall syn abt xs a. (ABT syn abt, JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn) => Assocs (abt '[]) -> abt xs a -> abt xs a
- binder :: ABT syn abt => Text -> Sing a -> (abt '[] a -> abt xs b) -> abt (a ': xs) b
- withMetadata :: meta -> MetaABT meta syn xs a -> MetaABT meta syn xs a
- cataABT :: forall abt syn r. (ABT syn abt, Functor21 syn) => (forall a. Variable a -> r '[] a) -> (forall x xs a. Variable x -> r xs a -> r (x ': xs) a) -> (forall a. syn r a -> r '[] a) -> forall xs a. abt xs a -> r xs a
- paraABT :: forall abt syn r. (ABT syn abt, Functor21 syn) => (forall a. Variable a -> r '[] a) -> (forall x xs a. Variable x -> abt xs a -> r xs a -> r (x ': xs) a) -> (forall a. syn (Pair2 abt r) a -> r '[] a) -> forall xs a. abt xs a -> r xs a
- data TrivialABT syn xs a
- data MemoizedABT syn xs a
- data MetaABT meta syn xs a = MetaABT {
- getMetadata :: !(Maybe meta)
- metaView :: !(View (syn (MetaABT meta syn)) xs a)

# Our basic notion of variables.

resolveVar :: (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), ABT syn abt) => abt '[] (a :: k) -> Assocs (abt '[]) -> Either (Variable a) (syn abt a) Source #

If the expression is a variable, then look it up. Recursing until we can finally return some syntax.

# The abstract binding tree interface

data View :: (k -> *) -> [k] -> k -> * where Source #

The raw view of abstract binding trees, to separate out variables
and binders from (1) the rest of syntax (cf., `Term`

), and (2)
whatever annotations (cf., the `ABT`

instances).

The first parameter gives the generating signature for the signature. The second index gives the number and types of locally-bound variables. And the final parameter gives the type of the whole expression.

HACK: We only want to expose the patterns generated by this type, not the constructors themselves. That way, callers must use the smart constructors of the ABT class. But if we don't expose this type, then clients can't define their own ABT instances (without reinventing their own copy of this type)...

class ABT syn abt | abt -> syn where Source #

The class interface for abstract binding trees. The first
argument, `syn`

, gives the syntactic signature of the ABT;
whereas, the second argument, `abt`

, is thing being declared as
an ABT for `syn`

. The first three methods (`syn`

, `var`

, `bind`

)
alow us to inject any `View`

into the `abt`

. The other methods
provide various views for extracting information from the `abt`

.

At present we're using fundeps in order to restrict the relationship
between `abt`

and `syn`

. However, in the future we may move `syn`

into being an associated type, if that helps to clean things up
(since fundeps and type families don't play well together). The
idea behind the fundep is that certain `abt`

implementations may
only be able to work for particular `syn`

signatures. This isn't
the case for `TrivialABT`

nor `MemoizedABT`

, but isn't too
far-fetched.

syn :: syn abt a -> abt '[] a Source #

var :: Variable a -> abt '[] a Source #

bind :: Variable a -> abt xs b -> abt (a ': xs) b Source #

caseBind :: abt (x ': xs) a -> (Variable x -> abt xs a -> r) -> r Source #

Since the first argument to `abt`

is not `'[]`

, we know
it must be `Bind`

. So we do case analysis on that constructor,
pushing the annotation down one binder (but not over the
whole recursive `View`

layer).

viewABT :: abt xs a -> View (syn abt) xs a Source #

freeVars :: abt xs a -> VarSet (KindOf a) Source #

nextFree :: abt xs a -> Nat Source #

Return the successor of the largest `varID`

of *free*
variables. Thus, if there are no free variables we return
zero. The default implementation is to take the successor
of the maximum of `freeVars`

. This is part of the class in
case you want to memoize it.

This function is used in order to generate guaranteed-fresh variables without the need for a name supply. In particular, it's used to ensure that the generated variable don't capture any free variables in the term.

nextBind :: abt xs a -> Nat Source #

Return the successor of the largest `varID`

of variable
*binding sites* (i.e., of variables bound by the `Bind`

constructor). Thus, if there are no binders, then we will
return zero. N.B., this should return zero for *uses* of the
bound variables themselves. This is part of the class in
case you want to memoize it.

This function is used in order to generate guaranteed-fresh variables without the need for a name supply. In particular, it's used to ensure that the generated variable won't be captured or shadowed by bindings already in the term.

nextFreeOrBind :: abt xs a -> Nat Source #

Return the maximum of `nextFree`

and `nextBind`

. For when
you want to be really paranoid about choosing new variable
IDs. In principle this shouldn't be necessary since we should
always freshen things when going under binders; but for some
reason only using `nextFree`

keeps leading to bugs in
transformations like disintegration and expectation.

*N.B.*, it is impossible to implement this function such
that it is lazy in the bound variables like `nextBind`

is.
Thus, it cannot be used for knot-tying tricks like `nextBind`

can.

(JmEq1 k (Sing k), Show1 k (Sing k), Foldable21 k k [k] syn) => ABT k syn (MemoizedABT k syn) Source # | |

(JmEq1 k (Sing k), Show1 k (Sing k), Foldable21 k k [k] syn) => ABT k syn (TrivialABT k syn) Source # | |

(JmEq1 k (Sing k), Show1 k (Sing k), Foldable21 k k [k] syn) => ABT k syn (MetaABT k meta syn) Source # | |

caseVarSyn :: ABT syn abt => abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r Source #

binds :: ABT syn abt => List1 Variable xs -> abt ys b -> abt (xs ++ ys) b Source #

Call `bind`

repeatedly.

binds_ :: ABT syn abt => List1 Variable xs -> abt '[] b -> abt xs b Source #

A specialization of `binds`

for when `ys ~ '[]`

. We define
this to avoid the need for using `eqAppendIdentity`

on the result
of `binds`

itself.

underBinders :: ABT syn abt => (abt '[] a -> abt '[] b) -> abt xs a -> abt xs b Source #

Transform expression under binds

maxNextFree :: (ABT syn abt, Foldable f) => f (Some2 abt) -> Nat Source #

Call `nextFree`

on all the terms and return the maximum.

maxNextBind :: (ABT syn abt, Foldable f) => f (Some2 abt) -> Nat Source #

Call `nextBind`

on all the terms and return the maximum.

maxNextFreeOrBind :: (ABT syn abt, Foldable f) => f (Some2 abt) -> Nat Source #

Call `nextFreeOrBind`

on all the terms and return the maximum.

## Capture avoiding substitution for any `ABT`

rename :: forall syn abt a xs b. (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn, ABT syn abt) => Variable a -> Variable a -> abt xs b -> abt xs b Source #

Rename a free variable. Does nothing if the variable is bound.

renames :: forall syn abt xs a. (ABT syn abt, JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn) => Assocs (Variable :: k -> *) -> abt xs a -> abt xs a Source #

subst :: forall syn abt a xs b. (JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn, ABT syn abt) => Variable a -> abt '[] a -> abt xs b -> abt xs b Source #

Perform capture-avoiding substitution. This function will
either preserve type-safety or else throw an `VarEqTypeError`

(depending on which interpretation of `varEq`

is chosen). N.B.,
to ensure timely throwing of exceptions, the `Term`

and `ABT`

should have strict `fmap21`

definitions.

substs :: forall syn abt xs a. (ABT syn abt, JmEq1 (Sing :: k -> *), Show1 (Sing :: k -> *), Functor21 syn) => Assocs (abt '[]) -> abt xs a -> abt xs a Source #

The parallel version of `subst`

for performing multiple substitutions at once.

## Constructing first-order trees with a HOAS-like API

:: ABT syn abt | |

=> Text | The variable's name hint |

-> Sing a | The variable's type |

-> (abt '[] a -> abt xs b) | Build the binder's body from a variable |

-> abt (a ': xs) b |

A combinator for defining a HOAS-like API for our syntax.
Because our `Term`

is first-order, we cannot actually have any
exotic terms in our language. In principle, this function could
be used to do exotic things when constructing those non-exotic
terms; however, trying to do anything other than change the
variable's name hint will cause things to explode (since it'll
interfere with our tying-the-knot).

N.B., if you manually construct free variables and use them in
the body (i.e., via `var`

), they may become captured by the new
binding introduced here! This is inevitable since `nextBind`

never looks at variable *use sites*; it only ever looks at
*binding sites*. On the other hand, if you manually construct a
bound variable (i.e., manually calling `bind`

yourself), then
the new binding introduced here will respect the old binding and
avoid that variable ID.

### Highly experimental

withMetadata :: meta -> MetaABT meta syn xs a -> MetaABT meta syn xs a Source #

## Abstract nonsense

cataABT :: forall abt syn r. (ABT syn abt, Functor21 syn) => (forall a. Variable a -> r '[] a) -> (forall x xs a. Variable x -> r xs a -> r (x ': xs) a) -> (forall a. syn r a -> r '[] a) -> forall xs a. abt xs a -> r xs a Source #

The catamorphism (aka: iterator) for ABTs. While this is
equivalent to `paraABT`

in terms of the definable *functions*,
it is weaker in terms of definable *algorithms*. If you need
access to (subterms of) the original ABT, it is more efficient
to use `paraABT`

than to rebuild them. However, if you never
need access to the original ABT, then this function has somewhat
less overhead.

paraABT :: forall abt syn r. (ABT syn abt, Functor21 syn) => (forall a. Variable a -> r '[] a) -> (forall x xs a. Variable x -> abt xs a -> r xs a -> r (x ': xs) a) -> (forall a. syn (Pair2 abt r) a -> r '[] a) -> forall xs a. abt xs a -> r xs a Source #

The paramorphism (aka: recursor) for ABTs. While this is
equivalent to `cataABT`

in terms of the definable *functions*,
it is stronger in terms of definable *algorithms*. If you need
access to (subterms of) the original ABT, it is more efficient
to use this function than to use `cataABT`

and rebuild them.
However, if you never need access to the original ABT, then
`cataABT`

has somewhat less overhead.

The provided type is slightly non-uniform since we inline (i.e.,
curry) the definition of `Pair2`

in the type of the `bind_`

argument. But we can't inline `Pair2`

away in the type of the
`syn_`

argument. N.B., if you treat the second component of the
`Pair2`

(either the real ones or the curried ones) lazily, then
this is a top-down function; however, if you treat them strictly
then it becomes a bottom-up function.

# Some ABT instances

data TrivialABT syn xs a Source #

A trivial ABT with no annotations.

The `Show`

instance does not expose the raw underlying data
types, but rather prints the smart constructors `var`

, `syn`

,
and `bind`

. This makes things prettier, but also means that if
you paste the string into a Haskell file you can use it for any
`ABT`

instance.

The `freeVars`

, `nextFree`

, and `nextBind`

methods are all very
expensive for this ABT, because we have to traverse the term
every time we want to call them. The `MemoizedABT`

implementation
fixes this.

(JmEq1 k (Sing k), Show1 k (Sing k), Foldable21 k k [k] syn) => ABT k syn (TrivialABT k syn) Source # | |

(Show1 k (Sing k), Show1 k (syn (TrivialABT k syn))) => Show2 k [k] (TrivialABT k syn) Source # | |

(Show1 k (Sing k), Show1 k (syn (TrivialABT k syn))) => Show1 k (TrivialABT k syn xs) Source # | |

(Show1 k (Sing k), Show1 k (syn (TrivialABT k syn))) => Show (TrivialABT k syn xs a) Source # | |

data MemoizedABT syn xs a Source #

An ABT which memoizes `freeVars`

, `nextBind`

, and `nextFree`

,
thereby making them take only *O(1)* time.

N.B., the memoized set of free variables is lazy so that we can
tie-the-knot in `binder`

without interfering with our memos. The
memoized `nextFree`

must be lazy for the same reason.

(JmEq1 k (Sing k), Show1 k (Sing k), Foldable21 k k [k] syn) => ABT k syn (MemoizedABT k syn) Source # | |

(Show1 k (Sing k), Show1 k (syn (MemoizedABT k syn))) => Show2 k [k] (MemoizedABT k syn) Source # | |

(Show1 k (Sing k), Show1 k (syn (MemoizedABT k syn))) => Show1 k (MemoizedABT k syn xs) Source # | |

(Show1 k (Sing k), Show1 k (syn (MemoizedABT k syn))) => Show (MemoizedABT k syn xs a) Source # | |

data MetaABT meta syn xs a Source #

An ABT which carries around metadata at each node.

Right now this essentially inlines the the TrivialABT instance but it would be nice if it was abstract in the choice of ABT.

(JmEq1 k (Sing k), Show1 k (Sing k), Foldable21 k k [k] syn) => ABT k syn (MetaABT k meta syn) Source # | |

(Show1 k (Sing k), Show1 k (syn (MetaABT k meta syn)), Show meta) => Show2 k [k] (MetaABT k meta syn) Source # | |

(Show1 k (Sing k), Show1 k (syn (MetaABT k meta syn)), Show meta) => Show1 k (MetaABT k meta syn xs) Source # | |

(Show1 k (Sing k), Show1 k (syn (MetaABT k meta syn)), Show meta) => Show (MetaABT k meta syn xs a) Source # | |