hydra.checking module

Type checking and type reconstruction (type-of) for the results of Hydra unification and inference.

hydra.checking.all_equal(els: Sequence[T0]) → bool

True if every element of the list is equal to every other element (vacuously true for the empty list).

hydra.checking.apply_type_arguments_to_type(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], t: Type) → object

Apply type arguments to a type, substituting forall-bound variables. Paper: inference.tex, ‘Checking the witness’ (consuming the pending-type-argument stack).

hydra.checking.check_for_unbound_type_variables(cx: T0, tx: Graph, term0: Term) → object

Check that a term has no unbound type variables (Either version). Paper: inference.tex, ‘Checking the witness’ (always-on finalization invariant).

hydra.checking.check_same_type(cx: T0, tx: Graph, desc: str, types: Sequence[Type]) → object

Ensure all types in a list are equal and return the common type.

hydra.checking.check_type_subst(cx: T0, tx: Graph, subst: TypeSubst) → object

Sanity-check a type substitution arising from unification. Specifically, check that schema types have not been inappropriately unified with type variables inferred from terms. Paper: inference.tex, ‘Checking the witness’ (always-on invariant: a substitution may not bind a type name as if it were an inference variable).

hydra.checking.contains_in_scope_type_vars(tx: Graph, t: Type) → bool

Check if a type contains any type variable from the current scope.

hydra.checking.normalize_type_free_vars(typ: Type) → Type

Normalize free type variables in a type to canonical names based on order of first occurrence. This allows comparing types that differ only in the naming of free type variables. Paper: inference.tex, ‘Checking the witness’ (effective equality).

hydra.checking.to_f_context(cx: Graph) → Mapping[Name, Type]

Get the bound types from a graph as a type environment.

hydra.checking.type_lists_effectively_equal(tx: Graph, tlist1: Sequence[Type], tlist2: Sequence[Type]) → bool

Check whether two lists of types are effectively equal, disregarding type aliases.

hydra.checking.type_of(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], term: Term) → object

Given a type context, reconstruct the type of a System F term. Paper: inference.tex, ‘Checking the witness’ – the executable form of the System F typing judgment in the soundness theorem.

hydra.checking.type_of_annotated_term(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], at: AnnotatedTerm) → object

Reconstruct the type of an annotated term (Either/InferenceContext version). Paper: inference.tex, rule Ann (checking side).

hydra.checking.type_of_application(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], app: Application) → object

Reconstruct the type of an application term (Either/InferenceContext version). Paper: inference.tex, rule App (checking side).

hydra.checking.type_of_case_statement(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], cs: CaseStatement) → object

Reconstruct the type of a case statement (Either/InferenceContext version). Paper: inference.tex, rules Case and Case_d (checking side).

hydra.checking.type_of_either(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], et: object) → object

Reconstruct the type of an either value (Either/InferenceContext version). Paper: inference.tex, rules Eith_L and Eith_R (checking side).

hydra.checking.type_of_injection(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], injection: Injection) → object

Reconstruct the type of a union injection (Either/InferenceContext version). Paper: inference.tex, rule Inj (checking side).

hydra.checking.type_of_lambda(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], l: Lambda) → object

Reconstruct the type of a lambda function (Either/InferenceContext version). Paper: inference.tex, rule Abs (checking side).

hydra.checking.type_of_let(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], let_term: Let) → object

Reconstruct the type of a let binding (Either/InferenceContext version). Paper: inference.tex, rule Let (checking side).

hydra.checking.type_of_list(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], els: Sequence[Term]) → object

Reconstruct the type of a list (Either/InferenceContext version). Paper: inference.tex, rules Lst_0 and Lst_+ (checking side).

hydra.checking.type_of_literal(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], lit: Literal) → object

Reconstruct the type of a literal (Either/InferenceContext version). Paper: inference.tex, rule Lit (checking side).

hydra.checking.type_of_map(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], m: Mapping[Term, Term]) → object

Reconstruct the type of a map (Either/InferenceContext version). Paper: inference.tex, rules Map_0 and Map_+ (checking side).

hydra.checking.type_of_maybe(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], mt: object) → object

Reconstruct the type of an optional value (Either/InferenceContext version). Paper: inference.tex, rules Opt_0 and Opt_1 (checking side).

hydra.checking.type_of_pair(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], p: tuple[Term, Term]) → object

Reconstruct the type of a pair (Either/InferenceContext version). Paper: inference.tex, rule Pair (checking side).

hydra.checking.type_of_primitive(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], name: Name) → object

Reconstruct the type of a primitive function (Either/InferenceContext version). Paper: inference.tex, rule Prim (checking side).

hydra.checking.type_of_projection(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], p: Projection) → object

Reconstruct the type of a record projection (Either/InferenceContext version). Paper: inference.tex, rule Proj (checking side).

hydra.checking.type_of_record(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], record: Record) → object

Reconstruct the type of a record (Either/InferenceContext version). Paper: inference.tex, rule Rec (checking side).

hydra.checking.type_of_set(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], els: Set[Term]) → object

Reconstruct the type of a set (Either/InferenceContext version). Paper: inference.tex, rules Set_0 and Set_+ (checking side).

hydra.checking.type_of_term(cx: InferenceContext, g: Graph, term: Term) → object

Check the type of a term.

hydra.checking.type_of_type_application(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], tyapp: TypeApplicationTerm) → object

Reconstruct the type of a type application term (Either/InferenceContext version). Paper: inference.tex, ‘Checking the witness’ (pushes onto the pending-type-argument stack).

hydra.checking.type_of_type_lambda(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], tl: TypeLambda) → object

Reconstruct the type of a type lambda (type abstraction) term (Either/InferenceContext version). Paper: inference.tex, type abstraction terms in the elaborated Term grammar.

hydra.checking.type_of_unit(cx: InferenceContext, tx: Graph, type_args: Sequence[Type]) → object

Reconstruct the type of the unit term (Either/InferenceContext version). Paper: inference.tex, rule Unit (checking side).

hydra.checking.type_of_unwrap(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], tname: Name) → object

Reconstruct the type of an unwrap operation (Either/InferenceContext version). Paper: inference.tex, rule Unwr (checking side).

hydra.checking.type_of_variable(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], name: Name) → object

Reconstruct the type of a variable (Either/InferenceContext version). Paper: inference.tex, rules Var and Prim (checking side); note the primitives-first lookup order, the reverse of inference.

hydra.checking.type_of_wrapped_term(cx: InferenceContext, tx: Graph, type_args: Sequence[Type], wt: WrappedTerm) → object

Reconstruct the type of a wrapped term (Either/InferenceContext version). Paper: inference.tex, rule Wrp (checking side).

hydra.checking.types_all_effectively_equal(tx: Graph, tlist: Sequence[Type]) → bool

Check whether a list of types are effectively equal, disregarding type aliases and free type variable naming. Also treats free type variables (not in schema) as wildcards, since inference has already verified consistency.

hydra.checking.types_effectively_equal(tx: Graph, t1: Type, t2: Type) → bool

Check whether two types are effectively equal, disregarding type aliases, forall quantifiers, and treating in-scope type variables as wildcards. Paper: inference.tex, ‘Checking the witness’ (effective equality, the type-level analogue of the referential-transparency equality of terms).