Package hydra

Interface Reduction

  • public interface Reduction
    Functions for reducing terms and types, i.e. performing computations.

    • Method Summary

      Static Methods 
      Modifier and Type Method Description
      static Term alphaConvert​(Name vold, Name vnew, Term term)
      Alpha convert a variable in a term
      static <T0> Either<Error_,​Type> betaReduceType​(T0 cx, Graph graph, Type typ)
      Eagerly beta-reduce a type by substituting type arguments into type lambdas
      static <T1> Either<Error_,​Type> betaReduceType_mapExpr​(java.util.function.Function<ApplicationType,​Either<Error_,​Type>> reduceApp, java.util.function.Function<T1,​Either<Error_,​Type>> recurse, T1 t)  
      static Term contractTerm​(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.
      static <T0> Term contractTerm_rewrite​(java.util.function.Function<Term,​Term> hydra_strip_deannotateTerm, java.util.function.Function<Name,​java.util.function.Function<Term,​java.lang.Boolean>> hydra_variables_isFreeVariableInTerm, java.util.function.Function<Name,​java.util.function.Function<Term,​java.util.function.Function<Term,​Term>>> hydra_variables_replaceFreeTermVariable, java.util.function.Function<T0,​Term> recurse, T0 t)  
      static java.lang.Boolean countPrimitiveInvocations()
      Compile-time flag controlling whether primitive invocations are counted during evaluation.
      static Term etaExpandTerm​(Graph tx0, Term term0)
      Recursively transform terms to eliminate partial application, e.g.
      static Either<Error_,​Term> etaExpandTypedTerm​(InferenceContext cx, Graph tx0, Term term0)
      Recursively transform arbitrary terms like 'add 42' into terms like '\x.add 42 x', eliminating partial application.
      static java.lang.Integer etaExpansionArity​(Graph graph, Term term)
      Calculate the arity for eta expansion Note: this is a "trusty" function which assumes the graph is well-formed, i.e.
      static Term etaReduceTerm​(Term term)
      Eta-reduce a term by removing redundant lambda abstractions
      static Either<Error_,​Term> reduceTerm​(InferenceContext cx, Graph graph, java.lang.Boolean eager, Term term)
      A term evaluation function which is alternatively lazy or eager
      static java.lang.Boolean termIsClosed​(Term term)
      Whether a term is closed, i.e.
      static java.lang.Boolean termIsValue​(Term term)
      Whether a term has been fully reduced to a value

    • Method Detail

      • alphaConvert

        static Term alphaConvert​(Name vold,
                         Name vnew,
                         Term term)
        Alpha convert a variable in a term

      • betaReduceType

        static <T0> Either<Error_,​Type> betaReduceType​(T0 cx,
                                                     Graph graph,
                                                     Type typ)
        Eagerly beta-reduce a type by substituting type arguments into type lambdas

      • contractTerm

        static Term contractTerm​(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.

      • contractTerm_rewrite

        static <T0> Term contractTerm_rewrite​(java.util.function.Function<Term,​Term> hydra_strip_deannotateTerm,
                                      java.util.function.Function<Name,​java.util.function.Function<Term,​java.lang.Boolean>> hydra_variables_isFreeVariableInTerm,
                                      java.util.function.Function<Name,​java.util.function.Function<Term,​java.util.function.Function<Term,​Term>>> hydra_variables_replaceFreeTermVariable,
                                      java.util.function.Function<T0,​Term> recurse,
                                      T0 t)

      • countPrimitiveInvocations

        static java.lang.Boolean countPrimitiveInvocations()
        Compile-time flag controlling whether primitive invocations are counted during evaluation. For demo and instrumentation purposes.

      • etaExpandTerm

        static Term etaExpandTerm​(Graph tx0,
                          Term term0)
        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.

      • etaExpandTypedTerm

        static Either<Error_,​Term> etaExpandTypedTerm​(InferenceContext cx,
                                                    Graph tx0,
                                                    Term term0)
        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.

      • etaExpansionArity

        static java.lang.Integer etaExpansionArity​(Graph graph,
                                           Term term)
        Calculate the arity for eta expansion Note: this is a "trusty" function which assumes the graph is well-formed, i.e. no dangling references.

      • etaReduceTerm

        static Term etaReduceTerm​(Term term)
        Eta-reduce a term by removing redundant lambda abstractions

      • termIsClosed

        static java.lang.Boolean termIsClosed​(Term term)
        Whether a term is closed, i.e. represents a complete program

      • termIsValue

        static java.lang.Boolean termIsValue​(Term term)
        Whether a term has been fully reduced to a value