Keywords: linear types, ownership, mutation, resource safety, effect systems, substructural type systems, dual-layer runtime

1 Introduction

The history of programming language design can be read, in large part, as a long negotiation with mutable state. Assembly gives the programmer direct access to every register and memory cell. C organizes that access into functions and structs but leaves aliasing entirely to the programmer’s discipline. Java introduces garbage collection and access modifiers but permits unrestricted sharing of mutable objects across threads. Haskell confines all side effects to the IO monad, achieving referential transparency at the cost of pervasive monadic plumbing. Rust enforces ownership and borrowing rules that prevent data races at compile time, but its borrow checker pervades every layer of the program, even pure data transformations that could never cause a data race.

Japl takes a different position: mutation is local and explicit. The language is organized around two sharply delineated layers:

1. A pure layer where values are immutable, garbage-collected, and freely shared. Most application code—business logic, data transformations, protocol handling—lives here.

2. A resource layer where mutable resources (file handles, network sockets, GPU buffers, FFI pointers) are tracked by a linear ownership discipline. Resources must be consumed exactly once: used and then released.

This separation is the second of Japl’s seven core design principles¹ and is the subject of this paper.

1.1 The Mutation Problem

Shared mutable state creates three interrelated difficulties:

1.1.0.1 Concurrency bugs.

When two threads can both read and write the same memory location, the result depends on scheduling—a data race. Languages without mutation restrictions must rely on locks, atomic operations, or transactional memory, each introducing its own class of bugs (deadlocks, priority inversion, live-lock).

1.1.0.2 Aliasing and invalidation.

When multiple references point to the same mutable object, a mutation through one reference can invalidate assumptions made through another. The classic example is iterator invalidation: removing an element from a collection while iterating over it. More subtle is the borrowed reference problem in systems code: a pointer into a buffer becomes dangling after the buffer is reallocated.

1.1.0.3 Reasoning difficulty.

Equational reasoning—substituting equals for equals—fails in the presence of mutation. If f(x) mutates x, then let y = f(x); g(y, x) is not equivalent to g(f(x), x), because the second occurrence of x observes different state. This makes refactoring hazardous and formal verification prohibitively expensive.

Japl’s dual-layer design addresses all three problems. Pure values cannot be mutated, so they are immune to data races, aliasing bugs, and reasoning failures. Resources can be mutated, but ownership tracking ensures that at most one reference exists at any time, restoring the ability to reason locally about mutation effects.

1.2 Contributions

This paper makes the following contributions:

1. We present a formal account of Japl’s dual-layer type system, connecting it to Girard’s linear logic and the theory of substructural type systems ([sec:formal,sec:dual-layer]).

2. We define the ownership semantics for the resource layer, including consumption, borrowing, region-based inference, and uniqueness inference (5).

3. We formalize Japl’s resource types and prove that well-typed programs satisfy resource safety: every acquired resource is eventually released exactly once ([sec:resource-types,sec:proofs]).

4. We describe the interaction between the two layers, including the borrowing protocol and escape hatches (7).

5. We provide a detailed comparison with six other language designs (8) and describe an implementation strategy for the dual-layer runtime (9).

1.3 Paper Organization

2 surveys related work. 3 develops the formal framework: linear logic, substructural type systems, and categorical semantics. 4 presents Japl’s dual-layer model. 5 details ownership semantics. 6 defines resource types. 7 describes layer interaction. 8 compares with related languages. 9 discusses implementation. 10 contains formal proofs. 11 reflects on practical trade-offs. 12 concludes.

2 Background and Related Work

2.1 Substructural Type Systems

The structural rules of a type system determine how hypotheses in a typing context may be used. Classical logic (and the simply-typed lambda calculus) admits three structural rules: weakening (a hypothesis may be ignored), contraction (a hypothesis may be duplicated), and exchange (hypotheses may be reordered). Dropping one or more of these rules yields a substructural type system :

Japl’s resource layer employs linear types: each resource must be consumed exactly once. The pure layer uses standard structural types (with all three rules), since immutable values can be freely shared, duplicated, or ignored.

2.2 Linear Logic

Girard’s linear logic  provides the proof-theoretic foundation for linear type systems. The key connectives are:

• \(A \multimap B\) (linear implication): consuming one \(A\) produces one \(B\).

• \(A \otimes B\) (tensor / multiplicative conjunction): both \(A\) and \(B\) are available simultaneously, each used exactly once.

• \({\mathop{!}}A\) (of course / exponential): an unlimited supply of \(A\), recoverable as many times as needed.

• \(A \,\&\, B\) (with / additive conjunction): a choice between \(A\) and \(B\), where only one is consumed.

• \(A \oplus B\) (plus / additive disjunction): exactly one of \(A\) or \(B\) is provided.

The exponential \({\mathop{!}}A\) is critical: it bridges linear and unrestricted worlds. In Japl, the pure layer corresponds to the \({\mathop{!}}\)-fragment of linear logic: every pure value implicitly carries an exponential modality, meaning it can be freely duplicated and discarded. The resource layer corresponds to the linear fragment proper.

2.3 Rust’s Ownership and Borrowing

