hydra.reduction module
Functions for reducing terms and types, i.e. performing computations.
- hydra.reduction.alpha_convert(vold: Name, vnew: Name, term: Term) Term
Alpha convert a variable in a term.
- hydra.reduction.beta_reduce_type(cx: T0, graph: Graph, typ: Type) object
Eagerly beta-reduce a type by substituting type arguments into type lambdas.
- hydra.reduction.contract_term(term: Term) Term
- Apply the special rules:
((x.e1) e2) == e1, where x does not appear free in e1
- and
((x.e1) e2) = e1[x/e2]
These are both limited forms of beta reduction which help to “clean up” a term without fully evaluating it.
- hydra.reduction.eta_expand_term(tx0: Graph, term0: Term) Term
Recursively transform terms to eliminate partial application, e.g. ‘add 42’ becomes ‘x.add 42 x’. Uses the Graph to look up types for arity calculation. Bare primitives and variables are NOT expanded; eliminations and partial applications are. This version properly tracks the Graph through nested scopes.
- hydra.reduction.eta_expand_typed_term(cx: InferenceContext, tx0: Graph, term0: Term) object
Recursively transform arbitrary terms like ‘add 42’ into terms like ‘x.add 42 x’, eliminating partial application. Variable references are not expanded. This is useful for targets like Python with weaker support for currying than Hydra or Haskell. Note: this is a “trusty” function which assumes the graph is well-formed, i.e. no dangling references. It also assumes that type inference has already been performed. After eta expansion, type inference needs to be performed again, as new, untyped lambdas may have been added.
- hydra.reduction.eta_expansion_arity(graph: Graph, term: Term) int
Calculate the arity for eta expansion Note: this is a “trusty” function which assumes the graph is well-formed, i.e. no dangling references.
- hydra.reduction.eta_reduce_term(term: Term) Term
Eta-reduce a term by removing redundant lambda abstractions.
- hydra.reduction.reduce_term(cx: T0, graph: Graph, eager: bool, term: Term) object
A term evaluation function which is alternatively lazy or eager.