Rex Type System (rexlang-typesystem)

This crate implements a Hindley-Milner style type system with parametric polymorphism, type classes, and simple algebraic data types (ADTs). It is intended to power Rex's checker and can also be reused by host code to register additional builtins or domain-specific types.

Features

• Types: primitives (u8, u16, u32, u64, i8, i16, i32, i64, f32, f64, bool, string, uuid, datetime), tuples, functions, dictionaries (Dict a), and user constructors (List, Result, Option).
• Arrays: host-native Array a values intended for performance and supported by the same collection combinators via type classes.
• Schemes: quantified types with class constraints.
• Type classes: class hierarchy for additive/multiplicative monoids, semiring, additive group, ring, and field, plus instance resolution with superclass propagation.
• Prelude: ADT constructors (Empty, Cons, Ok, Err, Some, None) and constrained function declarations for numeric, equality, list, option, and result operations.
• Utilities: substitution, unification (with occurs check), instantiation, and generalization helpers.

Quickstart

use rex_ast::expr::intern;
use rex_ts::{BuiltinTypeId, Predicate, Type, TypeSystem};

fn main() -> Result<(), rex_ts::TypeError> {
    let mut ts = TypeSystem::new_with_prelude()?;

    // Register an additional function: id :: a -> a
    let a = Type::var(ts.supply.fresh(Some(intern("a"))));
    let scheme = rex_ts::generalize(&ts.env, vec![], Type::fun(a.clone(), a));
    ts.add_value("id", scheme);

    // Ask whether a class constraint is satisfiable in the prelude
    let field_f32 = Predicate::new("Field", Type::builtin(BuiltinTypeId::F32));
    assert!(rex_ts::entails(&ts.classes, &[], &field_f32)?);
    Ok(())
}

Inference

The inference entry points are infer(&mut ts, expr) (predicates + type) and infer_typed(&mut ts, expr) (typed AST + predicates + type), both of which work on rex_ast::expr::Expr. Literal behavior follows the current language requirement:

The inference engine and its tests live in src/inference.rs; src/typesystem.rs contains the shared type-system data structures, unification machinery, and declaration/typeclass registration code that inference builds on.

• Integer literals are Integral-constrained and can specialize from context; ambiguous cases default later to i32
• Float literals default to f32

Example (from tests):

let
  id = \x -> x
in
  id (id 420, id 6.9, id "str")

This infers to the tuple type (i32, f32, string).

The current inference implementation covers variables, application, lambdas, let-in, if-then-else, tuples, lists, dicts, named constructors, literals, and match.

Prelude Summary

Classes

• AdditiveMonoid, MultiplicativeMonoid, Semiring, AdditiveGroup, Ring, Field
• Eq (equality), Ord (ordering)
• Functor, Applicative, Monad, Foldable, Filterable, Sequence, Alternative

Operators

• Arithmetic: +, -, *, /, negate
• Equality: ==, != (Eq a constraints)
• Ordering: <, <=, >, >= (Ord a constraints)
• Booleans: &&, || (bool only)
• Monoid identities: zero, one

Collection Combinators

• map, fold, foldl, foldr, filter, filter_map, bind, ap, or_else
• sum, mean, count, take, skip, zip, unzip, min, max These are type-class constrained and work for List, Array, Option, and Result where applicable.

Option/Result Helpers

• Option: is_some, is_none
• Result: is_ok, is_err

Run the library tests with:

cargo test -p rexlang-typesystem

Extending

You can register new ADTs with AdtDecl + TypeSystem::register_adt. The TypeSystem also exposes register_instance for low-level instance-head injection and a supply for generating fresh type variables when building new schemes.