curry.typecheck.engine module

The engine: types one Python-built expression over the schemes of the front end (item Y6 of the typed boundary, epic #48).

The engine is Algorithm J without levels. A caller describes an expression as a tree of specs: an App of a symbol to arguments, a Lit for a Python value, a Free marker, a Known value whose type the caller supplies, a List, a Tuple, an Iter and a Typed annotation. Problem instantiates the scheme of every symbol with fresh variables, unifies eagerly as it walks the tree, and keeps the class predicates on the variables. Problem.solve() reduces the predicates through the instances, defaults the ambiguous numeric variables as the front end does, records the undefaulted scheme (what :type prints), applies the table of the PAKCS REPL (defaulting), and resolves every predicate to a dictionary term.

After solve the caller asks the type of every spec, the dictionaries an application takes, the type a literal resolved to, and the Data dictionary of a free variable. materialize() is the reference materializer: it builds the node of a solved problem through raw_expr, with the dictionaries in scheme order, apply chains for over-application and newtype constructors erased. The typed builder of curry.expr is its production counterpart.

class curry.typecheck.engine.App(symbol, *args)[source]

Bases: Spec

A symbol applied to arguments. symbol is a CurryNodeInfo, the qualified name of a symbol, or a Scheme; each argument is a spec or a Python value spec_of() accepts. After solve: scheme, preds (the predicates of the context, in order), dicts (their dictionary terms), erased (a newtype constructor, built as its argument).

args

dicts

erased

param_roots

params

preds

scheme

symbol

class curry.typecheck.engine.Free(marker=None)[source]

Bases: Spec

A free variable. payload is the marker; two specs with one marker share one variable. After solve, dict is the Data dictionary of its type, or the placeholder of Bool for a polymorphic type.

dict

class curry.typecheck.engine.Iter(iterator=None)[source]

Bases: Spec

A Python iterator: a list whose element type is fixed by the context and by the table, never by an item.

elem

class curry.typecheck.engine.Known(typeexpr, payload=None)[source]

Bases: Spec

A value with a type the caller supplies: a FlatCurry type whose TVar leaves become fresh variables, or a type in Curry syntax. payload is the value, kept as it is.

typeexpr

class curry.typecheck.engine.List(items)[source]

Bases: Spec

A Python list: every item unifies with one element type.

elem

items

class curry.typecheck.engine.Lit(value)[source]

Bases: Spec

A Python value: a bool, an int, a float, a str, or None. An int is typed by a variable with Num, a float by one with Fractional; the expected type decides between Char and [Char] for a one-character string. None is an error that names the expected type.

default

pred

value

class curry.typecheck.engine.Problem(interp, spec, exprtype=None, what=None, hint=DEFAULT_HINT, module=None)[source]

Bases: object

The typing of one expression.

Parameters:

interp – The interpreter.
spec – The expression, as a spec or as the arguments of curry.expr.
exprtype – The expected type of the root, in Curry syntax, or None. Its type variables are rigid.
what – How the errors of the defaulting table name the expression; the default describes the spec.
hint – The last line of those errors.
module – The module whose type names an unqualified name in exprtype prefers, or None.

The constructor types the expression (phase 1); solve() reduces, defaults and resolves (phase 2). Both raise the errors of curry.typecheck.errors.

property defaulted_signature

dictionaries(app)[source]: The dictionary terms of an application, in the order of its scheme.

free_dictionary(free)[source]

literal_dictionary(lit)[source]: The Num or Fractional dictionary of a literal at its type, or None.

literal_type(lit)[source]

location(spec)[source]: The text of the position of a spec, e.g., argument 2 of Prelude.+ :: Num a => a -> a -> a or element 2 of the list in argument 1 of Prelude.length :: [a] -> Int. The chain ends at the nearest application or at the expression; a chain of more than LOCATION_DEPTH positions is elided in the middle, so the text of a deeply nested value stays short.

placeholder()[source]: The dictionary of a polymorphic free variable: Data Bool, unread.

short_location(spec)[source]

show(term, naming=None)[source]: A term in Curry syntax.

show_type_of(spec)[source]

property signature: The undefaulted scheme in Curry syntax, what :type prints.

solve()[source]: Phase 2: reduction, the defaulting of the front end, the table of the REPL, and the resolution of the dictionaries. Returns the problem.

type_of(spec, naming=None)[source]: The type of a spec as a FlatCurry type.

type_of_term(term, naming=None)[source]

property typeexpr: The type of the expression, defaulted after solve.

property what: How the errors of the defaulting table name the expression.

class curry.typecheck.engine.Spec(payload=None)[source]

Bases: object

One node of the description of an expression.

Variables:

type – The term of the node, after the problem typed it.
index (parent,) – The spec this one is an argument of, and its position there.
payload – An object of the caller, kept as it is: the node of a known value, the free marker, the iterator.

index

parent

payload

type

class curry.typecheck.engine.Tuple(items)[source]

Bases: Spec

A Python tuple. () is the unit; Curry has no 1-tuple.

items

class curry.typecheck.engine.Typed(spec, text)[source]

Bases: Spec

A nested annotation: spec at the type text.

spec

text

curry.typecheck.engine.build(interp, *args, **kwds)[source]: Types the arguments of curry.expr and builds the node.

curry.typecheck.engine.describe(spec, depth=DESCRIBE_DEPTH)[source]: The text of a spec in Curry syntax, for messages. A subtree deeper than depth prints as ....

curry.typecheck.engine.infer(interp, *args, **kwds)[source]: Types the arguments of curry.expr and solves; returns the Problem.

curry.typecheck.engine.materialize(problem)[source]: Builds the node of a solved problem through raw_expr: the dictionaries first in scheme order, apply chains for the arguments past the arity, a partial application for fewer, a newtype constructor as its argument and a bare one as Prelude.id, one unknown node per free marker with the Data dictionary of its type, literals at their resolved types. The typed builder of curry.expr is the production counterpart; this one serves the tests of the engine.

curry.typecheck.engine.spec_of(*args)[source]: The spec of the arguments of curry.expr: a spec as it is; a symbol with its arguments; a Python value; a list headed by a symbol as an application and any other list as a Curry list; a tuple; a free marker; a choice marker as a call of Prelude.?; an iterator.