hydra.unification module

Utilities for type unification.

hydra.unification.join_types(cx: T0, left: Type, right: Type, comment: str) → object

Join two types, producing a list of type constraints.The comment is used to provide context for the constraints.

hydra.unification.unify_type_constraints(cx: T0, schema_types: Mapping[Name, TypeScheme], constraints: Sequence[TypeConstraint]) → object

Robinson’s algorithm, following https://www.cs.cornell.edu/courses/cs6110/2017sp/lectures/lec23.pdf Specifically this is an implementation of the following rules:

• Unify({(x, t)} ∪ E) = {t/x} Unify(E{t/x}) if x ∉ FV(t)

• Unify(∅) = I (the identity substitution x ↦ x)

• Unify({(x, x)} ∪ E) = Unify(E)

• Unify({(f(s1, …, sn), f(t1, …, tn))} ∪ E) = Unify({(s1, t1), …, (sn, tn)} ∪ E)).

hydra.unification.unify_type_lists(cx: T0, schema_types: Mapping[Name, TypeScheme], l: Sequence[Type], r: Sequence[Type], comment: str) → object

Unify two lists of types pairwise, producing a single substitution that satisfies every pair. The lists must have the same length; the comment is attached to each generated constraint for diagnostics.

hydra.unification.unify_types(cx: T0, schema_types: Mapping[Name, TypeScheme], l: Type, r: Type, comment: str) → object

Unify two types, producing a substitution that makes them equal (or an error). The comment is attached to the generated constraint for diagnostics.

hydra.unification.variable_occurs_in_type(var: Name, typ0: Type) → bool

Determine whether a type variable appears within a type expression.No distinction is made between free and bound type variables.