23 Traits — one promise kept by many types

23.1 What they are for#

module why .
rem run: demo

trait shape do
  area input s self . output u64 .
end .

struct rect do
  satisfies shape .
  w u64 .
  h u64 .
end .

struct square do
  satisfies shape .
  side u64 .
end .

fn rect.area input s rect . output u64 .
do
  return mul field s. w . field s. h . . .
end .

fn square.area input s square . output u64 .
do
  return mul field s. side . field s. side . . .
end .

fn double_area input comptime t type . input s t . output u64 .
  requires shape t. . .
do
  return mul 2 method s. area. . . .
end .

fn demo output u64 .
do
  let r lit rect do w 2 . h 3 . end . .
  let q lit square do side 4 . end . .
  return add double_area rect. r. . double_area square. q. . . .
end .

$ lowentc --run demo why.low
demo() = 44

• trait shape do … end . is the promise “has area”. self in a signature is the type that will satisfy the promise.
• rect and square write satisfies shape . in their bodies, declaring they will satisfy it.
• fn rect.area and fn square.area actually satisfy it. The rect. in the name means the op is attached to rect.
• double_area accepts any shape. requires shape t. . . pins it down to “only types that can tell their area”.
• method s area calls the area attached to the type of s — rect.area for a rect, square.area for a square.

Think of a trait as a qualification. There is a requirement, “can tell its area”, and only types that meet it may enter an op that asks for it.

                trait shape  ── requirement: area input s self . output u64 .
                   ▲        ▲
       satisfies   │        │   satisfies
     ┌─────────────┴─┐    ┌─┴─────────────┐
     │ rect          │    │ square        │
     │ rect.area     │    │ square.area   │   ← the ops that actually meet it
     └───────────────┘    └───────────────┘

 double_area has requires shape t. . .  ── only types that meet shape
   double_area rect r    →  method s area  =  rect.area
   double_area square q  →  method s area  =  square.area

double_area rect r and double_area square q are each monomorphised to their own instance (chapter 22), so method is resolved at translation, not looked up at run time. There is no virtual function table.

23.2 Ops attached to types, and method#

An op can be attached to a type even without a trait. Put the type name and a dot in front of the op name, and its first input is a value of that type. method <value> <name> <args…> calls that op. The receiver may be the result of another form — method method r. grow. 1 . area. .. If no such op is attached, the call is rejected.

module method_undef .
rem expect: E-METHOD-UNDEF

struct point do
  x u8 .
end .

fn f input p point . output u8 .
do
  return method p. nosuch. . .
end .

$ lowentc --check method_undef.low
method_undef.low:10:0 E-METHOD-UNDEF: no op of that name is associated with the receiver's type — declare it as `fn <type>.<name> input <recv> <type> . …` (RFC-0062)

Calling a name that does not exist does not search upwards. Attached ops are a device for dividing the name space, not inheritance.

23.3 Traits with several ops#

module many .
rem run: demo 3 4
rem trap: demo_empty

trait shape do
  area input s self . output u64 .
  perimeter input s self . output u64 .
  grow input s self . input k u64 . output self .
  checked_area input s self . output u64 . effects panic .
end .

struct rect do
  satisfies shape .
  w u64 .
  h u64 .
end .

fn rect.area input s rect . output u64 .
do
  return mul field s. w . field s. h . . .
end .

fn rect.perimeter input s rect . output u64 .
do
  return mul 2 add field s. w . field s. h . . . .
end .

fn rect.grow input s rect . input k u64 . output rect .
do
  return lit rect do w add field s. w . k. . . h add field s. h . k. . . end . .
end .

proc rect.checked_area input s rect . output u64 . effects panic .
do
  if eq field s. w . 0 . do
    panic "empty rect" .
  end .
  return mul field s. w . field s. h . . .
end .

proc demo input w u64 . input h u64 . output u64 . effects panic .
  requires le w. 1000 . .
  requires le h. 1000 . .
do
  let r lit rect do w w. . h h. . end . .
  let big rect method r. grow. 1 . .
  return add method big. perimeter. . method big. checked_area. . . .
end .

proc demo_empty output u64 . effects panic .
do
  let r lit rect do w 0 . h 5 . end . .
  return method r. checked_area. . .
end .

$ lowentc --run demo many.low 3 4
demo(3, 4) = 38
$ lowentc --run demo_empty many.low
== ir diagnostics (1) ==
0:0 E-VM-PANIC: the program called `panic` — this is an unrecoverable stop, and it is NOT a contract violation (the code chose to stop, it did not break a promise)

There are three things to know about writing them.

• One line per signature. A line starts with the op’s name and then writes clauses in the same order as an op head — inputs, output, effects. The next name starts the next signature. Write as many as you like.
• When the output is self, as in grow, the implementer returns its own type (rect).
• An implementing op is named <type>.<name>.

demo_empty calls checked_area on a rectangle of width 0 and stops. The signature promised effects panic, so callers know it may stop.

23.4 Signatures do not say fn or proc#

