The method catalog

Every method in Praxis is a row in one table. There are 149 of them, they live in crates/praxis-stdlib/src/builtins.rs, and there is no way to add a 150th from a program: the language has no impl, no traits, no extension methods, and a record carries fields but no methods. This chapter is that table.

The closedness is load-bearing rather than a limitation the compiler tolerates. Because the catalog is the complete method universe, a name it does not carry at that arity can never resolve against any receiver — so fn f(x) { x.nope() } is refused at check time, before anything has said what x is.

How to read these tables

Method is the row’s name and the type pattern of each parameter; Result is its result pattern. Both are rendered the way the compiler prints a type: T, U, K, V and Acc are type variables, two occurrences of one name in a row are the same type, (Int, Int) is a tuple, and (T) -> Bool is a closure parameter. A nullary collection prints bare, so it is BitSet and not BitSet[].

Mutates is the row’s purity flag. The impure rows are exactly the ones that change the receiver, and the flag is visible from a program: the crash debugger’s p expression evaluator refuses a call to an impure method, because a debugger that mutates a faulted state cannot resume it.

var v = [1, 2, 3]
out(v[9])

That faults, and the debugger it drops into will evaluate one of these two calls and not the other:

error: program faulted: index out of bounds

Backtrace:
#0   <entry>

  locals:
    v: Vec[Int] = [1, 2, 3]
  temps:
    <tmp#1: Vec[Int]> @ "[1, 2, 3]" = [1, 2, 3]
    <tmp#2: Int> @ "1" = 1
    <tmp#3: Unit> = Unit
    <tmp#4: Int> @ "2" = 2
    <tmp#5: Unit> = Unit
    <tmp#6: Int> @ "3" = 3
    <tmp#7: Unit> = Unit
    <tmp#9: Int> @ "9" = 9
    <tmp#10: Int> @ "v[9]" = <uninit>
    <tmp#11: Unit> @ "out(v[9])" = <uninit>
Entered crash debugger. 1 frame(s). Type `help` for commands.
Praxis crash> p v.len()
3
Praxis crash> p v.push(4)
error: method `push` is impure (may mutate state) — `p` rejects mutating expressions
Praxis crash> quit

Faults is whether the call can raise a runtime fault. For a row backed by a runtime wrapper this is the wrapper’s own declaration in the ABI manifest, which is what puts a fault check after the call — so “yes” means the check is emitted, not that you are likely to trigger it. Vec.push says yes for a type-mismatch case a well-typed program cannot reach; Vec.get says yes because indexing off the end is the everyday one.

Allocates is whether the call may allocate, and therefore whether its call site is a garbage-collection safepoint. It is derived from the same manifest row, which is why len() says yes on every collection: the count comes back as a freshly boxed Int.

Neither flag is restated per method — both are read off the wrapper the row lowers to, so a row cannot disagree with the code it calls. Thirty-one of the thirty-five pipeline rows have no wrapper to read: the compiler fuses them into the loop, so their tables below carry no Allocates column and their Faults column is what the fused code does rather than a manifest row.

Sequence collections

Vec[T]

var v = [10, 20, 30]

out(v.len())
out(v.is_empty())
out(v.get(1))

v.push(40)
out(v)

3
false
20
[10, 20, 30, 40]

push is the only way a vector grows. v[v.len()] = x is an IndexOutOfBounds fault and not an append.

Deque[T]

var d = Deque()
d.push_back(2)
d.push_back(3)
d.push_front(1)

out(d)
out(d.len())
out(d.get(0))
out(d.pop_front())
out(d.pop_back())
out(d.is_empty())

[1, 2, 3]
3
1
1
3
false

Index 0 is the front, whichever end you have been pushing to.

Keyed collections

Map[K, V]

var m = Map()
m.insert("a", 1)
m.insert("b", 2)

out(m.len())
out(m.contains("a"))
out(m.get("a"))
out(m.get("z"))
out(m.keys())
out(m.values())

