[Paper] NVLang: BEAM에서 액터 기반 동시성을 위한 통합 정적 타입 지정

Source: arXiv - 2512.05224v1

Overview

NVLang은 Erlang/OTP와 동일한 가상 머신(BEAM) 위에서 실행되는 새로운 정적 타입 언어입니다. 액터가 주고받는 메시지의 형태에 대해 컴파일 타임 보장을 제공하여, 현재 테스트나 모니터링으로만 잡을 수 있는 다양한 런타임 크래시를 사전에 방지합니다.

Key Contributions

• Typed actor interfaces – Pid[T]를 도입합니다. 여기서 타입 매개변수 T는 액터가 받을 수 있는 정확한 메시지 집합을 의미합니다.
• Algebraic data types for protocols – ADT를 사용해 메시지 어휘를 모델링함으로써, 타입 시스템이 올바른 패턴 매칭을 강제합니다.
• Typed futures (Future[T]) – 타입 안전한 요청‑응답 패턴을 제공하며, 액터 모델과 깔끔하게 통합됩니다.
• Hindley‑Milner inference extension – 고전적인 타입 추론을 확장해 프로토콜 정보를 전파하고, 프로그래머가 추가 어노테이션을 달 필요 없이 동작합니다.
• Seamless BEAM interop – Core Erlang으로 컴파일되므로 기존 OTP 라이브러리와 도구를 그대로 재사용할 수 있습니다.
• Formal soundness proof sketch – 잘 타입이 지정된 NVLang 프로그램은 액터가 선언한 프로토콜을 위반하는 메시지를 보낼 수 없음을 보여줍니다.

Methodology

저자들은 먼저 BEAM의 핵심 기능인 경량 프로세스, 메시지 전달, 패턴 매칭을 포착하는 작은 코어 계산법을 정의합니다. 이어서 각 프로세스 식별자와 연관된 합 타입(ADT)을 추적하는 프로토콜 kind를 포함하도록 Hindley‑Milner 타입 시스템을 확장합니다.

핵심 단계는 다음과 같습니다:

1. Message‑type encoding – 모든 메시지는 사용자 정의 ADT의 인스턴스입니다. 컴파일러는 주어진 Pid가 기대하는 ADT를 추론합니다.
2. Typed Pids – Pid[T]는 1급 값이며, 타입 매개변수 T는 함수 시그니처를 통해 전달되어 호환 가능한 메시지만 전송될 수 있도록 보장합니다.
3. Future abstraction – 프로세스가 요청을 보낼 때 Future[T]가 생성되며, 타입은 최종 응답이 T 타입임을 보장합니다.
4. Inference algorithm – 타입 검사기는 일반 타입 제약과 함께 프로토콜 제약을 전파하고, 두 제약을 동시에 해결하여 대부분의 코드에서 명시적 타입 어노테이션이 필요 없게 합니다.
5. Compilation pipeline – NVLang 소스는 Core Erlang으로 변환되며, 추론된 타입은 런타임에 확인 가능한 메타데이터로 보존됩니다. BEAM은 성능을 위해 이를 무시합니다.

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