Writing fn or proc in a trait signature is rejected.

module sig_kind .
rem expect: E-TRAIT-SIG

trait shape do
  fn area input s self . output u64 .
end .

$ lowentc --check sig_kind.low
5:3 E-TRAIT-SIG: a trait signature does not say `fn` or `proc` — write `area input s self . output u64 .`. Its `effects` line says what the op may do (none = pure), and the implementation chooses `fn` or `proc` (§6.11.2)

What the op may do is decided by the signature’s effects line.

A proc always carries an effects line (chapter 5). One without it is rejected on its own, before any signature is matched — an effect-free signature is implemented by a proc that says effects none ., or by a fn.

module proc_noeff .
rem expect: E-EFFECT-MISSING

trait shape do
  area input s self . output u64 .
end .

struct rect do
  satisfies shape .
  w u64 .
  h u64 .
end .

proc rect.area input s rect . output u64 .
do
  return mul field s. w . field s. h . . .
end .

$ lowentc --check proc_noeff.low
proc_noeff.low:14:0 E-EFFECT-MISSING: a `proc` states its effects — add `effects <atoms> .` (or `effects none .`) to the head. Omitting it used to mean three different things (the checker, `--doc` and the spec disagreed). `lowentc --doc` prints the effects the body actually performs (`inferred:`) — that is the clause to write (RFC-0113 R1)
9:0 E-TRAIT-EFFECT: the implementation is a `proc` with NO `effects` clause, so it may do anything — more than the trait declares. Write the same `effects` line the trait has (or fewer), or make it a `fn` if it is pure

Declaring more effects than the signature is rejected too.

module more_effect .
rem expect: E-TRAIT-EFFECT

trait shape do
  checked_area input s self . output u64 . effects panic .
end .

struct rect do
  satisfies shape .
  w u64 .
  h u64 .
end .

proc rect.checked_area input s rect . output u64 . effects panic wait .
do
  if eq field s. w . 0 . do
    panic "empty rect" .
  end .
  return mul field s. w . field s. h . . .
end .

$ lowentc --check more_effect.low
9:0 E-TRAIT-EFFECT: the implementation has an EFFECT the trait does not declare. A caller reasons against the TRAIT's contract — if the implementation does more, that reasoning is a lie (this is exactly what makes dynamic dispatch safe or unsafe)
more_effect.low:15:1 W-EFFECT-OVER: this op DECLARES `wait` but never PERFORMS it. A declared effect is a cost the caller must budget for (a pure caller cannot call an `io` op). Drop it, or — if a future version will perform it — say so (RFC-0007)

Callers reason against the trait’s contract. If the implementer does something outside that contract, the reasoning goes wrong. A trait whose names match but whose effects differ cannot carry a contract.

23.5 When a trait is not satisfied#

module missing .
rem expect: E-TRAIT-MISSING

trait shape do
  area input s self . output u64 .
  perimeter input s self . output u64 .
end .

struct rect do
  satisfies shape .
  w u64 .
  h u64 .
end .

fn rect.area input s rect . output u64 .
do
  return mul field s. w . field s. h . . .
end .

$ lowentc --check missing.low
10:0 E-TRAIT-MISSING: this type claims to satisfy a trait, but the trait REQUIRES an op that the type does not have. Declare it as `fn <Type>.<name> …` (RFC-0062). A claim that is not checked is the defect this language exists to remove

satisfies is not a comment. The moment you write that you will satisfy a trait, the processor checks the whole list.

23.6 via self — more allocation effects only#

Some promises, like the allocator trait, have allocation effects that differ by implementation. When a signature’s effects line says via self, the implementer may declare more allocation-family effects (alloc, heap, lock, atomic) than the signature. Declaring more of any other effect is still E-TRAIT-EFFECT.

export trait byte_allocator do
  reserve input s self . input n usize . output option mut slice u8 . effects state via self .
  grow input s self . input old mut slice u8 . input newn u64 . output option mut slice u8 . effects state via self .
  used input s self . output u64 . effects state .
end .

A bump allocator’s reserve is just state, while heap_bytes, carving from the heap, has heap state. That difference rises through a generic op’s via a all the way to its callers (chapter 20).

The same device serves promises that are not allocators. Two actors satisfy a ticket-issuing trait: one only counts, the other carves bytes from the fixed window for every ticket.

module viaself .
rem run: main

rem a promise to hand out tickets; an implementation may add allocation-family effects
trait ticketer do
  issue input s self . output u64 . effects state via self .
end .

rem only counts, so its effect is just state
actor counter do
  satisfies ticketer .
  state do
    upcoming u64 .
  end .
  proc issue output u64 . effects state . do
    set upcoming. add upcoming. 1 . .
    return upcoming. .
  end .
end .

rem carves 8 bytes from the fixed window per ticket, so it adds alloc
actor carver do
  satisfies ticketer .
  state do
    root cap allocator .
    count u64 .
  end .
  proc issue output u64 . effects alloc state . do
    let g option mut slice u8 alloc_bytes root. capacity 8 . .
    guard is_some g. . else return 0 . .
    set count. add count. 1 . .
    return mul count. 10 . .
  end .
