hydra.inference module

Type inference for Hydra: Hindley-Milner with elaboration to System F. Extends textbook Algorithm W with nominal types, explicit type abstraction and application, and class constraints. See the Inference wiki page for the full picture.

hydra.inference.at_or_fail(i: int, desc: str, xs: Sequence[T0]) → object

Return the element at the given index, or Left(Other) with the given description if out of range.

hydra.inference.bind_constraints(flow_cx: InferenceContext, cx: Graph, constraints: Sequence[TypeConstraint]) → object

Unify type constraints and check the substitution.

hydra.inference.bind_unbound_type_variables(cx: Graph, term0: Term) → Term

Handle unbound type variables under a typed let binding. Variables appearing free in the binding’s declared type (but not in schema types or the scheme’s own quantified variables) are added to the scheme and the term is wrapped in matching TypeLambdas. Variables appearing only in the term body (at type-application or lambda-domain positions) are phantom — they have no external effect on the binding’s type — and are substituted with hydra.core.Unit in the body rather than generalized. This keeps downstream stages from seeing vacuous foralls that target languages with non-polymorphic value bindings (e.g. Scala val) cannot express.

hydra.inference.build_type_application_term(tvars: Sequence[Name], body: Term) → Term

Fold a list of type variables over a term to build a type application term.

hydra.inference.discharge_class_constraints(fcx: InferenceContext, subst: TypeSubst, constraints: Mapping[Name, TypeVariableConstraints]) → object

Check that every constrained type variable’s final resolved type is an instance of each class it was constrained to.

hydra.inference.extend_context(pairs: Sequence[tuple[Name, TypeScheme]], cx: Graph) → Graph

Add (term variable, type scheme) pairs to the graph’s bound types.

hydra.inference.finalize_inferred_term(flow_cx: T0, cx: Graph, term: Term) → object

Finalize an inferred term by checking for unbound type variables, then normalizing type variables.

hydra.inference.for_inferred_term(fcx: InferenceContext, cx: Graph, term: Term, desc: str, f: Callable[[InferenceResult], T0]) → object

Infer a term’s type and map over the result.

hydra.inference.free_variables_in_context(cx: Graph) → Set[Name]

Get all free variables in a graph’s bound types.

hydra.inference.fresh_variable_type(cx: InferenceContext) → tuple[Type, InferenceContext]

Generate a fresh type variable.

hydra.inference.generalize(cx: Graph, typ: Type) → TypeScheme

Generalize a type to a type scheme. Paper: inference.tex, gen() and rule Gen.

hydra.inference.head_or_fail(desc: str, xs: Sequence[T0]) → object

Return the first element of a list, or Left(Other) with the given description if the list is empty.

hydra.inference.infer_graph_types(fcx0: InferenceContext, bindings0: Sequence[Binding], g0: Graph) → object

Infer types for all elements in a graph, using the provided ordered bindings. Returns both the inferred graph and the ordered inferred bindings. Paper: inference.tex, the SCC treatment of cycles (section introduction); the whole graph is one mutually recursive let.

hydra.inference.infer_in_graph_context(fcx: InferenceContext, cx: Graph, term: Term) → object

Infer the type of a term in a given inference context.

hydra.inference.infer_many(fcx: InferenceContext, cx: Graph, pairs: Sequence[tuple[Term, str]]) → object

Infer types for multiple terms, propagating class constraints from sub-expressions.

hydra.inference.infer_type_of(fcx: InferenceContext, cx: Graph, term: Term) → object

Map a possibly untyped term to a fully typed term and its type.

hydra.inference.infer_type_of_annotated_term(fcx: InferenceContext, cx: Graph, at: AnnotatedTerm) → object

Infer the type of an annotated term (Either version). Paper: inference.tex, rule Ann.

hydra.inference.infer_type_of_application(fcx0: InferenceContext, cx: Graph, app: Application) → object

Infer the type of a function application (Either version). Paper: inference.tex, rule App (elaboration form).

hydra.inference.infer_type_of_case_statement(fcx: InferenceContext, cx: Graph, case_stmt: CaseStatement) → object

Infer the type of a case statement (Either version). Paper: inference.tex, rules Case and Case_d.

hydra.inference.infer_type_of_collection(fcx: InferenceContext, cx: Graph, typ_cons: Callable[[Type], Type], trm_cons: Callable[[Sequence[Term]], Term], desc: str, class_names: Set[Name], els: Sequence[Term]) → object

Infer the type of a collection. The classNames parameter specifies type classes (e.g. ordering) that the element type variable must satisfy. Paper: inference.tex, shared implementation of the collection introduction rules (Lst_0/Lst_+, Set_0/Set_+).

hydra.inference.infer_type_of_either(fcx: InferenceContext, cx: Graph, e: object) → object

Infer the type of an either value (Either version). Paper: inference.tex, rules Eith_L and Eith_R.

hydra.inference.infer_type_of_injection(fcx: InferenceContext, cx: Graph, injection: Injection) → object

Infer the type of a union injection (Either version). Paper: inference.tex, rule Inj.

hydra.inference.infer_type_of_lambda(fcx: InferenceContext, cx: Graph, lambda_: Lambda) → object

Infer the type of a lambda function (Either version). Paper: inference.tex, rule Abs (elaboration form).

hydra.inference.infer_type_of_let(fcx0: InferenceContext, cx: Graph, let0: Let) → object

