NVLang: Unified Static Typing for Actor-Based Concurrency on the BEAM
By: Miguel de Oliveira Guerreiro
Actor-based systems like Erlang/OTP power critical infrastructure -- from telecommunications to messaging platforms -- handling millions of concurrent connections with legendary reliability. Yet these systems lack static guarantees about message protocols: processes communicate by sending arbitrary messages that pattern-matched at runtime, deferring protocol violations to production failures. We present NVLang, a statically typed functional language that brings comprehensive type safety to the BEAM virtual machine while preserving actor model's simplicity and power. NVLang's central contribution that algebraic data types (ADTs) naturally encode actor message protocols: each actor declares the sum type representing its message vocabulary, and the type system enforces protocol conformance at compile time. We introduce typed process identifiers (Pid[T]) that encode the protocol an actor expects, and typed futures (Future[T]) that provide type-safe request-reply patterns. By extending Hindley-Milner type inference to track message protocols, NVLang eliminates an entire class of message-passing errors while maintaining clean syntax that rivals dynamically typed alternatives. Our implementation compiles to Core Erlang, enabling seamless interoperability with the existing Erlang ecosystem. We formalize the type system and provide proof sketches for type soundness, demonstrating that well-typed NVLang programs cannot send messages that violate actor protocols.
Similar Papers
A Complementary Approach to Incorrectness Typing
Programming Languages
Finds errors in computer programs automatically.
A Language-Agnostic Logical Relation for Message-Passing Protocols
Programming Languages
Checks if different computer parts talk correctly.
A Complementary Approach to Incorrectness Typing
Programming Languages
Finds mistakes in computer programs automatically.