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 customizable via PrimitiveType impl. In the simplest case, there can be 2 primitive types: Booleans (Bool) and numbers (Num), as encapsulated 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.

Method calls

In agreement with the arithmetic-eval crate, methods are treated as syntactic sugar for functions. For example, xs.map(sin) is equivalent to map(xs, sin).

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 = "
    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.