Linear Types

A linear value must be used exactly once — the compiler rejects code that drops it without consuming it, or uses it twice. This makes resource leaks and double-frees impossible to write.

Declaring a linear type

A plain type is unrestricted by default — any binding of it can be copied, dropped, or used any number of times. Linearity is requested at the binding site, with linear let, or on a function parameter with linear:

type FileHandle = FileHandle(Int)

fn read_file(path : String) : String do
  linear let fh = open_file(path)
  -- fh must be used before the function returns — the compiler tracks this
  let content = read_all(fh)   -- consumes fh
  content
end

Forgetting to use fh is a compile error:

fn bad(path : String) : String do
  linear let fh = open_file(path)
  "oops"    -- error: "The linear value `fh` was never used."
end

And using it twice is also a compile error:

fn also_bad(path : String) : String do
  linear let fh = open_file(path)
  let a = read_all(fh)
  let b = read_all(fh)   -- error: "The linear value `fh` is used more than once here."
  a ++ b
end

Always-linear types

always_linear type promotes every binding to linear without per-use-site annotations:

always_linear type DbConn = DbConn(Int)

Useful when you want the linearity guarantee enforced everywhere in the codebase, not just where the author remembered to write linear let.

Typestate: handles that track state

A typestate handle adds a phantom state parameter to an always_linear type, so the compiler can track not just “used exactly once” but which state the value is in at every point in the program:

always_linear type FileHandle(s) = FileHandle(Int)

tag FileTag
tag Closed
tag Open

State transitions are declared with transitions. Each via function must take the handle in its from state and return the handle — and only the handle, with no Result wrapper and no tuple — in its to state:

fn open_conn(h : FileHandle(Closed)) : FileHandle(Open) do
  ...
end

fn close_file(h : FileHandle(Open)) : FileHandle(Closed) do
  ...
end

transitions FileHandle do
  FileTag: Closed -> Open   via open_conn
  FileTag: Open   -> Closed via close_file
end

Calling close_file on a FileHandle(Closed) — or open_conn on a FileHandle(Open) — is a compile error: the compiler tracks exactly which state the handle is in and rejects the call before it ever runs.

Two things fall out of via’s “handle in, bare handle out” shape:

1. Acquiring the first handle is not itself a transition. open_file takes a String, not a FileHandle — the transitions block only covers moves between states of a value you already hold, not creating that value in the first place. It’s an ordinary function, free to return Result for the acquisition to fail:

   fn open_file(path : String) : Result(FileHandle(Closed), String) do
     ...
   end
   

2. An operation that also returns data can’t be declared as a via transition — its return type would be a tuple, not a bare handle — but it’s still typestate-checked, for free, by its argument type. read_chunk only accepts a FileHandle(Open), so calling it before open_conn is exactly as much a compile error as calling close_file twice would be; it just isn’t listed under transitions, since it can’t be:

   fn read_chunk(h : FileHandle(Open)) : (String, FileHandle(Open)) do
     ...
   end
   

Putting the pieces together:

fn process(path : String) : Result(String, String) do
  let? h0        = open_file(path)          -- FileHandle(Closed)
  let h1         = open_conn(h0)             -- FileHandle(Open)      — declared transition
  let (data, h2) = read_chunk(h1)             -- FileHandle(Open)      — checked via argument type
  match close_file(h2) do                     -- FileHandle(Closed)    — declared transition
    FileHandle(_) -> Ok(data)                 -- consumes the final handle
  end
end

Skipping the open_conn step and calling read_chunk(h0) directly is rejected at compile time:

expected `Open` but got `Closed`.

    let (data, h2) = read_chunk(h0)
                                 ^^
    This is argument #1 of a function call.

with for linear resource scopes

with pairs acquisition with guaranteed cleanup — useful when you want RAII-style deterministic release. It’s an alternative to let? for the same kind of Result-returning acquisition; here it drives the same state machine as process above:

fn process_with(path : String) : Result(String, String) do
  with Ok(h0) <- open_file(path) do
    let h1         = open_conn(h0)
    let (data, h2) = read_chunk(h1)
    match close_file(h2) do
      FileHandle(_) -> Ok(data)
    end
  else
    Err(e) -> Err(e)
  end
end

Just like any other linear binding, a handle acquired through with is tracked for double-use and drop: consuming h0 twice, or leaving h2 unconsumed, is a compile error the same way it would be with a plain let.

Complete example: safe socket lifecycle

mod Net do
  always_linear type Socket(s) = Socket(Int)

  tag SockTag
  tag Connected
  tag Disconnected

  fn connect(addr : String) : Result(Socket(Connected), String) do
    ...
  end

  fn disconnect(sock : Socket(Connected)) : Socket(Disconnected) do
    ...
  end

  -- `send_bytes`/`recv_bytes` take or return more than a bare handle (a
  -- payload alongside it), so — like `read_chunk` above — they can't be
  -- listed in `transitions`. Their `Socket(Connected)` argument type still
  -- makes calling them out of order (e.g. after `disconnect`) a compile
  -- error; `transitions` only needs to cover the pure handle-to-handle edges.
  fn send_bytes(sock : Socket(Connected), data : String) : Socket(Connected) do
    ...
  end

  fn recv_bytes(sock : Socket(Connected)) : (String, Socket(Connected)) do
    ...
  end

  transitions Socket do
    SockTag: Connected -> Disconnected via disconnect
  end

  fn echo_once(addr : String) : Result((), String) do
    let? sock0       = connect(addr)
    let (msg, sock1) = recv_bytes(sock0)
    let sock2        = send_bytes(sock1, msg)
    match disconnect(sock2) do
      Socket(_) -> Ok(())
    end
  end
end

recv_bytes consumes sock0 and returns (msg, Socket(Connected)) — a fresh handle. Using sock0 again after that — say, passing it to a second recv_bytes call — is a compile error: sock0 is linear, and it was already consumed. Forgetting to call disconnect at the end would also be a compile error — the final handle would be dropped without being consumed. And calling send_bytes or recv_bytes after disconnect fails too: their parameter type is Socket(Connected), and by then all you have is a Socket(Disconnected).