# 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 `Value`

s 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
`Constraint`

s. 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 |

error | Errors related to type inference. |

visit | Visitor traits allowing to traverse |

## Structs

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

DynConstraints | Arbitrary type implementing certain constraints. Similar to |

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 |

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