Rust  pioneered the use of ownership and borrowing as a practical mechanism for memory safety without garbage collection. Rust’s key rules are:

1. Each value has a single owner.

2. Ownership can be transferred (moved).

3. References can be borrowed: either one mutable reference or any number of immutable references, but not both simultaneously.

4. Values are dropped (destructors run) when the owner goes out of scope.

The RustBelt project  formalized Rust’s type system using the Iris separation logic framework, proving that well-typed Rust programs (even those using unsafe) satisfy memory safety when the unsafe blocks are locally sound.

Japl differs from Rust in a fundamental architectural decision: Rust applies ownership to all values, requiring lifetime annotations even for purely functional data transformations. Japl restricts ownership to the resource layer, leaving the pure layer free of ownership concerns.

2.4 Clean’s Uniqueness Types

Clean  uses uniqueness types to ensure that a value has at most one reference. If a value is unique, it can be destructively updated in place without violating referential transparency, because no other reference can observe the mutation.

Clean’s uniqueness attribute * is propagated by the type checker. For example, *File denotes a unique file handle that can be read or written. Uniqueness types are closely related to linear types: a unique value must be used exactly once (or threaded through a computation that returns a new unique value).

Japl’s resource layer is inspired by Clean’s approach but extends it with explicit own and ref qualifiers, region inference, and integration with an algebraic effect system.

2.5 Linear Haskell

Linear Haskell  extends Haskell with linear arrow types \(a \multimap b\), allowing functions to specify that an argument must be consumed exactly once. The key insight is retrofitting: linear types are added to an existing language without breaking backward compatibility, by making linearity a property of function arrows rather than types.

Japl takes a complementary approach. Rather than adding linearity to arrows, Japl adds linearity to a distinguished class of types (resource types). This makes the boundary between linear and unrestricted code syntactically visible.

2.6 Region-Based Memory Management

Tofte and Talpin  introduced region-based memory management, where objects are allocated into lexically scoped regions and deallocated en masse when the region goes out of scope. The Cyclone language  brought regions to a C-like setting with static safety guarantees.

Region inference automatically determines which region each allocation belongs to, minimizing annotation burden. Japl uses region-like reasoning in its ownership inference pass: the compiler determines the lifetime of each resource and inserts release operations at the appropriate scope boundaries.

2.7 Capability-Based Security

The capability model of security  organizes access control around unforgeable tokens (capabilities) rather than identity-based access control lists. A process can only perform an operation if it holds the appropriate capability.

Japl applies this principle to resource access: a file can only be read if the function holds an Owned<File> or ref File capability. The effect system (Io, Net) further restricts which capabilities can be exercised in a given context.

2.8 Austral, Roc, and Koka

Several recent languages explore design points closely related to Japl’s.

2.8.0.1 Austral.

Austral  is a systems language with linear types in which every type is either free (unrestricted, may be copied and discarded) or linear (must be consumed exactly once). The dichotomy mirrors Japl’s pure/resource split, but Austral applies it within a single layer: there is no garbage-collected pure heap, and all memory management is explicit. Japl’s dual-layer design adds a GC-managed pure layer for ergonomics, and borrowing via \(\mathsf{ref}\;T\) for non-consuming reads, which Austral lacks.

2.8.0.2 Roc.

Roc is a functional language that targets application-level programming and uses a capability-based effect system in which all side effects flow through platforms. Like Japl, Roc keeps the vast majority of code pure and pushes effects to the boundary. Unlike Japl, Roc does not expose linear or ownership types to the programmer; resource management is delegated entirely to the platform layer.

2.8.0.3 Koka.

Koka  pioneered row-typed algebraic effects with automatic effect inference. Japl’s effect system draws on Koka’s design, but Koka does not provide linear types or an ownership discipline for resources. The combination of row-typed effects and linear resource tracking is a distinctive feature of Japl’s design.

2.9 Algebraic Effects and Handlers

Algebraic effects  provide a structured alternative to monads for describing side effects. An effect signature declares a set of operations; an effect handler provides implementations for those operations.

Japl’s effect system (Io, State[s], Fail[e], etc.) draws on algebraic effects. Effects form a commutative monoid under composition, and effect handlers serve as natural transformations from effectful computations to pure results . The interaction between effects and linear types is a key contribution of this paper: resource operations are effectful (with Io), and the linear discipline ensures that effect handlers cannot accidentally duplicate or discard resources.

3 Formal Framework

This section develops the type-theoretic and logical foundations of Japl’s dual-layer system.

3.1 Linear Type Theory

We begin with a standard presentation of the linear lambda calculus .

The typing judgment \(\Gamma; \Delta \vdash e : A\) asserts that expression \(e\) has type \(A\) under unrestricted context \(\Gamma\) and linear context \(\Delta\), where every assumption in \(\Delta\) is consumed exactly once.

The \({\mathop{!}}\)-I rule requires that the expression \(e\) use no linear resources: only unrestricted values can be promoted to the exponential. This is the formal counterpart of Japl’s rule that pure values cannot capture resources.

3.2 Connection to Girard’s Linear Logic

The Curry-Howard correspondence extends to linear logic: proofs correspond to programs, propositions to types, and cut-elimination to evaluation .

