Mathematical reasoning of API design

[bvssvni]

In Rust you can use mathematics to help reason about API design. In code, there is no distinction between self as a function, as a variable or as a parameter to its method. By translation into mathematical functions, it might become easier to discover issues. It can also be used to transform the API into another equivalent form and play around with the concepts.

For example, in mathematics the function f(t) usually means a function of time. It does not tell what f is or how you compute f, but it is clear that f means something more specific than t. It would be awkward to write t(f) because we think of time as something generic and independent. Neither it does tell what f(t) returns, but if it returned an image, we could write f(t) -> img.

Pure functions in the mathematical sense can be used to reason about dependencies. When you have f(x) and g(f), then g does not depend on x. Example: animation(time) -> image and frames(animation) -> uint. frames is independent of time.

When you write g(f(t)) you can also write g(f, t) which means you also can couple and decouple dependencies. You can also substitute for f(t) -> h and do g(h). Now you have a new type! Decoupling means you get fewer types, but more parameters. There is a tradeoff you have to make, both in how types, functions and parameters work.

• g(f, t) vs g(f(t))
• f(t) -> g vs f(t) -> g1, f(t) -> g2
  • You can have one complex structure with multiple aspects
  • You can have multiple structures describing different aspects
• What is the role of the self type? A function or a variable?
  • A function is often immutable
  • A variable is often mutated or replaces some other variable of same name
• f(t) -> a could mean a is a method name, or a new type
  • This form can be used when the method name is unknown, as when calling g(f(t))
  • Types and method names can be interchanged

Some examples:

window.title() -> String becomes title(window) -> String. You might consider info(window) -> WindowInfo and title(info(window)) -> String. Perhaps title(info)(window) and title(info) -> TitleInfo? Should title be a type?

It might help solve some problems where you are stuck in the design process and need a way to "sketch up" new ideas.

Semantics

The -> operator can be thought of as having two sides, one before and one after. When a name appears on the left side but not on the right side, it is assumed to be immutable. When a name appears on the right side with a ', for example x', it is assumed to be transformed. All objects are functions, and all functions are objects. This means all objects are intended to have a "default" purpose, which can be defined as a function. It is not a strict semantics, but gives a rough idea of how different names/functions relates to each other.

For example:

f(x) -> x'

This means x is transformed by f into a new version x'. f might still exist after the transformation, but we don't write it, both to make it shorter and to make it easier to switch to programming thinking. If we do, we write it like this:

f(x) -> f, x'

The arrow does not have mean "returns", it can be side effects of the function. Usually we are interested in the side effects, compositions, and whether one thing needs to depend on another thing.

[bvssvni]

Associated functions

An extension for something I call "associated functions":

Examples:

• add(f32, f32) -> f32 and is_zero(f32) -> bool gives add [is_zero] (bool, bool) -> bool which tells how addition transforms the knowledge of whether a number is zero, and since adding two zeroes equals zero we can say add [is_zero] (true, true) = true
• An iterated solver object has the function solver(problem) -> problem' and heuristic(problem) -> difficulty gives solver [heuristic] (difficulty) -> difficulty' which tells how heuristic difficulty changes when a solver function iterates on a problem (hopefully decreasing).

A associated functions can be used to prove things about compositions or test for combination errors. It seems repeated associated functions are communative and can be written f [g] [h] (x) or f [h] [g] (x). An asymmetric form f [g, h] (x, y) -> [i] z can be used but is often "less natural".

Very often you have to figure out the values and it is possible to make mistakes, but once you have written down something it becomes easier to puzzle the picture together.

Symmetry rule

1. A function operating on a single type, for example f(x, x) -> x
2. A lift function g(x) -> y
3. There exists possibly an associated function f [g] (y, y) -> y that operates on the lifted value but with similar semantics. If we have f(x1, x2) then f [g] (g(x1), g(x2)) = g(f(x1, x2)).

Semantics

The earlier idea that we built on is that all functions are objects and all objects are functions. With associated functions you can make a new analogy: All functions or objects are paths through a space.

• Paths that can be combined to take you to a new place
• Paths can be combined to create a new path
• There can be several paths from A (input) to B (output)

Earlier the semantics of -> was to show side effects, but with associated functions the return value must be explicit or else there is no way to know what the arguments get lifted to.

[bvssvni]

Sets and values of types

A set is an object which contains other objects where each object occur exactly once. For example, if a contains a1 and a2 we can write:

a = { a1, a2 }

When reasoning about types, there is no need to distinguish between types and values because every value can be a set and therefore values can emulate types and types can emulate values. It is only when writing the Rust code you have to choose whether to interpret something as a value or a type.

For example:

bool = { true, false }

A set has an associated function : that works for every member of the sets, but only for inputs. For example, the and(bool, bool) -> bool has the following associated functions:

and [:] (false, false) -> false
and [:] (true, false) -> false
and [:] (false, true) -> false
and [:] (true, true) -> true

You can choose to omit [:] in obvious cases. This also has the side effect that values and types can be expressed with the same notation. For example add [is_zero] (true, true) -> true.

The relationship between types and values and the idea of sets can be derived from a kind of asymmetry that appears to be symmetric:

and(bool, bool) -> bool
true(bool) -> true
false(bool) -> false
and [true, false] (true, false) -> [false] false
and [:] (true, false) -> false

It is possible to express all properties of everything without adding specific notations, but some ideas are nice to express in shorter form because they are more useful.

[bvssvni]

niconii made an interesting twist http://puu.sh/hda0w/d54b90ff5a.txt

[bvssvni]

Generics

Generics can be thought of a function that returns a set:

option(x) = { none, some(x) }

none(option(x)) -> none
some(x)(option(x)) -> some(x)

[bvssvni]

Temporal logic

The syntax can be extended using a parameter of time X(t). If no parameter is given then it is assumed to be equal for all X in that expression.

Example:

foo increases it's value over time, independently on how other functions interact with X:

foo([:] X(t + 1)) > foo([:] X(t))

Temporal constraints can help solving problems by finding an algorithm which reaches a state where the constraints no longer changes. When parts of the constraints no longer changes conditioned on some acquired knowledge, this knowledge can then be computed to reduce the problem.