Additional time axes allow you to separate transactions from different sources of input. E.g. in a collaborative system it could be helpful to ask questions while rewinding the actions of a particular user.
But a different question is whether the system can do something useful for you with first-class time co-ordinates, compared to just stuffing additional timestamps into your data. (something useful being clever indexing, compaction, maybe more?)
If model-theoretic semantics and the various ways to slice, dice, and extend Datalog are interesting to you, then almost any talk by Peter Alvaro might be as well.
I think Finda (https://keminglabs.com/finda/) fills a similar need, runs offline, and indexes lots of other stuff as well. Although I think it is not possible to assign additional keywords.
Jonathan Blow's language "jai" allows for seamlessly switching between AoS and SoA and generally seems to value efficient data layout and "gradual" optimization over safety (in contrast to e.g. Rust).
Unfortunately, no public compiler seems to be available at this time.
I think that's cool, but I would almost say that's like the `const` problem of c++ and the Open System problem. It's a single special keyword. Not a point to extend with arbitrary layouts. It is progress, but a very small step.
AoS is useful for things where you want to effectively have fast (e.g. no cache misses) random access to many fields; the common OO approach. SoA is useful when you want fast iteration across only a couple fields of many objects; the common simulation loop approach. Effectively what Jai allows is deciding which to use when you declare a chunk of memory.
A lot of concerns I have can all theoretically be fixed in user space, on the other hand the same can be said for any language, and hence sort of defeats the purpose of a keyword. The point of the keyword is that it can inspect the fields of a type and decide how many arrays of what size to allocate. Here are some issues which would be annoying to implement in user space with AoS/SoA being merely an orthogonal keyword (e.g. limited operator overloading and without Turing Complete templates or macros):
* Alignment and padding so certain fields can be loaded into specific registers. This effects the layout of memory differently in each mode.
* Multiple buffers for some fields. A heavily used field (say position) could have a number of buffers which are rotated in SoA mode (e.g. render-posistions, last-frame-step, next-frame-step; allowing for reader/writer systems), and are simply an array of fields in AoS mode. Where as other fields retain their singular arity.
* Concurrency concerns. Partitioning arrays in SoA so cores don't fight over the lower caches. Aligning AoS on cache lines so whole objects can be locked at once without causing cache problems with neighboring objects.
* Sparse fields. If a field is generally empty, space is still allocated for it (e.g. in SoA using a dictionary rather than an array), or a cache miss due to usage of a pointer.
* But to answer the actual question it comes down to data structures: If I wanted to iterate across objects in an arbitrary quad-tree node and it's children, there are efficient ways to layout memory so that that and similar useful operations are fast (e.g. minimal cache misses). Yes I could put the data-structure in a different array but then I am looking up values in the data array randomly (e.g. cache misses). Many useful data structures have efficient systems for laying out their values and their structure in the same memory.
To elaborate on the last one more, maybe I have a structure that has 4 fields, two are keys that can be structured (e.g. string name, and x,y pos), and two are are actual data members. Regardless of `AoS` or `SoA`, I would have to write custom data structures to maintain string (trie) and pos2 (quad tree) indices, that would also be doing slow lookups. Alternatively, if I could set the layout of an array to `Trie.name` (Trie using name field) I would be saying, layout this container to be as fast as possible (e.g minimal cache misses) for string based lookups by making it the primary layout, without having to change any code that uses it (you could even go the next step with something like: `SoA | Trie.name | QuadTree.pos` to allow reordering a single line of code to effect the performance of all code referencing it, but for the semantics of the line to act like normal bit flags).
tl;dr: Think database indices on columns, but improving runtime performance by rearranging the data itself into the index so as to better fit the algorithm and CPU requirements (e.g. rather than more abstract decisions in databases, where the model of a piece of hardware isn't usually a concern).
I mean I'm not worrying about it at that level, just that it's something relevant to the idea of layout. C++'s templates are a powerful language feature for doing layout optimization however, and it's sort of the thing to beat in power.
For anyone interested in exploring the datomic model, there is a great ClojureScript in-memory implementation called datascript (https://github.com/tonsky/datascript) by Nikita Prokopov.
We use Datalog every day in a React-Native application, via the datascript db (https://github.com/tonsky/datascript).
Has been a very positive experience so far.
Thinking in "facts" / binary relations is itself a refreshing approach.
Clojure, with its dabbling in schemas and rule systems / logic programming (as a substitute for conditional statements) and thanks to its great tools (like figwheel or devcards), could really be establishing a cheaper, "as-good" alternative to static typing and full formal verification.
Instead of encoding constraints as type signatures, the Clojure folks (true to character) encode them in data. In my eyes a very interesting, pragmatic trade-off between expressiveness and automatic verifiability.
> Instead of encoding constraints as type signatures, the Clojure folks (true to character) encode them in data.
I've never bought this line of thinking when the "Clojure folks" also say "code is data", because then a syntactic type signature you write down is also just data. If you want to consume the type signature (or spec signature or whatever) as syntax (as a sibling comment suggests), use a macro or any other program which consumes programs.
The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time.
Lastly, I strongly disagree these approaches are meant as a replacement for static typing or formal verification because (as far as I can tell) a value can be checked against a spec on demand, but makes zero guarantees as to what that value does in other parts of a program. This is also in contrast to Racket contracts, which will give you the correct blame information between parties using and not using contracts.
You make a very good point, the comparison was flawed there.
> The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time.
This is a better way to put it. The second important factor for me is expressiveness. With spec or any other contracts-like system one gets the full power of the language to express constraints. Of course type systems are not artificially restricted in this regard, they simply make a different trade-off.
I hope my comment did not come off as a riff on static vs dynamic typing, and I don't think any contract system is meant to replace type systems. Until expressing all important program specifications formally becomes viable for everyone (maybe through this work https://www.math.ias.edu/vladimir/current_work?), a less-formal, dynamic approach seems very attractive.
I hear you on expressiveness of using the language. Of course (and as you mention) the strength of restricting the expressiveness is that it becomes decidable in some amount of acceptable time for most programs.
I agree with your last sentiment but I don't think it has to be any less "formal" than something like Coq. I just think we shouldn't be so concerned with proving all properties of a program before running. And then we can turn the knob to adjust how much to prove during vs. before running.
> a value can be checked against a spec on demand, but makes zero guarantees as to what that value does in other parts of a program
The spec is just metadata. How it's used is part of the tooling. I see nothing precluding using specs in tools that employ and analyze that information in different ways.
Yep you are totally correct. I only point this out because the tool presented here does not do the same thing as other contract systems, but could (as you say) be used as a building block to get there.
Important to note, that as data, they can be consumed by other systems for other purposes. For example, it's feasible to consume a spec within Alloy and use a SAT solver (which is made even easier given the split on keyset). This pushes spec from design and requirements validation, into runtime constraints, and on through to tests and verification.
As a side note in his talk "Simple Made Easy" (https://www.infoq.com/presentations/Simple-Made-Easy, around minute 42)
Rich Hickey mentions, that conditional statements are complex, because they spread (business-)logic throughout the program.
As a simpler (in the Hickey-sense) alternative, he lists
rule systems and logic programming. For example, keeping parts of the business logic ("What do we consider an 'active' user?", "When do we notify a user?", etc...) as datalog expressions, maybe even storing them in a database, specifies them all in a single place. This helps to ensure consistency throughout the program. One could even give access to these specifications to a client, who can then customise the application directly in logic, instead of chasing throughout the whole code base.
Basically everyone involved agrees on a common language of predicates explicitly, instead of informally in database queries, UI, application code, etc...
But Hickey also notes that this thinking is pretty "cutting-edge" and probably not yet terribly practical.
It can work. My current company uses a rule system to represent most of our business logic since it is so dynamic. The downside is that we have to rebuild the entire graph into memory (times the number of threads, times the number of app servers) every time anything changes (which is constant).
Facebook wrote about rebuilding a similar system in Haskell that only changes memory incrementally, so it's definitely possible to do better.
Full, formal verification of complex systems (especially in the distributed case) requires a lot of modelling effort, beyond what is needed for "mere" implementation. A lot of important constraints cannot even be expressed in most type systems. And if one uses a specialised modelling language for the proof, the actual implementation might introduce bugs.
Also relevant to real, shipping software: specifying a program in such that detail as required for automatic verification makes it even harder to change (which, given infinite time and money, is indeed a very very good property!).
This just goes to say, that a type system can be very helpful, but is ultimately just a part of regular testing.
So for most companies and most developers, anything that aides in keeping documentation up-to-date, writing or generating tests and helping developers understand what they are reading is probably a better ROI.
If static type systems cannot do everything, it does not make sense to me to conclude that they shouldn't then be used for anything. Type systems aren't part of "regular testing", they're part of compile-time error checking.
That was not the intension behind my comment at all. I rely on type systems a lot, myself.
I was trying to note that Clojure, as a dynamic language, is making a (to my eyes) very interesting choice, of doubling down on these dynamic methods of verification. For some uses, I can see this as the better choice, for others it isn't and won't be.
As I commented elsewhere, Clojure very deliberately adopts the stance that type systems like Haskell's are valuable but heavyweight, and chose development speed and concision over types.
In my own work, I chose Clojure because it mirrored my experiences: that type systems weren't worth the trade-offs for me and my field.
Would I prefer stronger typing in different domains (longer project times available, greater consequences of failure like medical devices, etc.)? Sure, and I have in the past. But it's not the case that dynamic languages are always the incorrect choice, like smoking cigarettes.
When you prove that a language like Clojure (untyped, but with dispatch that is no more dynamic than that of many modern typed languages) combined with a construct like specs is significantly less safe than any typed language, then you can make that statement. It's not like untyped and typed are two binary categories; otherwise, I could say that wanting less dangerous typed languages as opposed to formal tools are just like wanting less dangerous cigarettes. These ideas exist on a spectrum.
But a different question is whether the system can do something useful for you with first-class time co-ordinates, compared to just stuffing additional timestamps into your data. (something useful being clever indexing, compaction, maybe more?)