Crate arithmetic_typing[][src]

Expand description

Hindley–Milner type inference for arithmetic expressions parsed by the arithmetic-parser crate.

This crate allows parsing type annotations as a part of a Grammar, and to infer and check types for expressions / statements produced by arithmetic-parser. Type inference is partially compatible with the interpreter from arithmetic-eval; if the inference algorithm succeeds on a certain expression / statement / block, it will execute successfully, but not all successfully executing items pass type inference. (An exception here is Type::Any, which is specifically designed to circumvent the type system limitations. If Any is used too liberally, it can result in code passing type checks, but failing during execution.)

Type system

The type system corresponds to types of Values in arithmetic-eval:

  • Primitive types are customizeable via PrimitiveType impl. In the simplest case, there can be 2 primitive types: Booleans (Bool) and numbers (Num), as ecapsulated in Num.
  • There are two container types - tuples and objects.
  • Tuple types can be represented either in the tuple form, such as (Num, Bool), or as a slice, such as [Num; 3]. As in Rust, all slice elements must have the same type. Unlike Rust, tuple and slice forms are equivalent; e.g., [Num; 3] and (Num, Num, Num) are the same type.
  • Object types are represented in a brace form, such as { x: Num }. Objects can act as either specific types or type constraints.
  • Functions are first-class types. Functions can have type and/or const params. Const params always specify tuple length.
  • Type params can be constrained. Constraints are expressed via Constraints. As an example, Num has a few known constraints, such as type Linearity.

Inference rules

Inference mostly corresponds to Hindley–Milner typing rules. It does not require type annotations, but utilizes them if present. Type unification (encapsulated in Substitutions) is performed at each variable use or assignment. Variable uses include function calls and unary and binary ops; the op behavior is customizable via TypeArithmetic.

Whenever possible, the most generic type satisfying the constraints is used. In particular, this means that all type / length variables not resolved at the function definition site become parameters of the function. Likewise, each function call instantiates a separate instance of a generic function; type / length params for each call are assigned independently. See the example below for more details.


Field access

See Tuple docs for discussion of indexing expressions, such as xs.0, and Object docs for discussion of field access, such as point.x.

Type casts

A type cast is equivalent to introducing a new var with the specified annotation, assigning to it and returning the new var. That is, x as Bool is equivalent to { _x: Bool = x; _x }. As such, casts are safe (cannot be used to transmute the type arbitrarily), unless any type is involved.


use arithmetic_parser::grammars::{F32Grammar, Parse};
use arithmetic_typing::{defs::Prelude, Annotated, TypeEnvironment, Type};

let code = "sum = |xs| xs.fold(0, |acc, x| acc + x);";
let ast = Annotated::<F32Grammar>::parse_statements(code)?;

let mut env = TypeEnvironment::new();
env.insert("fold", Prelude::Fold);

// Evaluate `code` to get the inferred `sum` function signature.
let output_type = env.process_statements(&ast)?;
assert_eq!(env["sum"].to_string(), "([Num; N]) -> Num");

Defining and using generic functions:

let code = "sum_with = |xs, init| xs.fold(init, |acc, x| acc + x);";
let ast = Annotated::<F32Grammar>::parse_statements(code)?;

let mut env = TypeEnvironment::new();
env.insert("fold", Prelude::Fold);

let output_type = env.process_statements(&ast)?;
    "for<'T: Ops> (['T; N], 'T) -> 'T"
// Note that `sum_with` is parametric by the element of the slice
// (for which the linearity constraint is applied based on the arg usage)
// *and* by its length.

let usage_code = r#"
    num_sum: Num = (1, 2, 3).sum_with(0);
    tuple_sum: (Num, Num) = ((1, 2), (3, 4)).sum_with((0, 0));
let ast = Annotated::<F32Grammar>::parse_statements(usage_code)?;
// Both lengths and element types differ in these invocations,
// but it works fine since they are treated independently.



Types allowing to customize various aspects of the type system, such as type constraints and behavior of unary / binary ops.


ASTs for type annotations and their parsing logic.


Type definitions for the standard types from the arithmetic-eval crate.


Errors related to type inference.


Visitor traits allowing to traverse Type and related types.



Grammar with support of type annotations. Works as a decorator.


Arbitrary type implementing certain constraints. Similar to dyn _ types in Rust or use of interfaces in type position in TypeScript.


Function together with constraints on type variables contained either in the function itself or any of the child functions.


Functional type.


Builder for functional types.


Length variable.


Object type: a collection of named fields with heterogeneous types.


Slice type. Unlike in Rust, slices are a subset of tuples. If length is exact (has no UnknownLen part), the slice is completely equivalent to the corresponding tuple.


Tuple type.


Generic tuple length.


Environment containing type information on named variables.


Type variable.



Index of an element within a tuple.


Enumeration encompassing all types supported by the type system.


Unknown / variable length, e.g., of a tuple.



Primitive types in a certain type system.