[pron]

That depends what it is that you want to specify: a function or a computation (i.e., a machine). In TLA+ as in "reality" computations are not functions, and functions are not computations.

We'll start with a function. It's basically `[a -> [a -> a]]` or `[a × a -> a]`. More completely (to show that `a` is abstract):

    CONSTANT a, f
    ASSUME f ∈ [a -> [a -> a]]

`CONSTANT` means that a can be anything (formally, any set)

If you want to specify a computation, that, when terminates[1] returns a result in `a`, the "type" would be `[](done => result ∈ a)` (where [] stands for the box operator, signifying "always"), or more fully:

    CONSTANT a, Input
    ASSUME Input ∈ a × a
    VARIABLES done, result
    f ≜ ... \* the specification of the computation
    THEOREM f => [](done => result ∈ a)

So the first type is purely static. A set membership. The second has a modality, which says that whenever (i.e., at any step) `done` is true, then `result` must be in `a`.

------

[1]: Let's say that we define termination as setting the variable `done` to TRUE. BTW, in TLA as in other similar formalisms, a terminating computation is a special case of a non-terminating one, one that at some finite time stutters forever, i.e., doesn't change state, or, formally <>[](x' = x), or the sugared <>[](UNCHANGED x) namely eventually x is always the same (<> stands for diamond and [] for box; for some reason HN doesn't display those characters)

[tome]

Actually, I've thought of something that will be an even better example. You mentioned "reduce" here

https://news.ycombinator.com/item?id=11910858

Could you link to its implementation?

[pron]

I'll quote my own:

    Reduce(Op(_, _), x, seq) ==
        LET RECURSIVE Helper(_, _)
        Helper(i, y) ==
            IF i > Len(seq) THEN y
                            ELSE Helper(i + 1, Op(y, seq[i]))
        IN Helper(1, x)

A couple of things. First, the need for the helper is just a limitation of the language that doesn't allow recursive operators to take operators as arguments. Second, I used indexing, but you can use the Head and Tail operators. It's just that I use this often, and I care about the model-checking performance. Finally, Reduce is an operator not a function (it is not a function in the theory). Hence, its domain (for all arguments that aren't operators) is "all sets" something that would be illegal as a "proper" function (Russel's paradox). Operators, like functions, can be higher order, but they're not "first-class", i.e., they can't be considered "data". Functions require a proper domain (a set).

[tome]

> I'll quote my own: ...

Thanks

> Operators, like functions, can be higher order, but they're not "first-class", i.e., they can't be considered "data".

Do you mean you can't pass an operator to a function (or make it the argument of a computation)?

EDIT: Or more generally, what are the consequences of it not being "first-class", i.e., not being considered "data"?

[pron]

> Do you mean you can't pass an operator to a function

Right. Functions are objects in the theory, and must have a domain which is a set. Operators are outside the theory, and aren't in any sets. You also can't return an operator as a result of an operator.

A function can, of course, return a function, but functions can't be polymorphic within a single specification. So they must have a particular (though perhaps unspecified) set as their domain. Why? Because there is no such thing as polymorphic functions in math. Polymorphism is a feature of a certain language or "calculus", and TLA+ is about algorithms, not about a specific linguistic representation of them. "Polymorphism" of the kind I've shown does make sense, because you determine the level of the specification, and you can say that you want to reason about the use of a function (or a computation) without assuming anything more specific other than your explicit assumptions about a certain set. But that is not to say that you can’t have an operator that “creates” functions generically. E.g.:

    Foo(a) ≜ [x ∈ a × a ↦ x[1]]   /or/  Foo(a) ≜ LET f[x ∈ a × a] ≜ x[1] IN f

Which you can then use like so: Foo(Nat)[1, 2]. Foo must be an operator because its argument `a` ranges over all sets, so it's not a proper domain (Russel, etc.)

> or make it the argument of a computation

Ah, that actually you can do, and it's quite common as it's very useful. A constant can be an operator (a variable can't because a variable is state, and state must be an object in the theory). For example, it's useful for taking a relation as input (although a relation can also be defined as a set of pairs, so it’s an object in the theory). If in the polymorphic example you want to say that the set `a` is partially ordered (because you're specifying a sorting algorithm), you can write[1]:

    CONSTANTS a, _ ⊑ _
    ASSUME ∀x, y, z ∈ a :
              ∧ x ⊑ x
              ∧ x ⊑ y ∧ y ⊑ x => x = y
              ∧ x ⊑ y ∧ y ⊑ z => x ⊑ z

All of this, BTW, is actually the "+" in TLA+ (which is a bit technical, and trips me up occasionally), and not where the core concepts lie, which is the TLA part. Lamport would say you’re focusing on the boring algebraic stuff, rather than the interesting algorithmic stuff… I guess you could come up with another TLA language, with a different "+", but the choice of this particular "+" (i.e, set theory) was made after experimentation and work with engineers back in the '90s (Lamport says that early versions were typed). There is actually a type inferencer for TLA+, which is used when proofs are passed to the Isabelle backend (or intended to be used, I don't know; the proof system is under constant development at INRIA). So you get rich mathematical reasoning using simple math — no monads or dependent types (nor any types) necessary. Those things can be useful (for automatic code extraction, maybe, or for deep mathematical theories of languages — not algorithms), but for mathematically reasoning about programs, this is really all you need. And it works well, in the industry, for programs as small as a sorting routine or as large as a complex distributed database.

[1]: The aligned conjunctions are a syntactic convenience to avoid parentheses.

[tome]

Are those actually polymorphic? It seems like you've assumed a specific, concrete, a.

EDIT: On a second look, "CONSTANT" seems more like declaring a variable than requiring a concrete type.

EDIT 2: Hmm, still not completely sure about this ...

[pron]

Constants are external inputs to a specification. All you know about them is what you assert in the assumptions. When you use the proof system, the assumptions are your axioms and if you don't have any, then it's really polymorphic. If you use the model checker, you'll need to supply the checker with a concrete -- and finite[1] -- set for all constants.

[1]: The one supplied with TLA+, called TLC, is powerful enough to model-check an expressive language like TLA+, but it's algorithm is rather primitive; it's an "old-school" explicit state model-checker. A more modern, state-of-the-art model checker is under research: http://forsyte.at/research/apalache/. BTW, modern model checkers are amazing. Some can even check infinite models.