It seems to me like this should be something that can be done using continuations in Scheme. I tried writing the first example:
(define x 1)
(define t (now))
(display x)
(at t
(set! x 2))
and trying to implement now and at in a way that would behave correctly. I ran into a wall trying to implement it, because I don't think there is a way to define at that could reference the environment that t was defined in. Maybe a more powerful language like Kernel[0] could implement the same features, but I don't think Scheme can. Very cool!
Also FWIW here is the definition of now and at that I had before I decided to stop:
(define-syntax now
(syntax-rules ()
((_)
(call/cc
(lambda (k)
(lambda (at-body) (at-body) (k #f)))))))
(define-syntax at
(syntax-rules ()
((_ instant body1 body ...)
(instant (lambda () body1 body ...)))))
You might have to require that any code that uses the now/at constructs be wrapped in a macro invocation, e.g. (with-time-travel ...). The with-time-travel macro would then be a syntax transformer that rewrites the program. I'm not sure how, though... you'd have to enumerate all of the code blocks that are inside "at" forms, and then conditionally dispatch to them in the expansion of the "now" form; but that doesn't quite work because (now) is a value, and so figuring out which "at" forms consume it is probably undecidable. You can't have all the cases in the expansion, either, because of the incompatible environments.
It's an interesting problem, but one that I think is ok not to be able to solve in Scheme.
It's only legal for each `now` to be consumed by at-most one `at` form, so at that point you'd just be re-implementing the "timeline" and "instant" system from mariposa. The need to wrap the program in a form and the management of `now` "values" has me pondering the implications of IanTheHenry's macaroni[1] system, which (like the CSS :has operator) allow macros to climb up into manipulations of their parent forms-- the `now` macro could effectively wrap every remaining form in the program with a new context that augments eg. the closure of `at`. But indeed, perhaps a problem to not become too invested in :p
uh, case in point, that hypothetical closure would have some difficulty crossing module boundries (and that's assuming it gets away with re-writing top-level define forms), but still nothing technically incomputable, just supremely ill-advised and still closer to a reimplimentation of mariposa's semantics than a truely native concept emerging out of the continuations system
You could probably do it in the reflective language Black (<https://www.is.ocha.ac.jp/~asai/Black/>), but I'm gonna leave actually doing so as an exercise for someone who is interested.
Your approach is intriguing. I appreciate the inclusion of descriptions that elucidate what's happening in the code; this is often lacking in professional and scientific programming. This is particularly relevant in quantitative finance, where many bugs stem from misunderstandings related to the timing associated with variables.
To address this, we implemented a similar concept in ThetaML for defining stochastic processes, financial instrument payoffs, and trading strategies. We introduced the
theta t
operator, which represents the passage of time t. Here's how a stochastic process might be represented:
S = 1
loop inf
theta @dt
S = S * exp( (r - 0.5 * sigma^2) * @dt
end
We also introduced stochastic expressions like expected value E(V!) given the current state of all simulated values where V! is a reference to the future value of V.
Example:
1: model EuropeanPut
2: % This model returns a simulated European put option price
3: import S “Stock prices”
4: import CUR “Discount factor”
5: import K “Strike price for the European put option”
6: import T “Time to maturity in years”
7: export P “European put option price”
8:
9: P = E(V_CUR!)
10: % T years pass
11: theta T
12: % at maturity T, the option payoff is discounted to time 0
13: V_CUR = max(K - S, 0) * CUR
14:
15: end
This system enables the evaluation of the models using Monte Carlo Simulations and the computation of expected values E(x!) using regression techniques.
That reminds me of a funny presentation which is basically "if we engineered a bunch of exotic sci-fi concepts... what would the perl programs running on them look like?"
More formally: "Temporally Quaquaversal Virtual Nanomachine Programming In Multiple Topologically Connected Quantum-Relativistic Parallel Timespaces... Made Easy!"
This seems to have some parallels with durable execution engines like Temporal which have deterministic concepts of time and use event sourcing or snapshotting to ensure the past remains the past but allow you to evolve code for the future (disclaimer I work at Temporal).
Have you considered this approach to apply to more than time? There is all sorts of conditional-based divergence code may take beyond time.
I would love to see a future compiled programming language which would support some, or even all of the following compilation options:
1) Compile with "time travel" AKA point-in-time state memory enabled (and accept slower code execution).
2) Compile without "time travel", AKA standard compilation -- for much faster code execution.
3) Compile such that some, but not all sections of code will selectively save their exact state at points in time, and can be "time traveled" by a debugger -- but only for those sections of code explicitly marked.
4) Compile such that "time travel" could be selectively turned on or off (may require dynamic function recompilation at runtime) for any function or specific lines of code, as needed, during runtime!
Anyway, Mariposa looks like a step in the right direction -- and really cool!
Really cool project! It might be interesting to note that the mentioned time travel paradoxes can be solved by using probablistic states (as multi-valued interpretations of quantum mechanics would imply would be the case in any real system with time travel). And that this results in a computational system that can solve 'uncomputable' problems like the halting problem. See https://arxiv.org/abs/1609.05507. Time travel is really fun to think about in a computational setting!
Time loop logic is a hypothetical system of computation that exploits the Novikov self-consistency principle. In this system the computer is able to send the result of a computation backwards through time and rely upon the self-consistency principle to force the sent result to be correct.
I've written about this before. Instantaneous data transfer with zero lag is theoretically possible through use of quantum entanglement. You can use this same technique to build a doomsday clock similar to the film "Tomorrowland".
> I've written about this before. Instantaneous data transfer with zero lag is theoretically possible through use of quantum entanglement.
I hope you wrote a correction wherever you wrote this. Quantum entanglement can not transfer information by itself (because of the no-communication theorem) therefore any data transfer protocol that uses entanglement must also use some other form of communication (e.g. classical communication), and therefore is at most as fast as your other communication method is.
Maybe in general, but this is in the context of "time loop logic". Ordinarily, you can have entangled states where measuring both parts will produce the same (random) outcome. Unfortunately the outcome cannot be influenced by either party, so it's useless for communication, as you say.
Now suppose that the first party resolves to go back in time and kill his grandfather unless the bits he measures are precisely the message he wishes to send. The universe can't tolerate the paradox, so it is corralled into the only non-paradoxical outcome: both parties read the desired message. Something like that, anyway.
Ah I guess I misunderstood what was being claimed. I thought the claim was "you can use entanglement to instantly send messages", but it's actually "you can use entanglement and this model of how time travel might work to send messages instantly".
Obviously these are rather different. In fact I feel like the entanglement doesn't even help in the time-travel protocol. If you want to send messages instantly and you can send messages back in time, you can "just" send yourself the message distance/c seconds in the past and send it then. Some messing around let's you arrange for it to arrive at exactly the time you want to send it in the future.
Assuming what I wrote above is correct (I don't actually know anything about closed time-like curves), it's actually weirder than just going back in time and mailing a letter early so it arrives when you want. Specifically, once you set up the entangled state, no other communication between the parties is necessary.
Yeah I understand the proposed protocol using entanglement. I'm just saying that if you're assuming we have access to the ability to send messages back in time there are much simpler protocols to achieve instant communication /without/ having to do anything involving entanglement.
IMO this is like those discussions where someone says FTL communication is possible by using a very long solid rod, jiggling one and and monitoring the other... except on closer inspection it'll only work if the rod is infinitely rigid, which is already a violation of many of the same underlying physical laws.
So it's a kind of circular logic, or at best an observation that having one kind of supernatural magic power would let you cause another kind of supernatural magic outcome.
In this case, if only I had a time machine I could break the speed of light. (Or possibly vice-versa.)
> The principle asserts that if an event exists that would cause a paradox or any "change" to the past whatsoever, then the probability of that event is zero. It would thus be impossible to create time paradoxes.
> Instantaneous data transfer with zero lag is theoretically possible through use of quantum entanglement.
No, that's a common myth about quantum stuff.
The entangled relationship can't be used to transfer information on its own. Whatever you sample from the "instant parts" can only be checked and understood after additional context arrives in a conventional way--limited by the speed of light and the flow of time.
Ok human. You can read the Hans Moravec paper on CTC and time loop logic to understand Novikov self-consistency principle is formalized, yes you must run the computation for as long as it would have already taken or result will never arrive.
I say through "through use of quantum entanglement" as glossy term for reader. Crystalline quantum circuits are not really existing yet so is all scifi.
I won't be able to repsond to further posts in this thread. Cheers.
Time-loop logic does not violate causality. We are able to retrieve the answer instantly because we have committed to spending sixty seconds in the future calculating the answer and sending it back.
Maybe quantum superposition is just the universe compiling.
The blog-post asserts causality is not violated, but the author contradicts it elsewhere by claiming the hypothetical system would grant other benefits like "zero latency" gaming, which in turn means arbitrary data (e.g. human decisions) can somehow travel back-and-forth faster than light.
Then FTL communication opens up an enormous can of causality-worms.
That's a point, and I let them expand their definition of causality to include a chain of events flowing in a reversed arrow of time. I think they hand-wave away all those worms with the precept that any attempt to cause a paradox or other inconsistency would fail in practice. But I'd love to hear some examples that come to mind of problems that crutch doesn't fix.
I like the idea of this time travelling computer language. It got my head buzzing with all sorts of ideas about time travel in the real world too, and parallel universes!
You don't necessarily need to embed it into the programming language itself to get a ton of value. XTDB (https://github.com/xtdb/xtdb) offer a Clojure, Java and HTTP API for interacting with the database, which is bitemporal and lets you query the database for a specific point in time for example.
Why doesn't this print `1` before `2`, and then proceed to print `2` in a loop (i.e. treat `at` like a `goto`)? I think there is some detail that separates declaration and definitions of the environment from the execution, but the syntax doesn't make this obvious.
Maybe add (toy) programming language in the title?
I thought this would be a language integrating a time-travel debugger as main feature.
As a toy experiment it is fun, but shockingly useless if you come with such an expectation.
Well, that's at least a bit reductive. It's all electrons in most programs, but that doesn't mean we don't get advantages from higher level abstractions
In Haskell and other pure functional programming languages, monads are used to model arbitrary contexts. For example, in Haskell, there is a package which provides the Tardis monad which provides a time traveling context[1]. It can be used to solve some classes of algorithmic problems quite elegantly[2].
> Semantics and correctness of implementation
It is not obvious how the Mariposa language could be given a formal semantics. Since there is no specification of its semantics, it doesn't even make sense to ask if the implementation is right or wrong. However, we are sure that the implementation is incorrect for almost any conceivable semantics. It should be understood only as an exploratory game.
Exactly, there's no rationale given, nor any practical example of where this would be useful. Mutability is already a source of complexity, adding time-traveling to it seems like it would just make it worse...
Initially I followed the link wondering if perhaps the author had done something interesting regarding append only ledgers and derivative generation processing semantics (e.g. event 5 modifies event 2, impacting the proper processing of events 3 and 4). After all, the linearity of the character stream is not unlike log offset/ledger row.
Frequently these esoteric languages have very interesting purposes.
I don't know if this is still the case, but I recall needing to run LaTeX twice before it would produce the correct output. Something like this might make it easier to generate documents in one pass.
Sometimes LaTeX produced auxiliary files (e.g. for the table of contents) at the end of a compilation that that therefore wouldn't be used until the second pass. Long time since I needed to know that...
Also FWIW here is the definition of now and at that I had before I decided to stop:
[0] https://web.cs.wpi.edu/~jshutt/kernel.html