In Japl’s dual-layer system, the Curry-Howard correspondence manifests directly: pure-layer types correspond to the \({\mathop{!}}\)-fragment (all types implicitly carry \({\mathop{!}}\)), while resource-layer types correspond to the linear fragment (no implicit \({\mathop{!}}\)).

3.3 Categorical Semantics

The categorical semantics of linear types provides a rigorous foundation for the dual-layer design.

This result is directly relevant to Japl:

3.4 Compact Closed Categories and Duality

In the full linear logic setting, the multiplicative fragment admits a notion of duality: every type \(A\) has a dual \(A^\perp\), and the category of types forms a \(\ast\)-autonomous category .

While Japl does not expose full classical linear logic to the programmer, the duality principle manifests in the resource layer’s consumption pattern: acquiring a resource of type \(R\) creates an obligation (dual) to release it. The linear type system ensures that this obligation is always discharged.

4 JAPL’s Dual-Layer Model

This section presents the core design of Japl’s two-layer type and memory system.

4.1 Design Philosophy

The dual-layer model is motivated by an empirical observation: most code does not need mutation. Business logic, data transformations, protocol parsing, serialization, routing—all of these are naturally expressed as pure functions over immutable values. Mutation is needed only at the boundaries: reading files, writing sockets, managing GPU memory, interacting with foreign libraries.

By restricting ownership tracking to the resource layer, Japl achieves two goals simultaneously:

1. Ergonomics: The vast majority of code is free of ownership annotations, lifetime parameters, and borrow-checker errors.

2. Safety: The code that does interact with mutable resources is subject to a rigorous linear discipline that prevents resource leaks, use-after-free, and double-free.

4.2 The Pure Layer

The pure layer encompasses all immutable values: algebraic data types, records, tuples, lists, maps, strings, closures, and numeric types.

Pure values have the following properties:

• Immutable: Once created, a pure value never changes.

• GC-managed: Memory is reclaimed by a generational, per-process garbage collector.

• Freely shareable: Pure values can be passed to any number of functions, stored in any number of data structures, and sent to any number of processes.

• Structurally typed: Two values with the same structure have the same type (row polymorphism for records).

-- Pure values: immutable, GC-managed, freely shareable
let data = [1, 2, 3, 4, 5]
let copy = data  -- sharing is fine; data is immutable

-- Pure function: transforms data, no side effects
fn transform(data: List[Int]) -> List[Int] =
  List.map(data, fn x -> x * 2)

-- Composition of pure functions
fn process_order(order: Order) -> Invoice =
  order
  |> validate
  |> calculate_totals
  |> apply_discounts
  |> generate_invoice

4.3 The Resource Layer

The resource layer encompasses all mutable, owned values: file handles, network sockets, database connections, GPU buffers, FFI pointers, and mutable arrays.

resource File
resource Socket

-- Opening a file acquires ownership (manual management via let)
fn read_config(path: Path) -> Result[Config, ReadError] with Io =
  let file = File.open(path, Read)?
  let contents = File.read_all(file)?
  File.close(file)  -- ownership consumed; compile error if omitted
  parse_config(contents)

-- Ownership transfer: send consumes the socket, returns it
fn send(socket: Owned[Socket], bytes: Bytes)
    -> (Owned[Socket], Int) with Io =
  let n = Socket.write(socket, bytes)
  (socket, n)

4.4 The Split in Practice

The boundary between pure and resource layers is clean and syntactically visible. Consider a web server:

-- Pure layer: all business logic
fn route(req: Request) -> Response =
  match req.method, req.path with
  | Get, "/users/" ++ id -> get_user(id)
  | Post, "/users"       -> create_user(req.body)
  | _                    -> not_found()

fn get_user(id: String) -> Response =
  match UserRepo.find(id) with
  | Some(user) -> Response.json(200, User.to_json(user))
  | None       -> Response.json(404, error_json("not found"))

-- Resource layer: IO boundary
fn serve(listener: Owned[TcpListener])
    -> Never with Io, Process[ServerMsg] =
  let (listener, conn) = Tcp.accept(listener)
  let _ = Process.spawn(fn -> handle_conn(conn))
  serve(listener)

fn handle_conn(conn: Owned[TcpSocket]) -> Unit with Io =
  let (conn, req_bytes) = Tcp.read(conn)
  let req = parse_request(req_bytes)  -- pure
  let resp = route(req)               -- pure
  let conn = Tcp.write(conn, serialize_response(resp))
  Tcp.close(conn)

In this example, the pure functions route, get_user, parse_request, and serialize_response make up the majority of the code and require no ownership annotations. Only serve and handle_conn, which interact with TCP sockets, operate in the resource layer.

4.5 Formal Typing Judgment

The dual-layer system uses a combined typing judgment:

5 Ownership Semantics

5.1 Owned\(\langle T \rangle\)

The type \(\mathsf{Owned}\langle T \rangle\) represents exclusive ownership of a resource of type \(T\). The owner has three rights:

1. Use: Perform operations on the resource (read, write).

2. Transfer: Pass ownership to another function or process.

3. Release: Deallocate the resource, releasing its underlying system resource.

