Crate arithmetic_typing

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.

Operations

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.

Examples

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!(output_type.is_void());
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)?;
assert!(output_type.is_void());
assert_eq!(
    env["sum_with"].to_string(),
    "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.
env.process_statements(&ast)?;

Modules

arith	Types allowing to customize various aspects of the type system, such as type constraints and behavior of unary / binary ops.
ast	ASTs for type annotations and their parsing logic.
defs	Type definitions for the standard types from the arithmetic-eval crate.
error	Errors related to type inference.
visit	Visitor traits allowing to traverse Type and related types.

Structs

Annotated	Grammar with support of type annotations. Works as a decorator.
DynConstraints	Arbitrary type implementing certain constraints. Similar to dyn _ types in Rust or use of interfaces in type position in TypeScript.
FnWithConstraints	Function together with constraints on type variables contained either in the function itself or any of the child functions.
Function	Functional type.
FunctionBuilder	Builder for functional types.
LengthVar	Length variable.
Object	Object type: a collection of named fields with heterogeneous types.
Slice	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	Tuple type.
TupleLen	Generic tuple length.
TypeEnvironment	Environment containing type information on named variables.
TypeVar	Type variable.

Enums

TupleIndex	Index of an element within a tuple.
Type	Enumeration encompassing all types supported by the type system.
UnknownLen	Unknown / variable length, e.g., of a tuple.

Traits

PrimitiveType

Primitive types in a certain type system.