m.remove("a")
out(m)
out(m.is_empty())

2
true
Some(1)
None
[a, b]
[1, 2]
{b: 2}
false

get answers an Option; m[key] faults on a missing key. Those are the two halves of one question and the spelling picks which you meant.

keys() and values() answer Vecs in a fixed, deterministic order — by the key’s own order, the same one sorted() uses, so an Int key comes out numeric — and the two are index-aligned, so keys()[i] and values()[i] belong together. To get both at once, walk the map: for kv in m and the pipeline rows below both yield (K, V) pairs, and m.to_vec() is the Vec[(K, V)].

Set[T]

var s = Set()
s.insert(1)
s.insert(1)
s.insert(2)

out(s.len())
out(s.contains(2))

s.remove(2)
out(s)
out(s.is_empty())

2
true
{1}
false

Counter[T]

var c = Counter()
c.inc("x")
c.inc("x")
c.inc("y")

out(c.get("x"))
out(c.get("never seen"))
out(c.len())
out(c.keys())
out(c.values())
out(c.is_empty())

2
0
2
[x, y]
[2, 1]
false

A Counter is the collection whose absent values read as zero, so get and c[key] never fault and len() counts the keys that were actually touched.

Priority queues and bit sets

MinHeap[T]

MaxHeap[T]

var lo = MinHeap()
lo.push(5)
lo.push(1)
lo.push(3)

out(lo.len())
out(lo.peek())
out(lo.pop())
out(lo.is_empty())

var hi = MaxHeap()
hi.push(5)
hi.push(1)

out(hi.peek())
out(hi.pop())

3
1
1
false
5
5

peek is pure and pop is not, which is the only difference between them in this table and the whole difference at the call site.

BitSet

var b = BitSet()
b.insert(3)
b.insert(70)

out(b.contains(3))
out(b.contains(4))
out(b.len())

b.remove(3)
out(b)
out(b.is_empty())

true
false
2
{70}
false

insert faults on a negative or oversized member; remove does not, because clearing a bit that was never in range is not a question the set has to answer. contains is the one row in the catalog that lowers to a dedicated scalar-producing instruction rather than a call, which is why it is not a safepoint.

Grid[T]

A grid is indexed (x, y) with x the column and y the row, and positions(), cells() and find_all() walk it in row-major order.

Around4 and Around8 are the catalog’s only named result types, and they are records, not collections: read the field with a dot, a.up, and every one of them is an Option[(Int, Int)]. Around4 is the plus with the centre skipped; Around8 is the whole 3×3 block in reading order, again without the centre. Neither has a constructor — a grid is the only thing that makes one — and the order the rows above list the fields in is the order the runtime lays the value out in, which is why it is written that way and not alphabetically.

var g = read grid(one_of(".#"))
var wall = '#'

out(g.width())
out(g.height())
out(g.get(1, 0))
out(g.contains(3, 0))
out(g.row(0))
out(g.column(1))
out(g.cells())
out(g.positions().len())
out(g.neighbors4((1, 1)))
out(g.neighbors8((0, 0)))
out(g.around4((1, 1)))
out(g.around8((0, 0)))
out(g.around4((1, 1)).right)
out(g.count4((1, 1), wall))
out(g.count8((1, 1), wall))
out(g.count4_where((1, 1), |c| c != wall))
out(g.count8_where((1, 1), |c| c != wall))
out(g.find(wall))
out(g.find_all(wall))
out(g.transpose().row(0))
out(g.rotate_left().row(0))
out(g.rotate_right().row(0))

g.set(0, 0, wall)
out(g.row(0))

with input

.#.
..#

