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

Source: arXiv - 2512.05224v1

Overview

NVLang is a new statically‑typed language that runs on the same virtual machine (the BEAM) used by Erlang/OTP. It gives developers compile‑time guarantees about the shape of messages that actors exchange, eliminating a whole class of runtime crashes that currently have to be caught by testing or monitoring.

Key Contributions

• Typed actor interfaces – Introduces Pid[T] where the type parameter T is the exact set of messages an actor can receive.
• Algebraic data types for protocols – Uses ADTs to model message vocabularies, letting the type system enforce correct pattern‑matching.
• Typed futures (Future[T]) – Provides a type‑safe request‑reply pattern that integrates cleanly with the actor model.
• Hindley‑Milner inference extension – Adapts classic type inference to propagate protocol information without burdening programmers with extra annotations.
• Seamless BEAM interop – Compiles to Core Erlang, so existing OTP libraries and tools can be reused unchanged.
• Formal soundness proof sketch – Shows that well‑typed NVLang programs cannot send messages that violate an actor’s declared protocol.

Methodology

The authors start by defining a small core calculus that captures the essential features of the BEAM: lightweight processes, message passing, and pattern matching. They then extend the Hindley‑Milner type system with a protocol kind that tracks the sum type (the ADT) associated with each process identifier.

Key steps include:

1. Message‑type encoding – Every message is an instance of a user‑defined ADT. The compiler infers which ADT a given Pid expects.
2. Typed Pids – Pid[T] is a first‑class value; the type parameter T is carried through function signatures, ensuring only compatible messages can be sent.
3. Future abstraction – A Future[T] is created when a process sends a request; the type guarantees that the eventual reply will be of type T.
4. Inference algorithm – The type checker propagates protocol constraints alongside ordinary type constraints, solving them together so most code needs no explicit type annotations.
5. Compilation pipeline – NVLang source is translated to Core Erlang, preserving the inferred types as runtime‑checkable metadata, which the BEAM can ignore for performance.

Results & Findings

• Zero false positives in a suite of benchmark actor programs: all legitimate message patterns type‑checked, while deliberately malformed messages were rejected at compile time.
• Comparable performance to native Erlang: the extra type information is erased during compilation, so runtime overhead is negligible.
• Interoperability demo: an existing OTP chat server was ported to NVLang with <5 % code changes, gaining static guarantees for its client‑server protocol without sacrificing existing OTP behaviours.
• Soundness guarantee: the formal proof (sketched) confirms that a well‑typed NVLang program cannot cause a “badmatch” error due to an unexpected message shape.

Practical Implications

• Safer microservices – Teams building OTP‑based microservices can catch protocol mismatches early, reducing costly production incidents.
• Improved developer tooling – IDEs can leverage the inferred Pid[T] types for autocomplete, refactoring, and instant feedback on message‑passing code.
• Gradual migration – Because NVLang compiles to Core Erlang, legacy codebases can adopt typed modules incrementally, preserving investment in existing libraries.
• Better documentation – The ADT that defines an actor’s message set doubles as formal API documentation, making onboarding easier for new engineers.
• Future‑proofing – Typed futures open the door to more sophisticated request‑reply patterns (e.g., time‑outs, cancellation) while keeping type safety.

Limitations & Future Work

• Limited to BEAM – The current prototype targets only the Erlang VM; extending the approach to other actor runtimes (e.g., Akka, Orleans) would require additional work.
• No runtime enforcement – Type safety is compile‑time only; if untyped Erlang code sends malformed messages to a typed actor, the guarantee is broken.
• Tooling maturity – The compiler and IDE support are still early‑stage; richer debugging and error‑message facilities are planned.
• Protocol evolution – Handling versioned or evolving message protocols (e.g., backward compatibility) is an open challenge.

Future research directions include integrating gradual typing to allow mixed typed/untyped modules, exploring automated migration tools for large Erlang codebases, and extending the type system to capture more advanced OTP behaviours such as supervision trees and hot code upgrades.

Authors

• Miguel de Oliveira Guerreiro

Paper Information

• arXiv ID: 2512.05224v1
• Categories: cs.PL, cs.DC
• Published: December 4, 2025
• PDF: Download PDF