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 rect be make rect do w 2 . h 3 . end .
  let q square be make 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 make 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 rect be make rect do w w . h h . end .
  let big rect be method r grow 1 .
  return add (method big perimeter) (method big checked_area) .
end

proc demo_empty output u64 . effects panic .
do
  let r rect be make 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 without an effects line is not narrowed and reads as able to do anything (chapter 5). So implementing an effect-free signature with such a proc is rejected.

module proc_noeff .
rem expect: E-TRAIT-EFFECT

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
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 u64 . 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
    next u64 .
  end
  proc issue output u64 . effects state . do
    set next (add next 1) .
    return next .
  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 . . be 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 be send who issue .
  let b u64 be send who issue .
  return add a b .
end

proc main input al cap allocator . output u8 . effects alloc state .
do
  var c counter be spawn actor counter .
  var k carver be spawn actor carver .
  let x u64 be issue_two counter c .
  let y u64 be 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 rect be make 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 rect be make 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 rect be make 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 rect be make 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#