end .

rem takes any implementation; via t carries that implementation's effects up to here
proc issue_two
  input comptime t type .
  input who t .
  output u64 .
  effects state via t .
  requires ticketer t. . .
do
  let a u64 send who. issue . .
  let b u64 send who. issue . .
  return add a. b. . .
end .

proc main input al cap allocator . output u8 . effects alloc state .
do
  var c counter spawn actor counter . .
  var k carver spawn actor carver . .
  let x u64 issue_two counter. c. . .
  let y u64 issue_two carver. k. . .
  return narrow u8 add x. y. . . .
end .

$ lowentc --run main viaself.low
main() = 33

• The signature is issue input s self . output u64 . effects state via self .. counter satisfies it with effects state . and carver with effects alloc state .. alloc belongs to the allocation family, so via self allows it.
• issue_two says effects state via t .. The instance specialised to counter has the effect state; the one specialised to carver has alloc state. The effects are exact per instance.
• That is why main must receive cap allocator and declare alloc. Without the line that calls with carver, main would need no alloc.
• The answer 33 is counter’s 1 + 2 plus carver’s 10 + 20.

carver’s state has a capability field, root cap allocator .. The rule for that field is covered in chapter 25.

23.7 Common mistakes#

module mistake_methodorder .
rem expect: E-METHOD-UNDEF

struct rect do
  w u64 .
  h u64 .
end .
fn rect.area input s rect . output u64 .
do
  return mul field s. w . field s. h . . .
end .
fn f output u64 .
do
  let r lit rect do w 2 . h 3 . end . .
  rem ✘ after `method` comes the value first, then the name
  return method area. r. . .
end .

$ lowentc --check mistake_methodorder.low
mistake_methodorder.low:16:0 E-METHOD-UNDEF: no op of that name is associated with the receiver's type — declare it as `fn <type>.<name> input <recv> <type> . …` (RFC-0062)

module mistake_noprefix .
rem expect: E-TRAIT-MISSING

trait shape do
  area input s self . output u64 .
end .
struct rect do
  satisfies shape .
  w u64 .
  h u64 .
end .
rem ✘ no `rect.` in the name --- an ordinary op, not attached to the type
fn area input s rect . output u64 .
do
  return mul field s. w . field s. h . . .
end .

$ lowentc --check mistake_noprefix.low
8:0 E-TRAIT-MISSING: this type claims to satisfy a trait, but the trait REQUIRES an op that the type does not have. Declare it as `fn <Type>.<name> …` (RFC-0062). A claim that is not checked is the defect this language exists to remove

module mistake_nosatisfies .
rem expect: E-BOUND-UNSAT

trait shape do
  area input s self . output u64 .
end .
rem ✘ `rect.area` exists, but `satisfies shape .` is not written
struct rect do
  w u64 .
  h u64 .
end .
fn rect.area input s rect . output u64 .
do
  return mul field s. w . field s. h . . .
end .
fn double_area input comptime t type . input s t . output u64 .
  requires shape t. . .
do
  return mul 2 method s. area. . . .
end .
fn f output u64 .
do
  let r lit rect do w 2 . h 3 . end . .
  return double_area rect. r. . .
end .

$ lowentc --check mistake_nosatisfies.low
17:0 E-BOUND-UNSAT: this generic was instantiated with a type that does NOT satisfy the required trait. A bound is a PROMISE the callee relies on — instantiating past it would make the callee's contract a lie (RFC-0021 §6.3). Add `satisfies <trait> .` to the struct, and the required ops as `fn <Type>.<name>`

module mistake_recvlast .
rem expect: E-METHOD-RECV

struct rect do
  w u64 .
  h u64 .
end .
rem ✘ the receiver `s` is not the first input
fn rect.scaled input k u64 . input s rect . output u64 .
  requires le k. 100 . .
do
  return mul k. field s. w . . .
end .
fn f output u64 .
do
  let r lit rect do w 2 . h 3 . end . .
  return method r. scaled. 5 . .
end .

$ lowentc --check mistake_recvlast.low
mistake_recvlast.low:9:0 E-METHOD-RECV: an op attached to a type takes that type as its FIRST input — that is what `method <value> <name> …` passes. Here the receiver is not first, so a `method` call hands the value to the wrong parameter: it used to pass `--check` and stop at run time with `E-VM-TYPE`. Move the receiver to the first `input` clause

module direct_call .
rem run: f

struct rect do
  w u64 .
  h u64 .
end .
fn rect.area input s rect . output u64 .
do
  return mul field s. w . field s. h . . .
end .
fn f output u64 .
do
  let r lit rect do w 2 . h 3 . end . .
  rem the same op called two ways --- directly by name, and through `method`
  return add rect.area r. . method r. area. . . .
end .

$ lowentc --run f direct_call.low
f() = 12

23.8 This chapter’s syntax at a glance#