Copies, kinds, and the + mark

The chapter on affine values left a promise unkept: there is a way to use a value twice — write +x — but it is refused for some types and not others. This chapter is about what decides that, and about the loose end from the lists chapter, where List.range returned a List<&2, Nat> and nobody said what the &2 was.

Three quantities

A value can be bound three ways. The mark goes on the variable, at the point where it is introduced:

-x = ...     # erased     -- the checker sees it, the compiler deletes it
 x = ...     # affine     -- at most once. the default
+x = ...     # reusable   -- as many times as you like

-x is the one for proofs and type-level arguments: it exists so the checker can reason about something that has no runtime representation at all. You will meet it properly in the laws chapters.

+x is the interesting one, and it does not always work:

import Base
# trying to mark an array as reusable
def main() -> U32:
  +a = [0 : U32*4n]
  b = a[0]
  c = a[1]
  (b + c : U32)

Error:
- expected : Data
- observed : Type
Location: main
4>|   +a = [0 : U32*4n]

Bend is telling you that + is not a permission you grant. It is a property you ask for, and the type has to already have it. An Array does not.

Kinds: the property lives on the type

The types chapter introduced Kind(a) as machinery every parameterised type is forced to carry. This section is what the machinery is for: the kind is where the copy permission lives, and + is how a function asks for it.

Types themselves are sorted into two kinds, and the kind is part of a type’s declaration:

type Array<-T: Type> is Type:      # <- not copyable
type List<a, -A: Kind(a)> is Kind(a)   # <- copyable when A is

Type = Kind(&1)   may be used at most once -- a thing with identity
Data = Kind(&2)   may be copied           -- a thing without identity

So Data is not a different sort of value; it is a type that carries a permission. +x demands Data because you cannot copy a thing that cannot be copied, and that is the whole content of the error message above.

Base declares 22 types. 13 are is Data and exactly 3 are is Type. The other 6 — List, Maybe, Either, Result, Map, Sigma — are parameterised by their own kind, which is the subject of the next section. The three Types are worth reading as a list, because they are not arbitrary:

Array      a block of mutable memory
IO.OP      one IO operation
App        an application window

All three are handles. Copying a block of mutable memory would break the guarantee that in-place rewriting does not need to copy — two names for one block means the rewrite is visible through both, which is precisely what the Type/Data split exists to prevent. Copying an IO operation would forge a resource that was never created.

And List<U32> is Data, because copying a list just copies a structure. So this is accepted:

import Base
def main() -> Nat:
  +xs = {[1, 2, 3] : +List<U32>}
  Nat.add(List.length(&2, U32, xs), List.length(&2, U32, xs))

$ bend t8_listplus.bend
6n

while the same shape without + is refused:

import Base
def main() -> Nat:
  xs = {[1, 2, 3] : List<U32>}
  Nat.add(List.length(&1, U32, xs), List.length(&1, U32, xs))

Error:
- expected : xs
- observed : xs (consumed more than once)

The loose end from the lists chapter

Now the loose end — not how to read the header, which the types chapter covered, but why the kind has to be a parameter at all:

type List<a, -A: Kind(a)> is Kind(a)

A is the list’s own kind, threaded through as a type parameter — so a list’s declaration says whether it may be copied, and List.range returns List<&2, Nat> because the numbers it builds are freely copyable.

It also explains the oddest signature in the standard library, which the lists chapter flagged:

def List.append(a, -A: Kind(a), xs: List<a, A>, ys: List<a, A>) -> List<a, A>

The quantity is the first argument because a list is parameterised by its kind, and a function that takes lists cannot ignore that. You thread it through at the call site:

List.append(&2, Nat, xs, ys)

Bend is not hiding the copy question. It is making you answer it, at every call site, forever.

What + actually costs

It is not free, and the guide says why in the same breath as the no-GC claim:

Since values are affine, a match frees the node it opens on the spot, and only + values carry a reference count.

— bend guide, Under the Hood

So the price of +x is a runtime reference count — a real increment, decrement and check, on every use. When you write +x you are trading the thing that makes Bend fast for the convenience of not restructuring your code. Do it when the restructure is worse, not by default.

Closures, and a restriction that made the language faster

One more type refuses +, and the refusal is the same one:

import Base
# can the closure itself be called twice? t5 again, plus one +
def main() -> U32:
  +f = {x => (x + 1 : U32) : U32 -> U32}
  (f(1) + f(2) : U32)

Error:
- expected : Data
- observed : Type
Location: main
4>|   +f = {x => (x + 1 : U32) : U32 -> U32}

A closure is Type, so it can be called exactly once, and there is no way to mark it otherwise. + does not open this door.

This looks like a real limitation, and for a while it is. Then you find the answer, and the answer is better than the thing it replaced:

import Base

# ~f is a *template* parameter: the argument is substituted at compile time,
# not passed at runtime, so f can be called as many times as you like.
#
# The parameter-side ~ makes f a template. The call-site mark is optional;
# t11_template_implicit.bend shows the same call without it.
def twice(~f: U32 -> U32, x: U32) -> U32:
  f(f(x))

def main() -> U32:
  twice(~(x => (x + 1 : U32)), 40)

$ bend t10_template.bend
42

The checker adds nothing on stderr: a template instance is not disclosed as unsafe. The gate chapter is where the unsafe disclosure gets taken apart.

The ~ on the parameter means template. At the call site the mark is optional: the compiler specializes the argument with or without it. twice is inlined at compile time, and each distinct argument compiles its own copy of the function — so f can be called as many times as the body likes, because at runtime there is no closure there at all. Not a function pointer, not a reference-counted box. Inlined, and free.

Bend’s type system refuses to let you copy a closure. The answer the language arrived at is not “write more code” — it is “inline the function”, which is faster than the version that would have been allowed.

Hold on to that shape. It recurs throughout this book: a restriction that looks like a wall turns out to be the reason the thing is fast.

The files

Next: arrays — where the two kinds collide, and a read hands you back more than you asked for.