These rights are mutually exclusive over time: once ownership is transferred or the resource is released, the original holder loses all rights.

5.2 Consumption and Return Patterns

Japl supports several patterns for resource consumption:

5.2.0.1 Terminal consumption.

The resource is released and not returned:

fn close_file(file: Owned[File]) -> Unit with Io =
  File.close(file)
  -- file is consumed; cannot be used after this point

5.2.0.2 Threaded consumption.

The resource is used and then returned with updated state:

fn read_line(file: Owned[File])
    -> (Owned[File], String) with Io =
  let (file, line) = File.read_line(file)
  (file, line)

5.2.0.3 Fork-join consumption.

Ownership is temporarily split (borrowing) and then rejoined:

fn copy_file(src: Owned[File], dst: Owned[File])
    -> (Owned[File], Owned[File]) with Io =
  let bytes = File.read_all(src)
  let dst = File.write_all(dst, bytes)
  (src, dst)

5.3 Borrowing

Borrowing allows temporary read-only access to a resource without transferring ownership.

fn peek(buf: ref Buffer) -> Byte =
  Buffer.get(buf, 0)

fn process(buf: Owned[Buffer]) -> (Owned[Buffer], Byte) with Io =
  let byte = peek(ref buf)  -- borrow for read-only access
  (buf, byte)               -- buf is still owned here

The key constraint is that borrows cannot outlive the owner: the borrowed reference \(\mathsf{ref}\; T\) is valid only within the scope where it is created. This is enforced statically by the compiler.

5.4 Region-Based Inference

Japl uses region-based inference  to automatically determine resource lifetimes and insert release operations.

The compiler’s region inference pass operates in three phases:

1. Constraint generation: For each resource allocation, generate a region variable. For each use, generate a constraint that the resource’s region must contain the use site. For each ownership transfer, propagate the region.

2. Constraint solving: Solve the region constraints to find the minimal region for each resource.

3. Insertion: Insert release operations at region boundaries where resources go out of scope.

fn process_query(url: String, sql: String)
    -> Result[Rows, DbError] with Io =
  use conn = Db.connect(url)?
  let result = Db.query(ref conn, sql)?
  -- compiler inserts: Db.close(conn) here
  Ok(result)

5.5 Uniqueness Inference

Beyond region inference, Japl performs uniqueness inference to determine when a value has a single reference, enabling in-place mutation optimizations.

This optimization is particularly important for the common pattern of threading state through recursive functions:

fn server_loop(state: ServerState) -> Never with Process[Msg] =
  let msg = Process.receive()
  -- If state is unique (no other references), the update
  -- { state | count = state.count + 1 } is performed in-place.
  let new_state = { state | count = state.count + 1 }
  server_loop(new_state)

6 Resource Types

6.1 Declaring Resource Types

Resource types are declared with the resource keyword:

resource File
resource Socket
resource DbConnection
resource GpuBuffer
resource MutableArray[a]

The resource keyword instructs the compiler to apply linear typing rules to values of this type. A resource cannot be silently dropped, duplicated, or aliased.

6.2 Resource Lifecycle

Every resource follows a lifecycle:

1. Acquisition: A resource is created via a constructor (e.g., File.open, Tcp.connect). The constructor returns \(\mathsf{Owned}\langle R \rangle\).

2. Use: The resource is operated on via functions that take \(\mathsf{Owned}\langle R \rangle\) or \(\mathsf{ref}\; R\). Functions that take \(\mathsf{Owned}\langle R \rangle\) must return it (threaded pattern) or consume it (terminal pattern).

3. Release: The resource is released via a destructor (e.g., File.close, Tcp.disconnect). The destructor consumes \(\mathsf{Owned}\langle R \rangle\) and returns no resource.

We defer the proof to 10.

6.3 The use Binding

The use keyword introduces a linear binding with automatic release semantics:

fn read_entire_file(path: String) -> Result[String, IoError] with Io =
  use file = File.open(path, Read)?
  let contents = File.read_all(file)?
  -- File.close(file) is automatically inserted by the compiler
  -- at the end of the `use` scope
  Ok(contents)

The use binding desugars to a try-finally pattern: even if the body raises an error (via the ? operator or a crash), the resource is released.

6.4 Parametric Resource Types

Resources can be parametric:

resource MutableArray[a]

fn sort_in_place(arr: own MutableArray[Int])
    -> own MutableArray[Int] =
  let len = MutableArray.length(arr)
  loop i = 0, arr = arr while i < len do
    loop j = i + 1, arr = arr while j < len do
      if MutableArray.get(arr, j) < MutableArray.get(arr, i) then
        let arr = MutableArray.swap(arr, i, j)
        continue(j + 1, arr)
      else
        continue(j + 1, arr)
    continue(i + 1, arr)
  arr

The linearity constraint applies to the outer resource container, not to its type parameter. The elements of a MutableArray[Int] are pure Int values and can be freely copied.

6.5 Freezing: Resource to Value Conversion

A resource can be frozen to produce an immutable value, transferring data from the resource layer to the pure layer:

