Temporal Programming, a new name for an old paradigm

The first synchronous programming languages were, AFAIK, Statecharts and Esterel, the former designed by David Harel while he was working alongside Amir Pnueli, who would later win the Turing Award for introducing temporal logic to computer science. https://www.wisdom.weizmann.ac.il/~harel/papers/Statecharts....

Eve also combined synchronous programming with logic programming: https://witheve.com

There are precious few programs for which a|b ~ a;b is true for all atomic programs a,b where:

| is a parallel composition operator

; is the normal sequential composition operator (defined in the completely standard way in terms of updates to a global state or heap/stack-like structure if you want to be fancy)

~ is any sort of equivalence relation on reasonable and realistic semantics.

More-over, there are precious few programs that easily decompose into parts A,B,... such that A|B ~ A;B is true for each A and B in the set of parts. You can give theoretic characterizations of this fact, and many have, but the pragmatic point is more convincing.

Associativity and even reflexivity often fail as well.

The allure of this line of thought is promising, but alas... The "just make a simple algebra and arrange your programs to fit it" research program died early on for a reason. In the context of parallel and concurrent programs, it is hard/impossible to solve the decomposition problem at the language level of abstraction.

That pretty much summarizes outcome of a big chunk of program analysis research from the 70s to early 90s in a nutshell, unfortunately.

Let me briefly illustrate using OP's example:

`a' = b + 1; b' = a + 1`

from which I've deleted the errant training semicolon (it's `1+1` not `1+1+`!)

Suppose we instead have the program:

a' = a + b + 1; b' = a + b + 1

Now, the ordering does matter! No worries, so we order.

Additionally, suppose we put these programs into an outer while(true) loop and that's our whole program. Now what have we bought ourselves? Not much.

In this case we can solve that problem by... well, by solving some sort of integer recurrence equations that give us a program without loops which we can then think about algebraically. But of course this gets difficult or impossible very fast. (And, btw, the algebra part here did not buy us much. It was solving integer recurrence equations that saved the idea in this example). We haven't even added real data structures or external state yet.

Anyways, looks like OP is building something around this idea. Good luck! I'll be curious to see how you handle loops inside of blocks that contain @'d variables with recursively defined quantities :)

So John Backus not only suggested "Applicative State Transition" in his paper. He participated in ALGOL creation. Which influenced most contemporary languages.

We have this style of programming in our Pascal and Java programs.

Please no new names. Semicolon is semicolon.

Sorry, I can't find this blog or paper by Peyton Jones. Leaving that as an exercise for the reader :) And of course, I can misremember something.

https://en.wikipedia.org/wiki/Lucid_(programming_language)

They don't use x', but rather fby x, but otherwise the ideas seem very similar.

Of course, they called it dataflow, and Lucid inspired the "synchronous dataflow" languages like Esterel (imperative) and Lustre (functional). Which in turn inspired the non Conal Elliott variants of "FRP".

It's all related...

The wikipedia link describing it is overly arcane but here it is anyway: https://en.wikipedia.org/wiki/Operational_semantics

The idea behind STM is to specify some block of code as being one big fat atomic operation, and then the runtime will magically make it so. The idea behind SSA form is to only assign variables once, as doing so makes imperative optimization as easy as functional.

I wonder if the author knows about these things, or if they're coming in at a different angle.

Are people interpreting using their own experience, or is there a big overlap?

This sounds a lot like graph computation but on an extremely granular level.

You need a data base with full history (transaction time), try datomic. Additionally if you need full history AND domain time (bi-temporal) included in your data base, try or xtdb.

Functions.

> x = x + 1 would not be valid, while x' = x + 1 would be.

Yep.

    void tick() {
      a@ = b + 1;
      b@ = a + 1;
    }

For example

always @(posedge clk) begin A <= B; B <= A; end

swaps A and B on each positive clock edge.

You don’t need a functional language to do this. However it does require more discipline when the language doesn’t enforce purity.

And once I started thinking about software this way I realised that events are important and should be the core of any software design. Basically the application is a single function that takes an event and the current state, and computes a new state and zero or more events.

The IO type in haskell is defined,

    newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))

