NVLang: Unified Static Typing for Actor-Based Concurrency on the BEAM

TL;DR

<NVLang> presents a statically typed functional language for the BEAM that encodes actor message protocols as algebraic data types, enabling compile-time guarantees of message safety while preserving Erlang/OTP fault-tolerance and concurrency patterns. By extending Hindley-Milner type inference to track actor protocols, it supports typed PIDs and futures with uniform reply types, compiling down to Core Erlang for seamless interoperability. The work formalizes the type system, proves core safety properties (progress, preservation, message-type safety, principal types), and demonstrates near-native performance compared to Erlang with a comprehensive evaluation. The approach emphasizes safety with minimal runtime overhead and offers a practical path toward typed actor programming on BEAM, including OTP-style supervision and asynchronous-first messaging. Limitations include the absence of distributed types, effect tracking, and full session typing, with future directions toward gradual typing and more expressive protocol specifications.

Abstract

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.

Figures (4)

• Figure 1: OneForOne supervision strategy: when Worker 2 crashes, only Worker 2 is restarted while Workers 1 and 3 continue running. The restart policy (permanent/transient/temporary) determines whether restart occurs.
• Figure 2: NVLang compilation pipeline from source to BEAM bytecode. Type inference ensures all type errors are caught before code generation; ANF transformation normalizes expressions for optimal BEAM code generation; the resulting Core Erlang is compiled using Erlang's native compiler.
• Figure 3: Runtime overhead relative to Erlang baseline ($n$=10, error bars show 95% CI). Shaded band indicates $\pm$5% (negligible by systems convention). Only Ring shows statistically significant overhead (*$p < 0.001$). Negative values indicate NVLang outperforming Erlang.
• Figure 4: Execution time distributions across 10 runs. Box plots show median, quartiles, and outliers. NVLang exhibits variance comparable to Erlang; Elixir shows higher variance on message-passing benchmarks due to occasional latency spikes.

Theorems & Definitions (20)

• Theorem 3.1: Progress
• proof : Proof Sketch
• Theorem 3.2: Preservation
• proof : Proof Sketch
• Theorem 3.3: Message Type Safety
• Theorem 3.4: Principal Types
• proof : Proof Sketch
• Definition 4.1: Actor
• Definition 4.2: Supervision Strategy
• Definition 4.3: Supervision Tree