fn build_message() -> Bytes with Io =
  let buf = Buffer.alloc(1024)          -- resource layer
  let buf = Buffer.write(buf, 0, header)
  let buf = Buffer.write(buf, 64, payload)
  Buffer.freeze(buf)                    -- pure layer: immutable Bytes
  -- buf is consumed; only the frozen Bytes value remains

Freezing corresponds to the functor \(G : \mathcal{L} \to \mathcal{C}\) in the LNL model (7): it maps a linear resource to an unrestricted pure value.

7 Interaction Between Layers

7.1 Pure Functions Using Resources

Pure functions cannot own resources, but they can borrow them. A function that borrows a resource via \(\mathsf{ref}\; T\) does not participate in the ownership protocol; it simply reads the resource’s current state.

-- This function is pure except for the borrow
fn buffer_checksum(buf: ref Buffer) -> Int =
  let bytes = Buffer.to_bytes_view(buf)  -- read-only view
  Bytes.fold(bytes, 0, fn acc, b -> acc + b)

fn validate_and_send(buf: Owned[Buffer], sock: Owned[Socket])
    -> (Owned[Buffer], Owned[Socket]) with Io =
  let sum = buffer_checksum(ref buf)  -- borrow for pure computation
  if sum > 0 then
    let (sock, _) = Socket.send(sock, Buffer.to_bytes(ref buf))
    (buf, sock)
  else
    (buf, sock)

7.2 Ownership Transfer Between Processes

When a resource is sent to another process, ownership transfers:

fn producer() -> Unit with Io, Process[ProducerMsg] =
  let buf = Buffer.alloc(4096)
  let buf = Buffer.write(buf, 0, generate_data())
  -- Ownership transfers to the consumer process
  Process.send(consumer_pid, ProcessBuffer(buf))
  -- buf is consumed; using it here is a compile error

fn consumer() -> Never with Io, Process[ConsumerMsg] =
  match Process.receive() with
  | ProcessBuffer(buf) ->
      -- We now own buf
      let data = Buffer.freeze(buf)
      process_data(data)
      consumer()

7.3 The Escape Hatch

For interoperability with C libraries and low-level systems code, Japl provides an unsafe escape hatch that allows bypassing linearity checks:

-- unsafe block: linearity is not checked
fn raw_mmap(fd: Owned[File], size: Int) -> Owned[MappedRegion] with Io =
  unsafe {
    let ptr = foreign_mmap(File.raw_fd(ref fd), size)
    MappedRegion.from_raw(ptr, size)
  }
  -- Outside unsafe: normal linearity rules apply

The unsafe keyword has several properties:

1. It must appear explicitly in the source code, making it searchable and auditable.

2. It does not propagate: a function containing unsafe can still present a safe interface to its callers.

3. It is tracked by the effect system: unsafe blocks require the Unsafe effect, which cannot be silently introduced.

7.4 Effect System Interaction

Resource operations are effectful: they carry the Io effect. The effect system and the ownership system cooperate:

8 Comparison with Related Languages

8.1 Overview

8.2 Rust: Full Borrow Checker

Rust applies its ownership and borrowing discipline to every value, including purely functional data. This provides strong guarantees—no GC is needed, and memory safety is ensured at compile time—but imposes a significant annotation burden.

Consider a simple data transformation in Rust:

fn transform(data: Vec<i32>) -> Vec<i32> {
    data.into_iter().map(|x| x * 2).collect()
}

The programmer must choose between Vec<i32> (ownership transfer), &Vec<i32> (immutable borrow), and &mut Vec<i32> (mutable borrow). For a pure transformation, this choice is an unnecessary cognitive burden.

In Japl, the same function requires no ownership annotations:

fn transform(data: List[Int]) -> List[Int] =
  List.map(data, fn x -> x * 2)

The trade-off is that Japl’s pure layer requires a garbage collector, while Rust avoids GC entirely. We argue that this trade-off is worthwhile for application-level code, where GC pauses are negligible relative to I/O latency.

8.3 Go: GC Everything

Go takes the opposite extreme: all memory is garbage-collected, and there is no ownership system. Resources are managed by convention (defer and the io.Closer interface) rather than by the type system.

The consequence is that resource leaks are possible:

func processFile(path string) error {
    f, err := os.Open(path)
    if err != nil { return err }
    // Easy to forget: defer f.Close()
    data, err := io.ReadAll(f)
    // If we return here, f is leaked
    ...
}

Japl’s linear types make this class of bug impossible: the compiler rejects any program that fails to consume a resource.

8.4 Haskell: The IO Monad

Haskell confines side effects to the IO monad, ensuring that pure functions are referentially transparent. However, the monadic style has several drawbacks:

1. Monadic binding (>>=) is syntactically heavier than direct-style code.

2. Composing different effects (state, error, IO) requires monad transformers, which are notoriously difficult to use.

3. Resources within IO are not linearly tracked; finalizers and bracket provide safety but not compile-time guarantees.

Japl’s effect system provides effect tracking without monadic syntax: effects are listed after with in function signatures, and composition is automatic (effects form a commutative monoid). The resource layer adds linear tracking that Haskell’s IO lacks.

8.5 Erlang: Copy Everything

Erlang achieves concurrency safety by making all values immutable and copying data between processes. This eliminates shared mutable state entirely but has performance implications for large data transfers.