* simulation variables (presumably because the separation into x/x' is similar to the now/next calculation of state in a lot of simulations).

* SSA (although there is a subtle difference as x' becoming x in the next period isn't really SSA without some extra edges in the graph).

I wonder how phi nodes would fit into the author's scheme?

i call this "wave" calculation - as the algo to find the sequence after each input change/stimulus is spreading changes like wave from-the-point-of-change-outwards, in topological sort. There might be (direct or indirect) recursion allowed, up to some predefined level, or minimum-change-diff thresholds or whatever.

Writing a calculator for such set of rules is relatively easy, from memory they were like 1000 lines in c++, 100 lines python, 200 lines js.. it more depends on the "syntax" and conveniencies for the programmers, than actual engine.

Now, Turning that into full language .. will be really interesting. Kind of turning inside-out the relation wavecalc <--> general-language-of-choice..

If you write your program this way, how does it interact with the environment (e.g user input, output, network…)? Something is missing.

And if it doesn’t interact with the environment, then your program is just one big pure function, in which case you get all of the benefits in OP’s proposal anyway, without having to worry about transforming old state to new state, you just gotta transform input to output.

Firstly, we define a place (temporal x y) such that when this place is accessed, it denotes x, and when it is assigned, the assignment goes to y:

  (defplace (temporal-place var var*) body
    (getter setter
      ^(macrolet ((,getter () ,var)
                  (,setter (val) ^(set ,',var* ,val)))
         ,body))
    (setter
      ^(macrolet ((,setter (val) ^(set ,',var* ,val)))
         ,body)))

  (define-place-macro temporal (var var*) ^(temporal-place ,var ,var*))

  (defmacro temporal (var var*) var)

Here is a let-like macro which sets up the specified variable as temporal. The initial values propagate into both the old and new location.

Then before the last form of the body is evalulated, the new values are copied to the old values.

  (defmacro temporal-let (vars . body)
    (let ((olds (mapcar (ret (gensym)) vars))
          (news (mapcar (ret (gensym)) vars)))
      ^(let* (,*(zip olds [mapcar cadr vars])
              ,*(zip news olds))
         (symacrolet ,(zip [mapcar car vars]
                           [mapcar (op list 'temporal) olds news])
           ,*(butlast body)
           (set ,*(weave olds news))
           ,*(last body)))))

  1> (temporal-let ((x 1) (y 2))
        (set x y)
        (set y x)
        (list x y))
  (2 1)

  2> (expand '(temporal-let ((x 1) (y 2))
        (set x y)
        (set y x)
        (list x y)))
  (let* ((#:g0024 1)
         (#:g0025 2)
         (#:g0026 #:g0024)
         (#:g0027 #:g0025))
    (sys:setq #:g0026
      #:g0025)
    (sys:setq #:g0027
      #:g0024)
    (progn (sys:setq #:g0024
             #:g0026)
      (sys:setq #:g0025
        #:g0027))
    (list #:g0024 #:g0025))

  2> (disassemble (compile-toplevel '(temporal-let ((x 1) (y 2))
        (set x y)
        (set y x)
        (list x y))))
  data:
      0: 1
      1: 2
  syms:
      0: list
  code:
      0: 20020002 gcall t2 0 d1 d0
      1: 04010000
      2: 00000400
      3: 10000002 end t2
  instruction count:
      2
  #<sys:vm-desc: 903ec50>

  1> (let ((*opt-level* 0))
       (disassemble (compile-toplevel '(temporal-let ((x 1) (y 2))
         (set x y)
         (set y x)
         (list x y)))))
  data:
      0: 1
      1: 2
  syms:
      0: list
  code:
      0: 04020004 frame 2 4
      1: 2C800400 movsr v00000 d0
      2: 2C810401 movsr v00001 d1
      3: 2C820800 movsr v00002 v00000
      4: 2C830801 movsr v00003 v00001
      5: 2C820801 movsr v00002 v00001
      6: 2C830800 movsr v00003 v00000
      7: 2C800802 movsr v00000 v00002
      8: 2C810803 movsr v00001 v00003
      9: 20020002 gcall t2 0 v00000 v00001
     10: 08000000
     11: 00000801
     12: 10000002 end t2
     13: 10000002 end t2
  instruction count:
     12
  #<sys:vm-desc: 9de1b50>