Specs

Basic specs

Function templates will only let you call functions known to exist. Foe xample, you can't call + if it's not guaranteed to exist for all types the template is instantiated with.
The solution is to predeclare the function. That's what specs do.

main void() info log "{(1, 2)::nat[] sum}" info log "{(1.5, 3.6)::float[] sum}" summable[t] spec new t() + t(a t, b t) sum[t] t(a t[]) t summable res mut t = () for x : a res +:= x res

A function's specs are written after its parameter list. If there are multiple, separate them by commas, as in t summable, t equal.
The syntax for instantiating a spec template is just like for a type template. t summable instantiates summable using t. (The type parameter to sum happens to have the same name as the type parameter to summable.)

Since sum depends on summable, the functions declared inside summable are in scope inside of sum.
So, the call to () in res mut t = () calls new t(), and res +:= x calls + t(a t, b t).

When sum is called by main, type arguments are inferred first, then the spec is implemented using functions from the caller's context.
So in (1, 2)::nat[] sum, Crow first determines that it's calling sum@nat. Then it tries to implement nat summable.
To do that, it looks for functions new nat() and + nat(a nat, b nat). After finding those, it implements the spec to fully instantiate the template.

Specs avoid circular dependencies

In this example, ping.crow avoids a direct dependency on pong.crow. Instead, it uses a spec to declare the dependency.
The call can then be resolved in pong.crow which has access to both functions.

# ping.crow pong spec pong void(a nat) ping void(a nat) pong info log "ping {a}" if a != 0 a - 1 pong # pong.crow import ./ping pong void(a nat) info log "pong {a}" if a != 0 a - 1 ping main void() 10 ping

Spec inheritance

For convenience, you can write other specs on the first line of a spec declaration. You can even omit the spec body if all you need is to combine other specs.
So the first example could be written as:

main void() info log "{(1, 2)::nat[] sum}" info log "{(1.5, 3.6)::float[] sum}" add[t] spec + t(a t, b t) summable[t] spec t new, t add sum[t] t(a t[]) t summable res mut t = () for x : a res +:= x res

Special specs

There are special specs data and shared that aren't implemented by functions.
Instead, these specs are only satisfied when their type argument is a data or shared type, respectively.
For example, this is how functions on map types enforce that the key is data.

main void() info log "{(1, 2, 3)::nat[] count-unique}" # Compile error info log "{()::string-builder[] count-unique}" count-unique[t] nat(a t[]) t key a.to::(t set) size

Notice how to satisfy the spec needed by to::(t set), count just defers to its own caller by declaring the same spec itself.