Japl inherits Erlang’s process isolation model for pure values but extends it with ownership transfer for resources: a resource can be moved between processes without copying, while maintaining the invariant that only one process owns it at a time.

8.6 OCaml: Mutable Refs

OCaml allows mutation through mutable record fields and ref cells. The type system does not distinguish pure and impure code; any function may have side effects.

This pragmatic approach simplifies the type system but sacrifices the ability to reason about purity. Japl’s effect annotations (with Io, with State[s]) restore this reasoning while keeping the annotation burden low (effects are inferred within function bodies).

8.7 Clean: Uniqueness Types

Clean’s uniqueness types  are the closest relative of Japl’s resource layer. Clean uses a * attribute to mark unique values; the compiler ensures that unique values are not aliased.

Japl extends Clean’s approach in several ways:

1. Explicit layer separation: Japl does not apply uniqueness to all types; only declared resource types are subject to linear discipline.

2. Borrowing: Clean does not have a borrowing mechanism; in Clean, any use of a unique value consumes it. Japl’s ref qualifier allows non-consuming reads.

3. Effect integration: Japl’s resource operations are annotated with effects, providing an additional layer of safety.

4. Process integration: Japl supports ownership transfer between processes, which Clean (not being an actor-based language) does not address.

8.8 Summary of Trade-offs

Japl is the only language in this comparison that simultaneously provides data-race freedom, compile-time resource safety, low annotation burden (for the majority of code), and effect tracking. The cost is a garbage collector for the pure layer; we argue in 11 that this is an acceptable trade-off.

9 Implementation

9.1 Architecture Overview

The Japl compiler and runtime implement the dual-layer model as follows:

1. Parser: Produces an AST with explicit use, own, and ref annotations.

2. Type checker: Performs bidirectional type checking with local inference. Maintains separate unrestricted (\(\Gamma\)) and linear (\(\Delta\)) contexts.

3. Linearity checker: Verifies that all linear variables are consumed exactly once on every execution path.

4. Region inference: Assigns regions to resource allocations and inserts release operations.

5. Uniqueness analysis: Identifies pure values with a single reference for in-place update optimization.

6. Code generation: Compiles to native code via LLVM or Cranelift.

7. Runtime: Manages the dual-layer memory model at execution time.

9.2 Type Checker Implementation

The type checker uses a splitting judgment to partition the linear context among subexpressions :

For function application \(e_1\; e_2\), the type checker:

1. Generates a fresh split of the current linear context.

2. Checks \(e_1\) against \(\Delta_1\).

3. Checks \(e_2\) against \(\Delta_2\).

4. Verifies that \(\Delta_1\) and \(\Delta_2\) are both fully consumed.

For conditionals and pattern matching, the type checker verifies that all branches consume the same set of linear variables:

9.3 Linearity Checking Algorithm

The linearity checker runs as a separate pass after type checking. It traverses the typed AST and maintains a set of “live” linear variables. The algorithm is:

1. At a let binding of a resource type: add the variable to the live set.

2. At a use of a linear variable: remove it from the live set. If already removed, report a “use after move” error.

3. At a branch point (if/match): check each branch independently; verify that all branches have the same live set at exit.

4. At function exit: verify that the live set matches the function’s return type (i.e., any linear variable still live must be returned).

5. At scope exit for use bindings: if the variable is still live, insert a release call.

9.4 Runtime Memory Model

The runtime maintains two memory regions per process:

9.4.0.1 Immutable heap (GC-managed).

All pure values reside here. The garbage collector is generational and per-process:

• Nursery: Small, per-process bump allocator. Most values die young and are collected cheaply.

• Old generation: Surviving values are promoted to a shared old generation, collected concurrently.

• No write barriers: Since data is immutable, there are no pointer mutations to track. This significantly simplifies the GC.

• Process death: When a process terminates, its entire nursery is reclaimed instantly.

9.4.0.2 Resource arena (ownership-managed).

All linear resources reside here. There is no garbage collection; resources are freed deterministically when consumed:

• Allocation: Resources are allocated in a per-process arena.

• Deallocation: When a resource is consumed (released), its memory is immediately freed.

• Transfer: When ownership is transferred to another process, the resource is moved from one process’s arena to another’s.

• No fragmentation: Arena allocation avoids the fragmentation problems of general-purpose allocators.

9.5 Compile-Time Ownership Verification

The compiler performs ownership verification as a fixed-point computation over the control-flow graph (CFG):

1. Build the CFG for each function.

2. At each CFG node, compute the set of live linear variables.

3. At each join point, check that the live sets from all predecessors are identical.

4. At the function exit node, check that the live set matches the expected output (linear variables that appear in the return type).

5. If any check fails, emit a diagnostic with the offending variable and the point where it was consumed or escaped.

This analysis is similar to liveness analysis in traditional compilers but with the additional constraint that each linear variable must be consumed exactly once, not “at least once” or “at most once.”

9.6 Performance Characteristics

The dual-layer design has favorable performance characteristics:

• Pure-layer overhead: GC pauses are bounded by the nursery size and are per-process (no global stop-the-world). Uniqueness inference eliminates unnecessary copies.