Normalize a let term before inferring its type (Either version). The bindings are partitioned into strongly connected components and reorganized as nested lets, one let per SCC, in dependency order. This is the standard Hindley-Milner treatment of mutual recursion: each SCC is generalized once at its boundary (sound, because nothing inside the cluster sees a polymorphic instance of its siblings), and acyclic bindings generalize individually as usual. Paper: inference.tex, the SCC treatment of cycles (section introduction) and the remark following the elaboration-form Let rule.

hydra.inference.infer_type_of_let_normalized(fcx0: InferenceContext, cx0: Graph, let_term: Let) → object

Infer the type of a let (letrec) term which is already in a normal form (Either version). Paper: inference.tex, rule Let (elaboration form).

hydra.inference.infer_type_of_list(fcx: InferenceContext, cx: Graph, v1: Sequence[Term]) → object

Infer the type of a list (Either version). Paper: inference.tex, rules Lst_0 and Lst_+.

hydra.inference.infer_type_of_literal(fcx: InferenceContext, lit: Literal) → InferenceResult

Infer the type of a literal. Paper: inference.tex, rule Lit.

hydra.inference.infer_type_of_map(fcx: InferenceContext, cx: Graph, m: Mapping[Term, Term]) → object

Infer the type of a map (Either version). Paper: inference.tex, rules Map_0 and Map_+.

hydra.inference.infer_type_of_optional(fcx: InferenceContext, cx: Graph, m: object) → object

Infer the type of a Maybe value. Paper: inference.tex, rules Opt_0 and Opt_1.

hydra.inference.infer_type_of_pair(fcx: InferenceContext, cx: Graph, p: tuple[Term, Term]) → object

Infer the type of a pair (Either version). Paper: inference.tex, rule Pair.

hydra.inference.infer_type_of_projection(fcx: InferenceContext, cx: Graph, proj: Projection) → object

Infer the type of a record projection (Either version). Paper: inference.tex, rule Proj.

hydra.inference.infer_type_of_record(fcx: InferenceContext, cx: Graph, record: Record) → object

Infer the type of a record (Either version). Paper: inference.tex, rule Rec.

hydra.inference.infer_type_of_set(fcx: InferenceContext, cx: Graph, s: Set[Term]) → object

Infer the type of a set (Either version). Paper: inference.tex, rules Set_0 and Set_+.

hydra.inference.infer_type_of_term(fcx: InferenceContext, cx: Graph, term: Term, desc: str) → object

Infer the type of a given term (Either version).

hydra.inference.infer_type_of_type_application(fcx: InferenceContext, cx: Graph, tt: TypeApplicationTerm) → object

Infer the type of a type application (Either version). Paper: inference.tex, type application terms in the elaborated Term grammar.

hydra.inference.infer_type_of_type_lambda(fcx: InferenceContext, cx: Graph, ta: TypeLambda) → object

Infer the type of a type abstraction (Either version). Paper: inference.tex, type abstraction terms in the elaborated Term grammar.

hydra.inference.infer_type_of_unit(fcx: InferenceContext) → InferenceResult

The trivial inference rule for the unit term. Paper: inference.tex, rule Unit.

hydra.inference.infer_type_of_unwrap(fcx: InferenceContext, cx: Graph, tname: Name) → object

Infer the type of an unwrap operation (Either version). Paper: inference.tex, rule Unwr.

hydra.inference.infer_type_of_variable(fcx: InferenceContext, cx: Graph, name: Name) → object

Infer the type of a variable (Either version). Paper: inference.tex, rule Var (elaboration form), with rule Prim as the primitive-namespace fallback.

hydra.inference.infer_type_of_wrapped_term(fcx: InferenceContext, cx: Graph, wt: WrappedTerm) → object

Infer the type of a wrapped term (Either version). Paper: inference.tex, rule Wrp.

hydra.inference.infer_types_of_temporary_bindings(fcx: InferenceContext, cx: Graph, bins: Sequence[Binding]) → object

Infer types for temporary let bindings (Either version).

hydra.inference.is_unbound(cx: Graph, v: Name) → bool

Check if a variable is unbound in context.

hydra.inference.map_constraints(flow_cx: InferenceContext, cx: Graph, f: Callable[[TypeSubst], T0], constraints: Sequence[TypeConstraint]) → object

Map over type constraints after unification.

hydra.inference.merge_class_constraints(m1: Mapping[T0, TypeVariableConstraints], m2: Mapping[T0, TypeVariableConstraints]) → Mapping[T0, TypeVariableConstraints]

Merge two maps of class constraints. When both maps have constraints for the same variable, union the class sets.

hydra.inference.show_inference_result(result: InferenceResult) → str

Show an inference result for debugging.

hydra.inference.yield_(fcx: InferenceContext, term: Term, typ: Type, subst: TypeSubst) → InferenceResult

Create an inference result with no class constraints.

hydra.inference.yield_checked(fcx: InferenceContext, term: Term, typ: Type, subst: TypeSubst) → InferenceResult

Create a checked inference result.

hydra.inference.yield_checked_with_constraints(fcx: InferenceContext, term: Term, typ: Type, subst: TypeSubst, constraints: Mapping[Name, TypeVariableConstraints]) → InferenceResult

Create a checked inference result with class constraints.

hydra.inference.yield_with_constraints(fcx: InferenceContext, term: Term, typ: Type, subst: TypeSubst, constraints: Mapping[Name, TypeVariableConstraints]) → InferenceResult

Create an inference result with class constraints.