curry.typecheck.terms module

The type terms of the engine.

A term is a FlatCurry type whose leaves may be unification variables. The structural nodes are the constructors of the FlatCurry reader, TCons and FuncType. A leaf is a Var, a union-find cell that is bound once and never rebound, or a Rigid, a type variable of an exprtype string, which unifies with itself alone.

The pseudo constructor Prelude.Apply applies a type variable to a type. whnf() folds an Apply whose head became a constructor, up to the declared arity of the constructor, so that Apply IO Int reads IO Int, and writes a saturated (->) as a FuncType. zonk() resolves a term into a FlatCurry type with TVar leaves, for the printer and for the defaulting table.

class curry.typecheck.terms.Naming

Bases: object

Names the unbound variables of the terms it zonks, in the order of their first occurrence. names maps the index of a rigid variable to its name, for the printer.

index(leaf)

The index of an unbound or rigid variable; a new one on first use.

leaf(index)

The variable of an index.

show(typeexpr, module=None)

Prints a zonked type with the rigid names.

class curry.typecheck.terms.Rigid(name, source=None)

Bases: object

A type variable of an exprtype string. It is a constant to the unifier: it unifies with itself and with an unbound Var, and with nothing else.

name

source

class curry.typecheck.terms.Var(kind=None)

Bases: object

A unification variable.

Variables:

• binding – The term this variable is bound to, or None. Only the representative of a class is ever bound.

• kind – The kind the scheme declared, for messages; None for a fresh variable.

• holders – The specs that own this variable: literal and free-variable specs. The lists of two classes are merged when the classes are united.

• preds – The class predicates on this variable, merged in the same way.

binding

find()

The representative of this variable, with path compression.

holders

kind

preds

uid

union(other)

Unites two unbound representatives; other becomes the root.

curry.typecheck.terms.arrow(domain, range)

curry.typecheck.terms.free_vars(term)

The unbound variables of a term, in the order of their first occurrence. A structural node is visited once (see occurs()).

curry.typecheck.terms.instantiate(typeexpr, mapping, kinds=None)

The term of a FlatCurry type. mapping takes the index of a type variable to its Var; a variable absent from it gets a fresh one, with the kind kinds gives for the index. A nested ForallType quantifies fresh variables for its own indices.

curry.typecheck.terms.is_ground(term)

Whether a term holds no unbound variable and no rigid variable.

curry.typecheck.terms.occurs(var, term)

Whether the unbound variable var occurs in term. A structural node is visited once, so a term whose tree is exponential in the size of its graph (the type of a value that shares a node between two components of a pair, at every level) costs the size of the graph.

curry.typecheck.terms.prune(term)

Follows the bindings of a variable to the term it stands for.

curry.typecheck.terms.tcons(name, *args)

A constructor type of the Prelude, e.g., tcons('Maybe', a).

curry.typecheck.terms.tree_size(term, cap=None)

The number of nodes of the type zonk() would write for term: the size of its tree, counted over its graph, so a shared subterm is measured once and counted at every occurrence. With cap, a count above it is reported as cap + 1; the walk itself costs the size of the graph.

curry.typecheck.terms.type_arity(interp)

A function from the qualified name of a type constructor to its declared arity, or None for a type without an interface entry.

curry.typecheck.terms.whnf(term, arity=None)

The head of a term: a pruned term whose Apply is folded when its head is a constructor with room for one more argument, and whose saturated (->) is a FuncType. arity maps a qualified type name to its declared arity, or None; without it every such Apply is folded.

curry.typecheck.terms.zonk(term, naming=None, arity=None)

Resolves a term into a FlatCurry type. An unbound variable becomes a TVar whose index naming assigns; a rigid variable too, with its name recorded. Apply of a constructor is folded on the way.