• Resource-layer overhead: Zero runtime overhead beyond the actual resource operations; ownership is verified entirely at compile time.

• Combined: The compiler can optimize across layers. For example, a buffer that is allocated, filled, and frozen within a single function can be stack-allocated if uniqueness analysis proves it does not escape.

10 Formal Proofs

This section proves type safety and resource safety for Japl’s dual-layer system. We work with a core calculus \(\lambda^{\mathsf{JR}}\) (JAPL Resources) that captures the essential features.

10.1 Syntax of \(\lambda^{\mathsf{JR}}\)

10.2 Operational Semantics

We write \(\bot_R\) for the default initial state of resource type \(R\): the distinguished value that a freshly allocated resource holds before any operations have been performed on it. Each resource type declaration implicitly defines its \(\bot_R\) (e.g., an empty buffer, an unconnected socket descriptor).

10.3 Type Safety

10.4 Resource Safety

11 Discussion

11.1 When Ownership Pressure Leaks

The dual-layer design succeeds when the boundary between pure and resource code is clean. In practice, however, there are cases where ownership concerns propagate into otherwise-pure code:

11.1.0.1 Resource-carrying data structures.

If a data structure contains a resource (e.g., a list of open file handles), the entire structure becomes linear. This forces the programmer to manage ownership for the container, even if the business logic only cares about the data inside.

11.1.0.2 Callbacks with resources.

A higher-order function that accepts a callback may need to thread resources through the callback, complicating the interface.

11.1.0.3 Long-lived resources.

A database connection pool manages resources with lifetimes that span many function calls. The pool itself becomes a resource, and every function that uses the pool must participate in the ownership protocol.

11.2 Mitigations

Japl provides several mechanisms to reduce ownership pressure:

11.2.0.1 Borrowing (ref).

Most pure functions that need to read a resource can take a borrowed reference, avoiding ownership transfer entirely.

11.2.0.2 Scoped resources (use).

The use binding automatically manages resource lifetimes within a scope, reducing boilerplate.

11.2.0.3 Process encapsulation.

Long-lived resources can be owned by a dedicated process, which exposes a pure message-passing interface. Other processes interact with the resource through messages, never seeing the ownership:

-- The database process owns the connection
fn db_process(conn: Owned[DbConnection])
    -> Never with Io, Process[DbMsg] =
  match Process.receive() with
  | Query(sql, reply) ->
      let (conn, result) = Db.query(conn, sql)
      Reply.send(reply, result)
      db_process(conn)
  | Shutdown ->
      Db.close(conn)
      Process.exit(Normal)

-- Callers never see Owned[DbConnection]
fn get_user(db: Pid[DbMsg], id: UserId)
    -> Result[User, DbError] with Process =
  let result = Process.call(db, fn reply -> Query(user_sql(id), reply))
  parse_user_row(result)

This pattern is the recommended way to manage long-lived resources in Japl: the process boundary naturally encapsulates the ownership, and the caller’s interface is pure message-passing.

11.2.0.4 Region-based grouping.

Multiple resources acquired in the same scope can be grouped into a single region, reducing the number of individual ownership threads.

11.3 The 80/20 of Resource Management

Our experience with prototype Japl applications suggests the following distribution:

• 80% of code is pure: data transformations, business logic, protocol handling, serialization. No ownership annotations needed.

• 15% of code uses scoped resources (use): open file, read, close; connect, query, disconnect. Ownership is automatic via the use binding.

• 5% of code requires explicit ownership management: long-lived resources, cross-process transfers, complex resource graphs. This is where the linear type system provides its greatest value.

The dual-layer design ensures that the 80% majority pays no annotation cost, while the 5% minority gets strong compile-time guarantees.

11.4 Effect System Synergy

The effect system and the ownership system reinforce each other. The effect system ensures that resource operations are visible in function signatures (with Io), preventing hidden side effects. The ownership system ensures that resources are properly managed even when effects are composed.

Together, they provide a stronger guarantee than either alone: a function with signature fn(x: Int) -> Int is guaranteed to be pure—it cannot secretly open a file, allocate a buffer, or access the network.

11.5 Comparison with Monadic IO

The Haskell approach confines all effects to the IO monad, including both resource management and general side effects. This conflates two concerns:

1. Effect tracking: Knowing that a function performs IO.

2. Resource management: Ensuring that resources are properly released.

Japl separates these concerns: the effect system handles (1), and the ownership system handles (2). This separation allows finer-grained reasoning: two functions may both have effect Io, but one manages resources (visible in its type via Owned) while the other merely reads a file.

11.6 Limitations

The dual-layer approach has several limitations:

1. GC dependency: The pure layer requires a garbage collector, making Japl unsuitable for environments where GC is unacceptable (embedded systems, real-time audio).

2. Layer crossing cost: Moving data between layers (freezing a buffer into immutable bytes) may involve a copy if the resource is not uniquely held.

3. Learning curve: Programmers must understand the distinction between pure and resource types, even if the pure layer requires no annotations.

4. Expressiveness: Some patterns that are natural in Rust (e.g., self-referential structures with lifetimes) are more difficult to express in Japl’s simpler ownership model.

11.7 Future Work

