Specs

Type parameters are opaque

Normally, you can't do anything with a type parameter t unless it would work for every type.

main void() log all-same 1, 1, 1 all-same[t] bool(a t, b t, c t) # This won't work a == b and b == c

The above example doesn't work even though there is an == function for nats.
all-same can't be defined that way unless == worked for every type (which it doesn't).

This can be fixed by declaring all-same to use the equal spec.

main void() log all-same 1, 1, 1 log all-same 1, 1, 2 all-same[t] bool(a t, b t, c t) t equal a == b and b == c

The above example works because the equal spec predeclares that an == function should exist.
Then the caller of foo is responsible for providing that function.

The caller knows the actual type substituted for t (in this case nat) and looks for a concrete == function.
In this case it looks for == bool(a nat, b nat) and finds it in the standard library.

Specs are written after function parameters.
Multiple specs can be separated by commas as in t data, t equal .
For a multi-line function signature, specs are written after the do keyword.

main void() log all-same 1, 1, 1 log all-same 1, 1, 2 all-same[t] bool a t b t c t do t equal a == b and b == c

Defining specs

A spec declaration has a list of signatures in an indented block.

import keen/math/math main void() log prism-volume (circle 1), 2 log prism-volume (square 1), 7 area[t] spec area float(a t) prism-volume[t] float(a t, depth float) t area depth * area a circle record(radius float) area float(a circle) pi * a.radius ** 2 square record(width float) area float(a square) a.width ** 2

This defines an area spec and uses it to define prism-volume.
That allows that function to call area on the type parameter.

The syntax for spec signatures is the same as for union methods, but there is no implicit first parameter.

Spec inheritance

A spec can inherit from other specs.

import keen/math/math main void() log area-over-perimeter circle 1 log area-over-perimeter square 1 area-over-perimeter[t] float(a t) t shape a.area / a.perimeter shape[t] spec t area perimeter float(a t) area[t] spec area float(a t) circle record(radius float) area float(a circle) pi * a.radius ** 2 perimeter float(a circle) pi * a.radius * 2 square record(width float) area float(a square) a.width ** 2 perimeter float(a square) a.width * 4

In the above example, shape inherits from area, so it includes both area and perimeter signatures.

Special specs

The special spec data doesn't include any signatures. Instead, it is only satisfied for data types. (See Mutability.)
shared is the corresponding spec for shared types.

main void() foo 1 foo ()::nat mut[] # won't work foo[t] void(_ t) t data ()

There are also two special specs global and unsafe that don't have a type argument or any signatures. See Global side effects and Unsafe code.

Auto functions and specs

Even auto functions can use specs.
Below, == needs to use the equal spec so that the (automatic) body can call == on value.

main void() a nat wrapper = value: 1 log a wrapper[t] record(value t) ==[t] bool(a t wrapper, b t wrapper) t equal <=>[t] comparison(a t wrapper, b t wrapper) t compare hash[t] void(a t wrapper, state hash-state) t hash to[t] json(a t wrapper) (json, t) to

Multiple type parameters

Specs can have any number of type parameters. (Even 0 which is useful for avoiding circular imports. See Modules.)
The example above used the to spec, which takes the return type and parameter type of a to function as type parameters.

Methods and specs

Methods (and method implementations) can not declare specs.