What One Owner Is Worth

The 31 cells as build left them. Each carries a count of how many references point at it. Every count is 1: the tree has one holder, the binding t.

inc_leaves(t) is the last thing main does with t. The call takes over the only reference, so when a match looks inside a Node, that cell is about to die, and the Node being built has the same shape. The compiler writes the new fields into the old cell.

Across the whole walk, inc_leaves allocates 0 cells. That number is read from the runtime's own allocation trace of this program, not estimated.

Now main reads the old tree again afterwards:

fn main(_c : Cap(IO.Console)) : Unit do
  let t = build(4, 1)
  let t2 = inc_leaves(t)
  println(int_to_string(sum_leaves(t2) - sum_leaves(t)))
end

Two holders, so the counts on the path climb to 2 as the walk descends, and nothing may be overwritten. inc_leaves allocates 31 cells: a complete second tree. The program is still correct; it is only slower. The fallback is automatic, and the compiler says where it happened:

`inc_leaves` builds a new copy instead of reusing `t` in place, because `t` is used again afterwards. [copy_shared]

-- WARNING: COPY --------------------------- shared.march

`inc_leaves` builds a new copy instead of reusing `t` in place, because `t` is used again afterwards. [copy_shared]
A function can update a value in place only when it holds the only reference to it; make this call the last use of `t` and `inc_leaves` reuses its memory instead of allocating.

27 |     let t2 = inc_leaves(t)
                             ^

    `t` is used again here, so it is still shared when `inc_leaves` runs:

28 |     println(int_to_string(sum_leaves(t2) - sum_leaves(t)))
                                                           ^
    run `march --explain copy_shared`

A holder need not be a variable. Here the tree is put in a Vault, March's shared table, before the transform, and inc_leaves(t) is again the last use in the code:

fn main(_c : Cap(IO.Console), _m : Cap(IO.Mut)) : Unit do
  let t = build(4, 1)
  let kept = Vault.new("trees")
  Vault.set(kept, "before", t)
  let t2 = inc_leaves(t)
  println(int_to_string(sum_leaves(t2)))
end

The static report sees the code and finds no second use:

No copies found: every value passed to a function that reuses it in place is its last use.

The runtime sees the count. The Vault holds a reference, so the walk copies all 31 cells anyway. That is the division of labour on this page: the compiler decides where reuse is possible, and the count decides whether it happens.

One owner also means no lock. The two halves of a uniquely held Node are disjoint, so each can be rewritten on its own task with nothing to synchronise:

fn inc_parallel(t : Tree) : Tree do
  match t do
  Leaf(n)    -> Leaf(n + 1)
  Node(l, r) ->
    match List.pmap_n([l, r], fn half -> inc_leaves(half), 2) do
    [left, right] -> Node(left, right)
    _ -> panic("two halves")
    end
  end
end

Two tasks, and inc_leaves allocates 0 cells. The list, the chunks and the task handles around it cost 11 small cells; the tree costs none.

The same tree, declared linear. The token is minted at the binding and consumed by inc_leaves, which takes a linear parameter and so promises to consume what it is given. This compiles.

fn inc_leaves(linear t : Tree) : Tree do
  match t do
  Leaf(n)    -> Leaf(n + 1)
  Node(l, r) -> Node(inc_leaves(l), inc_leaves(r))
  end
end

fn main() : Int do
  linear let t : Tree = Node(Leaf(1), Node(Leaf(2), Leaf(3)))
  sum_leaves(inc_leaves(t))
end

The sharing program from above, with the same declaration. The second use has no token to consume. Where the runtime copied, the type checker refuses:

The linear value `t` is used more than once here. [linear_used_twice]

-- LINEARITY ------------------------- linear_twice.march

The linear value `t` is used more than once here. [linear_used_twice]
Linear values must be consumed exactly once — they cannot be copied or ignored.

22 |     sum_leaves(t2) - sum_leaves(t)
                                     ^

    `t` was already consumed here:

21 |     let t2 = inc_leaves(t)
                             ^
    run `march --explain linear_used_twice`

A token that reaches the end of its scope unconsumed is the other error. For a tree it is only a wasted value; for a file handle or a session endpoint it is a leak, and linear is how March makes "you must close this" a type.

The linear value `t` was never used. [linear_never_used]

affine keeps half the rule. A branch may leave the token unused:

fn maybe_sum(t : affine Tree, wanted : Bool) : Int do
  if wanted do sum_leaves(t) else 0 end
end

It is the right word for a permission or a one-shot token: something you may decide not to use, but must never use twice.

The other half still holds.

fn twice(t : affine Tree) : Int do
  sum_leaves(t) + sum_leaves(t)
end

The affine value `t` is used more than once here. [linear_used_twice]

The compiler already knows which functions came out allocation-free. Asked, it names them:

`inc_leaves` is verified allocation-free; add @[no_alloc] to keep it that way.

That is one line of march --compile --report-contracts, and forge fix --contracts applies every such line.

With the attribute on, the check is made on the compiled form, after reuse and stack promotion have been decided, and it is made every build:

@[no_alloc]
fn inc_leaves(t : Tree) : Tree do
  match t do
  Leaf(n)    -> Leaf(n + 1)
  Node(l, r) -> Node(inc_leaves(l), inc_leaves(r))
  end
end

Reintroduce an allocation, here or in anything inc_leaves calls, and the build fails instead of the benchmark.

The bare form means no allocation at all. The check runs on the compiled form, where describe has been inlined into width_bare, so it names the allocation where it ended up:

fn describe(i : Int) : String do
  "item " ++ int_to_string(i)
end

@[no_alloc]
fn width_bare(i : Int) : Int do
  String.byte_size(describe(i))
end

In `width_bare`: `int_to_string` allocates.

-- CONTRACT ------------------------- contract_bare.march

`width_bare` is marked @[no_alloc] but allocates. [no_alloc]
  In `width_bare`: `int_to_string` allocates.

10 |   fn width_bare(i : Int) : Int do
          ^^^^^^^^^^

A tick, a frame, a request handler: code that allocates freely and frees all of it before returning has a property the bare form cannot say. transient asks where a value ends up, not whether one was made:

@[no_alloc(transient)]
fn width(i : Int) : Int do
  String.byte_size(describe(i))
end

This compiles. It fails if the function returns something it allocated, stores one into an object it did not allocate, or hands one to an actor, a Vault, a task or foreign code.

Some values never reach the heap at all. A variant with one constructor of two to four Int, Float or Bool fields lives in registers, so forward passes. Storing it into a field boxes it, and the contract says so:

@[no_alloc]
fn forward(yaw : Float, pitch : Float) : Vec3 do
  let cp = Math.cos(pitch)
  Vec3(0.0 -. Math.sin(yaw) *. cp, Math.sin(pitch), 0.0 -. Math.cos(yaw) *. cp)
end

@[no_alloc]
fn record(yaw : Float, pitch : Float, id : Int) : Hit do
  Hit(forward(yaw, pitch), id)
end

In `record`: constructor `Hit` is allocated here.

One limit to hold on to. The contract is about the function's own code. Give inc_leaves a caller that keeps the old tree and the build still passes, while at run time the walk allocates every cell again (5 on the 5-cell tree in that program). The copy belongs to the caller, and --why-copies is the tool that points at it.

What the contract cannot yet say is "at most N". A parser that allocates a few cells per token is not allocation-free, but its count is worth pinning. @[alloc_bound(N)] and a per-activation form for recursive functions are designed and not shipped; the design is in the repository, with its open item.