Several directions remain for future investigation:

1. Graded linearity: Allowing resources to be used exactly \(n\) times (useful for connection pools with bounded concurrency).

2. Session types: Extending resource types with session type protocols, ensuring that resources are used in the correct order (e.g., connect, authenticate, query, disconnect).

3. Dependent resource types: Allowing resource types to depend on values, enabling richer invariants (e.g., a file handle that tracks whether it is open for reading, writing, or both).

4. Formal verification: Connecting Japl’s type system to separation logic via the LNL model, enabling machine-checked proofs of resource safety.

12 Conclusion

We have presented Japl’s second core principle: mutation is local and explicit. The dual-layer type system—pure values managed by GC, linear resources managed by ownership—achieves a design point that has not been explored by prior languages:

1. Safety without pervasive annotation: The majority of code lives in the pure layer and requires no ownership annotations, lifetime parameters, or borrow-checker reasoning.

2. Resource safety by construction: Every resource acquired by a well-typed program is released exactly once, as proven by our type safety and resource safety theorems.

3. Effect visibility: The effect system makes mutation visible in function signatures, enabling equational reasoning for pure code and local reasoning for effectful code.

4. Process integration: Ownership transfer between processes extends the linear discipline to concurrent settings, while process encapsulation hides ownership behind pure message-passing interfaces.

The formal framework—rooted in Girard’s linear logic, Benton’s LNL adjunction model, and the theory of substructural type systems—provides a rigorous foundation for the design. The categorical interpretation (3.3) shows that Japl’s dual-layer system is not an ad hoc engineering compromise but a principled instantiation of the well-studied relationship between linear and Cartesian closed categories.

We believe that the dual-layer approach represents a practical sweet spot for language design: it gives systems programmers the control they need over resources, while giving application programmers the simplicity they want for everyday code. The principle that mutation should be local and explicit—not absent, not pervasive, but controlled—is central to Japl’s mission of being “pure by default, concurrent by design, resource-safe by construction, distributed without apology.”

13 Complete Typing Rules for \(\lambda^{\mathsf{JR}}\)

For reference, we present the complete set of typing rules for the core calculus.

14 Extended Examples

14.1 Database Connection Pool

resource DbConnection

type PoolMsg =
  | Checkout(Reply[Owned[DbConnection]])
  | Return(Owned[DbConnection])
  | Shutdown

fn pool_process(conns: List[Owned[DbConnection]],
                waiting: List[Reply[Owned[DbConnection]]])
    -> Never with Io, Process[PoolMsg] =
  match Process.receive() with
  | Checkout(reply) ->
      match conns with
      | [conn, ..rest] ->
          Reply.send(reply, conn)
          pool_process(rest, waiting)
      | [] ->
          pool_process(conns, List.append(waiting, [reply]))
  | Return(conn) ->
      match waiting with
      | [waiter, ..rest] ->
          Reply.send(waiter, conn)
          pool_process(conns, rest)
      | [] ->
          pool_process([conn, ..conns], waiting)
  | Shutdown ->
      List.each(conns, fn conn -> Db.close(conn))
      Process.exit(Normal)

14.2 State Effect with Linear Resources

-- Explicit mutable state via effect
fn accumulate(items: List[Int]) -> Int with State[Int] =
  List.each(items, fn x -> State.modify(fn acc -> acc + x))
  State.get()

-- Resource layer: mutable buffer (ownership tracked)
fn fill_buffer(data: Bytes) -> Bytes with Io =
  let buf = Buffer.alloc(1024)
  let buf = Buffer.write(buf, 0, data)
  Buffer.freeze(buf)

-- Combining pure, state, and resource layers
fn process_and_store(items: List[Int], path: Path)
    -> Result[Unit, IoError] with Io =
  let total = State.run(0, fn -> accumulate(items))
  let file = File.open(path, Write)?
  File.write(file, Int.to_string(total))
  File.close(file)
  Ok(())

14.3 Safe FFI Wrapping

-- Foreign resource: a C library handle
resource CHandle

foreign "C" fn c_lib_open(config: CString) -> Ptr[CHandle]
foreign "C" fn c_lib_process(h: Ptr[CHandle], data: Ptr[Byte], len: CInt) -> CInt
foreign "C" fn c_lib_close(h: Ptr[CHandle]) -> Unit

-- Safe JAPL wrapper: all ownership is explicit
fn open_handle(config: String) -> Result[Owned[CHandle], Error] with Io =
  use cstr = CString.from(config)
  let ptr = unsafe c_lib_open(cstr)
  if Ptr.is_null(ptr) then Err(OpenFailed)
  else Ok(CHandle.from_raw(ptr))

fn process_data(handle: Owned[CHandle], data: Bytes)
    -> (Owned[CHandle], Result[Int, Error]) with Io =
  let result = unsafe c_lib_process(
    CHandle.as_ptr(ref handle),
    Bytes.as_ptr(data),
    Bytes.length(data)
  )
  if result < 0 then (handle, Err(ProcessFailed(result)))
  else (handle, Ok(result))

fn close_handle(handle: Owned[CHandle]) -> Unit with Io =
  unsafe c_lib_close(CHandle.into_raw(handle))