Can you give me a concrete example of a higher order computation in TLA? For example, can you show me how to construct a computation that runs another computation over all elements of a list?

It is actually very easy. I cover that in parts 3 and 4 of my series. I will answer your question, but the answer may sound a little tricky. Part of the problem is that simply in stating your question you have quite a few hidden assumptions that are natural in FP but don't take into account how an arbitrary computation can actually behave.

This is an example of a computation that is specifically tailored for functional languages, so let's instead start with something conceptually simpler for TLA, but downright impossible in FP: Plotkin's parallel or. Here you have a computation that takes two arbitrary computations, and simulates them in lockstep. [1]

Doing what you ask is certainly possible in TLA (in part 4), but that's just not how it's normally done. TLA allows you to abstract computations, i.e., extract some of their arbitrary features. As sequential computations of the kind you describe can correspond to functions and can be abstracted into function, that's exactly what you'll do in TLA+. You won't say "my computation runs an arbitrary computation over all elements of a list" (as is possible for Plotkin's or) because in order for that to make sense, that other computation must have certain features and cannot be arbitrary. In particular, it needs to behave like a function. So, what you'll write is a computation that runs something that can be represented as a function over all elements of a list. So, it will simply be:

    CONSTANTS T, R (* the "type" of elements in the in/out list *)
    VARIABLES in, out, f

    Map ≜ ∧ in ∈ Seq(T)
          ∧ f ∈ [T → R]
          ∧ □[∧ out' = Append(out, f[Head(in)])
              ∧ in' = Tail(in)
              ∧ UNCHANGED f]_⟨f, in, out⟩

As you'll note, there are no parameters at all. Instead, we use nondeterminism, i.e., define the computation for all lists of "type" T and for all functions T -> R.

Of course, this computation is then abstracted (for use by others) simply into:

    Map(list, f) ≜ [i ∈ DOMAIN list ↦ f[list[i]]]

which is how you'd normally write this in TLA+. This definition is fully polymorphic, as it's an operator, not a function. If we wanted a function instead, we need "type parameters":

    CONSTANTS T, R
    map[list ∈ Seq(T), f ∈ [T → R]] ≜ [i ∈ DOMAIN list ↦ f[list[i]]]

which is a proper higher-order function (but these functions are proper functions, not "functions" or computations).

In any event, f here is a function, not a computation. If for some reason you want to actually use a computation, you would need to specify more precisely what your expectations are of that computation (e.g., that it can take an argument at all). But, again, that's not how it's normally done in TLA+.

[1]: See here https://pron.github.io/posts/tlaplus_part3#plotkins-parallel... or here https://www.youtube.com/watch?v=15uy9Ga-14I

> In any event, f here is a function, not a computation. If for some reason you want to actually use a computation

Yes, absolutely I want to use a computation! The point is that I want to understand how TLA+ can abstract over computations.

First, take a look at the parallel or example [1]. It's a computation that manipulates two other completely arbitrary ones, in a simple, compositional way that's not possible in any other formalism I'm aware of. The idea is not too different from how continuous dynamical systems are composed to describe "higher order" systems, despite first-order representation.

Doing a "map" of a completely arbitrary computation f, would look like this:

    CONSTANTS T (* the "type" of elements in the in/out list *)
    VARIABLES in, out, f_param, f_result, f_done

    Map ≜ ∧ in ∈ Seq(T)
          ∧ f_param = Head(in)
          ∧ □[∧ f_done = TRUE ∧ f_done' = FALSE (* wait for f to work *)
              ∧ out'     = Append(out, f_result])
              ∧ f_param' = Head(in)               (* send another element to f *)
              ∧ in'      = Tail(in)
              ∧ UNCHANGED f_result
             ]_⟨f_param, in, out⟩ (* we don't allow f to change f_param, in or out *)

and then, the composition or the "application" would be:

    Map ∧ f

Nothing here guarantees that the computation f does any of those and that it terminates. We could do that by adding an assumption about f's behavior, that states that f behaves like a subroutine:

    f ⇒ □(f_done = FALSE ↝ f_done = TRUE)

which states that if ever f_done is false, f will cause it to eventually become true.

This is similar to how ODEs and processes in process calculi are composed, and all of this can be abstracted nicely into a "subroutine call" operator as I do in part 4. It is more cumbersome than sequential formalisms as composition is parallel "by default", but the technique is never used in practice precisely because of the Boolean algebra of computation that allows you to abstract appropriate computations as functions.

[1]: This is the exact spot in the video: https://youtu.be/15uy9Ga-14I?t=37m34s

Thanks. It will take me some time to digest this.

My 40 minute talk is a good intro to the theory, and the posts cover everything in great detail.

Also, I've given it some more thought, and I think that my original (slightly corrected) answer is actually the better way (even when dealing with computation), and I'll explain why below:

    CONSTANTS T, R (* the "type" of elements in the in/out list *)
    VARIABLES in, out, f

    Map ≜ ∧ in ∈ Seq(T)
          ∧ f ∈ [T → R]
          ∧ □[∧ Len(in) > 0
              ∧ out' = Append(out, f[Head(in)])
              ∧ in' = Tail(in)
              ∧ UNCHANGED f]_⟨f, in, out⟩

Now, I too fell victim to the Whorfian syndrome, and thought in terms of functions (subroutines), instead of thinking about the meaning of the map program. What does a map program mean? I.e., in the semantics of TLA, a program is the set of all its possible executions. Every parameter, is just another dimension of nondeterminism, which adds more possible execution. This holds for ordinary value parameters, but also for "function" arguments. What do we know about the function argument? Well, that it behaves like a partial function, meaning it could either never terminate, or return a response (which map will then write to the output list), but we also know (or, rather, choose to assume) that the argument isn't an arbitrary computation, but a pure "functions", which means that for every input it must return the same output. The above specification says exactly that (it may not terminate because we haven't added liveness conditions).

Map can then be composed with another computation that implements the mapping, and, if you watch the talk you'll see that the other computation may take as many steps as it likes due to stuttering invariance. The f function merely encodes our assumption about the mapping computation's behavior, namely that it always yields the same output to the same input. Without this assumption, the specification will simply look like:

    CONSTANTS T, R (* the "type" of elements in the in/out list *)
    VARIABLES in, out

    Map ≜ ∧ in ∈ Seq(T)
          ∧ □[∧ Len(in) > 0 (* sorry, forgot this before; must stop when the list is empty *)
              ∧ out' = ∃ y ∈ R : Append(out, y) (* completely nondeterministic in R *)
              ∧ in' = Tail(in)]_⟨f, in, out⟩

Now, we just state that any other computation must yield a value in R, but may not be "pure" and so may yield different values for the same input.

I may add this with the explanation to the posts.