curry.typecheck.unify module

First-order unification of type terms, with an occurs check and the rule for the pseudo constructor Prelude.Apply.

The rules (design of the typed boundary, section 3.3):

  • Apply f a against T a1 .. an with n >= 1 binds f to T a1 .. a(n-1) and unifies a with an. A function type is the constructor (->) with two arguments for this rule.

  • Apply f a against Apply g b unifies pairwise.

  • A variable is bound once; the occurs check refuses an infinite type.

  • A rigid variable (of an exprtype string) unifies with itself and with an unbound variable alone.

  • A nested ForallType is instantiated with fresh variables when the unifier reaches it.

The unifier does not know the engine. It calls on_bind(var, term) after it binds a variable to a term that is not a variable, so that the engine can reduce the predicates of the variable and check its holders.

exception curry.typecheck.unify.OccursError(lhs, rhs, top=None)[source]

Bases: UnifyError

A variable would be bound to a term that contains it.

exception curry.typecheck.unify.TypeMismatch(lhs, rhs, top=None)[source]

Bases: UnifyError

Two constructors differ, or a rigid variable meets another type.

exception curry.typecheck.unify.UnifyError(lhs, rhs, top=None)[source]

Bases: Exception

Two terms do not unify. lhs and rhs are the terms at the point of failure; top the two terms the call started from.

curry.typecheck.unify.unify(lhs, rhs, arity=None, on_bind=None)[source]

Unifies two terms in place.

Parameters:

  • lhs – The terms.

  • rhs – The terms.

  • arity – A function from a qualified type name to its declared arity, or None; terms.whnf() folds Apply with it.

  • on_bind – Called as on_bind(var, term) after a variable is bound to a term that is not a variable.

Raises:

TypeMismatch, OccursError –