3
2
#
false
[., #, .]
[#, .]
[., #, ., ., ., #]
6
[(1, 0), (0, 1), (2, 1)]
[(1, 0), (0, 1), (1, 1)]
{ up: Some((1, 0)), left: Some((0, 1)), right: Some((2, 1)), down: None }
{ up_left: None, up: None, up_right: None, left: None, right: Some((1, 0)), down_left: None, down: Some((0, 1)), down_right: Some((1, 1)) }
Some((2, 1))
2
2
1
3
Some((1, 0))
[(1, 0), (2, 1)]
[., .]
[., #]
[., .]
[#, #, .]

neighbors4 and neighbors8 return only the in-bounds neighbours, so they are already the neighbour function a graph walk wants: bfs(start, |p| g.neighbors4(p)) type-checks because the walk’s neighbours closure is (T) -> Vec[T].

around4 and around8 are not those rows spelled differently. A clipped Vec cannot say which direction each neighbour was, and at the edge of the grid it cannot say there was a direction at all — (1, 1) above has three orthogonal neighbours and the Vec has three entries, with nothing to mark the missing down. Every field of an Around4 is an Option, so both survive, at the cost of no longer being a Vec a walk can consume. Take the Vec for a search and the record when the direction is the answer.

count4 and count8 compare each in-bounds neighbouring cell to a value, where neighbors4 and neighbors8 answer positions; count4_where and count8_where take a predicate on the cell instead. A neighbour off the grid has no cell, so it is never counted and the closure never sees one — which is why the _where pair is the only Grid row besides column, get, row and set that can fault, and it faults for the predicate’s reasons rather than for any of its own.

transpose, rotate_left and rotate_right answer copies and leave the receiver alone.

A Grid is deliberately not a pipeline receiver. for cell in g walks it in row-major order, but g.map(f) is a Y110: a grid enters a pipeline through cells() or positions(), which already answer Vecs. A grid’s shape is part of its value, and a stage that flattened it would be answering about something else.

The pipeline

Thirty-five rows — thirty-four names, because count has two arities — sit on one generic receiver that stands for ten different receivers: Vec, Deque, Set, MinHeap, MaxHeap, Range, BitSet, Map, Counter and Text. That is the for loop’s list minus Grid, and what a receiver yields here is exactly what the for loop’s variable would bind — a Char from a Text, a (K, V) pair from a Map or a Counter, an element from everything else.

var s = Set()
s.insert(2)
s.insert(1)
out(s.sorted())

var m = Map()
m.insert("a", 1)
m.insert("b", 2)
out(m.map(|pair| pair.0))
out(m.to_vec())

var c = Counter()
c.inc("x")
out(c.to_vec())

var d = Deque()
d.push_back(7)
out(d.sum())

var lo = MinHeap()
lo.push(2)
lo.push(1)
out(lo.to_vec())

var b = BitSet()
b.insert(4)
b.insert(9)
out(b.sum())

out((0..5).sum())
out((0..=5).sum())
out("abc".map(|ch| ch.to_int()))

[1, 2]
[a, b]
[(a, 1), (b, 2)]
[(x, 1)]
7
[1, 2]
13
10
15
[97, 98, 99]

A pipeline’s currency is Vec. Every stage answers one whatever the receiver was, which is what makes “what does filter return” answerable without knowing what you started from. A program that wants a different collection back says which one, with a to_* row.

The Requires column below is the row’s own constraint on the item type. Its wording is the compiler’s: an unorderable element gets Y006 values of type ... cannot be ordered, and one that cannot be a key gets Y014 a value of type ... can change after it is stored.

Stages

sorted, sorted_by_key, unique, reversed, frequencies and join are barriers: each needs the whole sequence before it can answer anything, so each is a call into the runtime rather than a stage the compiler folds into the loop. reversed is the clearest case of the definition — it cannot answer its first element until it has seen the last. Being a barrier is invisible from a program except in what it costs — the other stages are fused into a single pass over the source, which is also what the “Faults” column is measuring here: a fused stage has no wrapper of its own to fault, while sorted and sorted_by_key do — and sorted_by_key‘s also propagates whatever the key closure raised. reversed is the barrier that does not fault, and the two facts are the same fact: it reads no descriptor callback, which is also why its Requires column is empty where its neighbours’ are not.

join is in the sinks table below rather than here, because it answers a Text rather than a sequence.

Sinks

count is the one name in the catalog that carries two arities on a single receiver — count() is the element count, count(pred) the matching-element count — which the table’s (receiver, name, arity) key has always allowed. (get, contains and [] also appear at two arities, but split across receivers: one argument on a Vec, two on a Grid.)

min/max are Int sinks and min_by/max_by take a “less-than” comparator and work on anything. find answers the element, position the index, and both answer an Option.

The seven faulting sinks fault for two reasons and no others. min, max, min_by, max_by and reduce raise empty collection on an empty sequence: each has to answer with an element and there is none. sum and product raise integer overflow, because the running total is checked arithmetic like every other + and *. fold is the sink that does not fault on an empty sequence — it answers its seed — which is the reason to reach for it over reduce.

var v: Vec[Int] = Vec()
out(v.min())

error: program faulted: empty collection

Backtrace:
#0   <entry>

  locals:
    v: Vec[Int] = []
  temps:
    <tmp#1: Vec[Int]> = []
    <tmp#3: Int> = 0
    <tmp#4: Int> = 0
    <tmp#8: Unit> @ "out(v.min())" = <uninit>

Conversions

There is a conversion for every collection that has a constructor, and exactly one that has none: to_grid does not exist, because a grid needs a width and a flat item sequence does not carry one.

to_map and to_counter say “my item is a pair” in the receiver pattern rather than in prose, so [1, 2].to_map() fails at the method name with expected (?T, ?U), found Int instead of resolving and then faulting.

The whole pipeline, run

var v = [3, 1, 4, 1, 5]

out(v.map(|n| n * 2))
out(v.filter(|n| n > 2))
out(v.filter_map(|n| if n > 3 { Some(n) } else { None }))
out(v.flat_map(|n| [n, n]))
out(v.take(2))
out(v.skip(3))
out(v.take_while(|n| n < 4))
out(v.enumerate())
out(v.zip(["a", "b"]))

out(v.fold(0, |acc, n| acc + n))
out(v.reduce(|acc, n| acc + n))
out(v.sum())
out(v.product())
out(v.count())
out(v.count(|n| n == 1))
out(v.min())
out(v.max())
out(v.min_by(|a, b| a < b))
out(v.max_by(|a, b| a < b))
out(v.any(|n| n == 4))
out(v.all(|n| n > 0))
out(v.find(|n| n > 3))
out(v.position(|n| n > 3))

out(v.sorted())
out(v.sorted_by_key(|n| 0 - n))
out(v.unique())
out(v.reversed())
out(v.frequencies())
out(["a", "b", "c"].join(", "))

out(v.to_vec())
out(v.to_set())
out(v.to_deque())
out(v.to_min_heap().peek())
out(v.to_max_heap().peek())
out(v.to_bitset())
out([(1, "a"), (2, "b")].to_map())
out([("x", 3)].to_counter())

[6, 2, 8, 2, 10]
[3, 4, 5]
[4, 5]
[3, 3, 1, 1, 4, 4, 1, 1, 5, 5]
[3, 1]
[1, 5]
[3, 1]
[(0, 3), (1, 1), (2, 4), (3, 1), (4, 5)]
[(3, a), (1, b)]
14
14
14
60
5
2
1
5
1
5
true
true
Some(4)
Some(2)
[1, 1, 3, 4, 5]
[5, 4, 3, 1, 1]
[3, 1, 4, 5]
[5, 1, 4, 1, 3]
{1: 2, 3: 1, 4: 1, 5: 1}
a, b, c
[3, 1, 4, 1, 5]
{1, 3, 4, 5}
[3, 1, 4, 1, 5]
1
5
{1, 3, 4, 5}
{1: a, 2: b}
{x: 3}

What the Requires column refuses

A tuple can be a key but cannot be ordered — no composite in this language can, because ordering goes through one scalar comparison. That is a statement about < and sorted(), not about a container: a Map[(Int, Int), V] still walks and prints its keys element-wise, because it has to walk them in some reproducible order. A record behaves exactly the same way: a fine key, not orderable. A Vec is neither one nor the other: not orderable, for the same composite reason, and not a key, because it can change after it has been stored. Below, the tuple fails the first column and the Vec fails the second.

var pairs = [(2, "b"), (1, "a")]
out(pairs.sorted())

var groups = [[1], [2]]
out(groups.to_set())

$ praxis check catalog-bounds.px
error[Y006]: values of type `(Int, Text)` cannot be ordered

  catalog-bounds.px:2:11
  2 | out(pairs.sorted())
    |           ^^^^^^ values of type `(Int, Text)` cannot be ordered

error[Y014]: a value of type `Vec[Int]` can change after it is stored, so it cannot be used as a key

  catalog-bounds.px:5:12
  5 | out(groups.to_set())
    |            ^^^^^^ a value of type `Vec[Int]` can change after it is stored, so it cannot be used as a key

help: use a value that cannot change — a number, `Text`, or a tuple of those

praxis: 2 error(s)

sorted_by_key is the answer to the first half: the ordering requirement moves to the key the closure extracts, so the elements themselves need not be orderable.

var pairs = [(2, "b"), (1, "a")]
out(pairs.sorted_by_key(|pair| pair.0))

[(1, a), (2, b)]

Scalars

Text is the one scalar with members, and Int, Float and Char have the conversions and the explicit-overflow family.

Text

var line = "héllo"

out(line.len())
out(line.is_empty())
out(line.get(1))
out(line.get(1).to_int())
out((233).to_char())
out(" 42 ".int())
out("héllo".int())
out("1.5".float())
out("inf".float())

5
false
é
233
é
Some(42)
None
Some(1.5)
None

len() counts Unicode scalar values and get/t[i] index by them, not by bytes — which is why "héllo".len() is 5 and line.get(1) is é. Char.to_int and Int.to_char are the round trip out of and back into a character, and they are Int and Char rows rather than Text ones.

int() and float() trim the text and then read exactly what the input parser’s int and float atomics read, over the whole of what is left. They share the parser’s own scanner, so t.int() and parse(t, int) cannot disagree about what a number is. Anything the run does not cover is None — "1 2", "12abc", "1." — because a text that is not a number is absence rather than a fault.

Two answers surprise people, and both follow from that rule:

• "+5".int() is None. The int atomic takes a leading - and not a +. "+5.0".float() is a value, because the float atomic does take one.
• "inf".float() and "nan".float() are None. Float has those values — 1.0 / 0.0 is one, and to_text() prints them — but no text spells one.

A value past Int’s range is None too. The input parser is the other way to get a number out of text, and the one to reach for when the text came from input in the first place: it reports where the parse broke instead of answering None.

There is no split, no chars and no to_upper: all three are Y110. for ch in text is how a Text is walked, and the pipeline rows above apply to it directly.

Int

Float

Char

All three receivers at once:

var x = -2.5

out(x.abs())
out(x.sign())
out(x.floor())
out(x.ceil())
out(x.round())
out(x.to_int())
out(x.to_text())
out(x.min(1.0))
out(x.max(1.0))
out((2.0).sqrt())
out((0.0 / 0.0).is_nan())
out((1.0 / 0.0).is_infinite())

out((7).to_float())
out((9223372036854775807).wrapping_add(1))
out((9223372036854775807).saturating_add(1))
out((9223372036854775807).checked_add(1))
out((5).checked_sub(1))
out((3).wrapping_mul(4))
out((1660).to_text())
out('A'.to_text())

2.5
-1.0
-3.0
-2.0
-3.0
-2
-2.5
-2.5
1.0
1.4142135623730951
true
true
7.0
-9223372036854775808
9223372036854775807
None
Some(4)
12
1660
A

Integer arithmetic is checked by default, and the nine wrapping_/saturating_ /checked_ rows are how a program opts out of the fault for one operation.

The to_text family is Int, Float and Char, and it is closed at three: Bool has no row and there is no universal T.to_text(). Each of the three answers exactly the characters out writes — the method and the printer share one renderer per scalar, so they cannot drift apart. A labelled line does not need any of them: "n = {n}" renders a value of any type through the same printer.

Subscripts

m[key], v[i] = x and grid[x, y] are catalog rows too, dispatched on the receiver’s shape and the index count exactly as a method call is. Their names — [], []=, []min=, []max= — are not identifiers, so no program can call them by name; the subscript grammar is their only caller.

Six receivers read. Five of the six also store: every one but Text, which is immutable.

var v = [10, 20, 30]
v[0] = 11
out(v[0])

var d = Deque()
d.push_back("a")
d[0] = "b"
out(d[0])

out("praxis"[2])

var m = Map()
m["k"] = 1
out(m["k"])

var c = Counter()
c["x"] = 4
out(c["x"])
out(c["never seen"])

var best = Map()
best["r"] min= 5
best["r"] min= 3
best["r"] max= 4
out(best)

11
b
a
1
4
0
{r: 4}

min= and max= exist as their own rows rather than as read-modify-write over the other two, because they give an absent entry a meaning no read can express: the first value is accepted as-is. A subscript read of an absent Map key faults, so there would be nothing to compare against.

var m = Map()
m.insert("a", 1)
out(m["b"])

error: program faulted: index out of bounds

Backtrace:
#0   <entry>

  locals:
    m: Map[Text, Int] = {"a": 1}
  temps:
    <tmp#1: Map[Text, Int]> = {"a": 1}
    <tmp#3: Text> @ ""a"" = "a"
    <tmp#4: Int> @ "1" = 1
    <tmp#5: Unit> @ "m.insert("a", 1)" = Unit
    <tmp#6: Text> @ ""b"" = "b"
    <tmp#7: Int> @ "m["b"]" = <uninit>
    <tmp#8: Unit> @ "out(m["b"])" = <uninit>

When a method does not resolve

Two diagnostics cover almost everything. Y110 is “this table has no such row” — including the wrong argument count, since arity is part of the key, so [1, 2].get() is no method 'get' on type 'Vec[Int]' taking 0 argument(s). Y001 is “the row exists and your types do not fit it”, which is what the item shapes produce; the two requirement columns above produce Y006 and Y014 instead.

out("a,b".split(","))
out([1.5, 2.5].sum())
out([1, 2].to_map())
out(['a'].join(""))
out([1, 2].to_text())

$ praxis check catalog-refusals.px
error[Y110]: no method `split` on type `Text` taking 1 argument(s)

  catalog-refusals.px:1:11
  1 | out("a,b".split(","))
    |           ^^^^^ no method `split` on type `Text` taking 1 argument(s)

error[Y001]: expected Int, found Float

  catalog-refusals.px:2:16
  2 | out([1.5, 2.5].sum())
    |                ^^^ expected Int, found Float

error[Y001]: expected (?T, ?U), found Int

  catalog-refusals.px:3:12
  3 | out([1, 2].to_map())
    |            ^^^^^^ expected (?T, ?U), found Int

error[Y001]: expected Text, found Char

  catalog-refusals.px:4:11
  4 | out(['a'].join(""))
    |           ^^^^ expected Text, found Char

error[Y001]: expected Char, found Int

  catalog-refusals.px:5:12
  5 | out([1, 2].to_text())
    |            ^^^^^^^ expected Char, found Int

praxis: 5 error(s)

The second is why sum is spelled as a bound rather than a literal Vec[Int] receiver: the row still matches a Vec[Float], so the report is about the element type you have rather than “no method sum on this type”. The last two are the same shape, and the same reason join and to_text bound their item rather than naming a concrete receiver.

See method resolution for how a call finds its row, and diagnostic codes for the full list.