The “implicit surfaces” described sound a lot like signed distance fields; any relation?
Also the demo is cool but I’m a little sad that it doesn’t have a pre-made program for the fidget spinner in the intro screenshot. ;_; (also the 3D examples are cool, I think it’s some weird polar coord setup so it’s a bit… uh, fidget-y but you can rotate them by dragging right mouse button.)
I had the same question regarding implicit surfaces and signed distance fields, and it appears that they’re the same, but the term implicit surfaces is used in academic/mathematical contexts and the terms SDFs is used in industry/game development contexts.
Not quite :) Mathematically, an implicit surface is a surface defined by the set of points I(f) \equiv {x | f(x) = 0 }, for any function R^n -> R. For example, a circle of radius 2 is the implicit surface of the function f((x, y)) := x^2 + y^2 - 2. That is, I(f) := { (x, y) | x^2 + y^2 - 2 = 0 }, which is the set of points on a circle of radius 2.
To recap: The operator I that builds as implicit surface takes as input a functionf, and produces as output a surfaceI(f).
Now, a signed distance function goes the other way round: It takes as input a surfaceS, and produces as output a functionSDF(S). This function, when fed a point p, gives the (signed) distance from the surface S to the point p. You can define this non-constructively by just saying “please find the point on the surface with minimum distance”: SDF(S)(p) := min_{x in S} dist(p, x).
As an example, if we choose the surface S to be the set of points on a circle of radius 3 union the set of points on a circle of radius 4, i.e. S := { (x, y) | x^2 + y^2 - 3 = 0 \/ x^2 + y^2 - 4 = 0}, then we can show that a signed distance function for this surface is g(p) = min(p.x^2 + p.y^2 - 3, p.x^2 + p.y^2 - 4).
Of course, when we informally think of this, we are in the lucky situation where we blur the lines between all of these. For example, when I say “circle of radius 2, we don’t bother to distinguish between the polynomial that vanishes on the circle, f(x, y) := x^2 + y^2 - 2, the equation that cuts out the points of the circle, I(f) := { (x, y) | x^2 + y^2 - 2 = 0 }, and the signed distance function of this implicit surface, which also happens to be f. But this is merely a lucky situation, that SDF(I(f)) = f in this case.
In general, the type signatures of these are different!
The reason signed distance functions are useful is that they take geometric operations on surfaces and convert them to algebraic properties of functions:
SDF(S1 U S2) = min(SDF(S1), SDF(S2))
SDF(S1 INTERSECT S2) = max(SDF(S1), SDF(S2)).
.
–
A question whose answer I don’t know, and would like to be enlightened: When is SDF(I(f)) = f? Is there a (categorical) adjunction between I and SDF? Feels vaguely algebro-geometric to me.
This happens in grad school semi-regularly. In my case I stayed enrolled in my old school but was paid as a grad student in my new school. It’s all coming out of grants that travel with the lab anyway. Universities generally make it pretty painless as a matter of courtesy.
We were all given the option, and all but one of us chose to move to Cambridge :) It involved dropping out of Edinburgh and then re-applying to Cambridge.
This is a nice literate walkthrough. If one wants to know specifically how to implement egg, I apparently hacked up a literate Monte module explaining that in detail. The paper to read is de Moura & Bjørner 2007 which introduces a virtual machine that can efficiently search e-classes.
Very nice, my previous implementation turned out to be incredibly messy, and you seem to have put some thought into making it non-messy: I especially like the idea of sealing the batching directly into the API. Super, will reimplement this and let you know how it goes!
Monte is easily transliterable to Python; each object literal needs its own class, and the pattern-matching one-liners have to be expanded into two or three lines of imperative actions. The resulting code will be missing most of the safety checks we built into the language, though.
Excellent post! I would say that this is the interpreter design pattern, where one writes a pure function that returns commands such as treeactions::SetupWindow, which can then be interpreted by different consumers (the real implementation, the test harness).
Closely related is the “functional core, imperative shell” pattern, where the functional core produces pure commands that are impurely interpreted.
This is all generalized to abstract nonsense via the free monad/cofree comonad, or if one prefers, extensible effects/effect handlers. The key idea is that once again, the core says what effects ought to happen (e.g. treeactions::SetupWindow) and an effect handlers decides how to implement this effect.
Flying to austin to spend 3 months at the AWS’ automated reasoning group writing Lean! Pretty excited :)
Hobby plan: implement “cutting to the chase” (https://leodemoura.github.io/files/cutsat.pdf), a solver for linear integer arithmetic in Lean.
there’s something strange going on here that I can’t place. Let’s cal f to be the function that takes our sum type and tells us what the config type should look like.
From the article, we agree that f(A + B) = 2 X A x B.
I now reason as follows:
For a boolean option, I need to have two options: f(2) = 2
For a non-option (ie, type with a single constructor), I need to have no options at all, because there is nothing to choose: f(1) = 0.
But this leads to a contradiction, since I have both f(2) = 2, and f(2) = f(1 + 1) = 2 x f(1) x f(1) = 2 x 0 x 0 = 0!
A fix that suggests itself is that f(1) = 1, but this seems to suggest that one should crate a “dummy”, permanently selected option field for a thing a user can’t change, which I find weird
I think you are conflating cardinality (2 = boolean, 1 = unit, 0 = uninhabited) with bits of information (1 = boolean, 0 = unit). In terms of cardinality, f(1) = 1 makes sense to me. It’s a unit type so you are storing nothing, and the transformation is a no-op.
To be candid, I joined academia for programmer inspo. It’s been a very interesting time — I was both right and wrong for doing so. Ways I ways right: There are high quality conferences that publish work on accounts of it being “beautiful”. Ways I was wrong: There are high quality conferences that reject work on account of it not being impactful. I get the sense (from speaking to my peers and superiors) that if one favours beauty over impact, then one’s likelihood of being able to “make it” in academia is lowered. Regardless, I’m quite happy to publish in an area (interactive theorem proving) where a paper on building dependent type nonsense for verifying compilers can be published next to a paper on build maths nonsense for verifying a pure maths conjecture.
Going to do a shit ton of admin for my J-1 Visa for a summer research internship for Amazon in the US! Excited about the research, not so much about the paperwork :(
Slowly setting up a stable benchmarking environment for a better reference counting algorithm (FBIP / frame limited reuse) for the Lean proof assistant.
Continuing to write a formally verified music synthesizer, whose UI is Rust and whose core data model is in Lean.
Learning how to carve soapstone here at a local artist at Cambridge!
I got a “lean (the programming language) core, rust shell” setup going: https://github.com/leanprover/lean4/pull/4271. I’m excited to implement a polished, fully keybindings based “piano roll” application for my jazz piano explorations.
In particular, I’m looking forward to having the manipulations for multiple cursors, undo/redo, and so on fully formally verified. This should prove theorems that every pair of operators one wants to be inverses to really be inverses (or at the worst, galois connections).
One hopes that this leads to a bug free, crash free, keyboard driven, piano roll DAW!
Waiting on tenderhooks about our submission results to ITP 2024, planning out the next two ish years of my PhD, and deciding what our paper sprint to POPL is going to look like!
As usual, I am obligated to plug one of the neatest ideas in this biome of computing: the futamura projection. The key idea is that given a language L, and a partial evaluator peval : L x L -> L, we can get a compiler, and even a JIT compiler out!
A restriction that is sometimes glossed over is that one needs the condition that peval is metacircular: that is, peval in L. See that is not a necessary condition for something to be a partial evaluator: for example, an interpretive partial evaluator obeys the type signature peval: L x L -> L but could be implemented in another language.
Thanks for the links. Implementing a partial evaluator for a small language, capable of the Futamura projections, seems like an interesting hobby project?
Some caveats from the second link:
Does partial evaluation eliminate the need to write compilers? Yes and no. . .
Pro: when given a language definition in the form of an operational semantics, a partial
evaluator eliminates the first and largest order of magnitude: the interpretation
overhead. A virtue is that the method yields target programs that are always
correct with respect to the interpreter. Thus the problem of compiler correctness
seems to have vanished. This approach is clearly suitable for prototype implementation of new languages from interpretive definitions.
Contra: the generated target code is in the partial evaluator’s output language,
typically the language the interpreter is written in. Thus partial evaluation will not
devise a target language suitable for the source language, e.g. Python bytecodes.
It won’t invent new runtime data structures either, so human creativity seems
necessary to gain the full handwritten compiler efficiency.
So what language M are you compiling your hobby language into? You’ll need a partial evaluator for M. For example, in order to use the Futamura projections to compile your hobby language into WASM, you would need an interpreter for the language written in WASM, and a partial evaluator that operates on WASM.
And that’s the problem the OP solves: weval is the partial evaluator you’d need for this.
I have never seen a “link log” before. I think that is a really cool tool (and it is available for others). Does your search look at only the titles of the links?
The software is low-effort symbiosisware, barely serviceable for my own use, and so bad I would not wish it on my worst enemies. It’s basically a single-user pinboard or delicious.
The search is the stupidest thing that could possibly work: it splits the query into words and does substring matches on the titles and urls, and lists the matching entries with the words emboldened. It is absolute shit for brains and works really well.
I’m sure @fanf meant RPython, the toolkit which builds PyPy and similar binaries, performs the first Futamura projection when translating to C. You’re allowed to not think of the JIT as a second Futamura projection, but it’s not a bad perspective when trying to understand how the JIT is optimizing one’s interpreter actions.
Ah, sorry, I may be wrong. Deegen takes “an interpreter” (but really the interpreter is your operational semantics encoded in C++) and generates both an interpreter and a compiler.
I used to think that this technique was magic, but now I think it gives you “A” compiler, but not necessarily a good compiler or the one you want. There are still a lot of engineering tradeoffs, and there’s a lot of work to do to make it fast
I still want to play with it (and weval actually sounds perfect for that), but I see it more as a “side quest”
All of lightweight modular staging (https://scala-lms.github.io/) is based off of the futamura projection, which in my mind was the “academic” establishment that this works “in practice”.
That looks like a nice JIT library to me. I couldn’t see anything about partial evaluation within the first handful of pages; do you have a more pertinent link?
Marching Cubes isn’t very complicated, it’s basically a pattern match on each voxel (every voxel is one of a fixed set of triangles). It’s slightly complicated by the fact that the original paper (and patent!) had an error.
Marching Trapeziums Tetrahedra[1] is basically the same algorithm, but has fewer cases and so is much easier to understand intuitively.
[1] Edit: Stupid pre-coffee brain gets shape names confused when they start with the same letter, even if they have different numbers of dimensions and sides.
No, because my pre-coffee memory was autocompleting the wrong shape name. Post coffee, the thing I was thinking of was Marching tetrahedra. This is the original paper. One of the books in the citations section at the end of the Wikipedia article was a coauthor of mine during my PhD, which is probably why the algorithm is more firmly entrenched in my brain than the name of it seems to be.
$work: modern 3D graphics pipelines and computational geometry. It’s very different from what I’ve been doing lately and hugely rewarding. Also very intimidating. Computational geometry was pretty low on my list of things to learn on my own back in uni, and nowhere in my curricula – I know my way around the basics but much of that was picked up informally over the years, from reading source code and the like. It’s a little foreign for someone whose math background was shaped by an EE curricula.
I’m moderately happy that, even though it’s gone largely unused for a few years, my math is still good enough that I can mostly approach this by reading selected chapters. Most of the basics (e.g. Euclidean vectors) are either second-nature or things that I was interested in back when I had more time for pure mathematics (e.g. quaternions) so I can generally google/textbook my way into anything.
$notwork: I’m playing with RISC-V. This is actually a good excuse to do some security/RE and OS development work, which is what I’ve always dreamed of doing. Back when I finished uni and had to stop being a pest in my parents’ home, the labour market in my area was hardly rewarding in these fields (it fluctuated between “absent” and “largely amateurish”, it still does in fact) so I ended up doing embedded development instead. I didn’t regret it one bit, I loved doing that; but now that the zombie apocalypse has made remote working somewhat more widespread, I’m kind of hoping to get into it a few years down the line. If the world of computer graphics doesn’t suck me in, that is; if it does, it’s still as rewarding a hobby as it was twenty years ago.
I’m very curious what $work is where you get work on computational geometry. I’m a huge fan, and I’ve been curious where in industry one gets to work on this type of thing (I’m still in academia), so having some insight into what you do would be super useful when I eventually go job hunting :)
I’m very curious what $work is where you get work on computational geometry.
The answer might be somewhat disappointing in strictly academic terms but $work = I’m making games :-). I can’t say much for obvious reasons but the game I’m working on has a CAD-like component of sorts; and in order for it to be fun, lots of things have to happen automatically. Think Kerbal Space Program but the rocket design module tries to do more of “the right thing” by itself.
I don’t think I’ll need to write too much original CG code in the next few months – it’s a little early to tell but I expect most of the stuff I need is already present in a library out there, that’s generally been the case so far. But I also can’t just codemonkey my way around it. Game players are notoriously unconstrained users, if your algorithm has a cornercase, they’ll find it, so even if all I end up doing is knitting third-party code, I need to be able to understand what it does and why.
That’s the most pressing concern, in any case. There’s a less pressing concern in the tooling department that may need some lower-level work. That’s for later down the road but I don’t want to cram for it, either.
This is interesting. I hope they open-source their changes to clang. (I understand this is currently a WIP.) Transactional memory is awesome, and so is being able to use foreign C++ code from a language with transactional memory, while preserving those semantics.
You probably don’t want to use this for c++; the main point of it is to be an ergonomic stopgap for implementing verse. In particular, the combination of:
not drawing a distinction between transactional and non-transactional data
drawing a distinction between transactional and non-transactional control, and wanting to impose ‘‘‘zero cost’’’ on the latter
structural deficiencies in c++ and llvm
means that the semantics is very much not what you want. If you ever access the same data both inside and outside of a transaction, your state will get silently fucked up; in particular:
writes inside of a transaction will not appear atomic to concurrent reads outside
if a write outside of a transaction is concurrent with a transaction accessing the same data, then serialisability is permanently lost
most damningly, non-transactional accesses not concurrent with any other accesses can still blow up; this is the privatisation problem
These problems can’t be solved at the library level in c++—my common lisp tm library is safe and scalable in a way that java and c++ tm libraries aren’t and fundamentally can’t be—and they can’t be solved at the language/implementation level without being much more aggressive. But a library tm (multiple already exist) strikes a much more reasonable balance. You explicitly annotate your transactional data, and get ‘‘‘zero-cost’’’ access to everything else. The semantic problems I outlined above completely disappear. The only thing you have to make sure of is that, inside of a transaction, you don’t do any side effects except accesses to transactional locations or locations you allocated inside of the transaction. Which—sure, it’s nice they make bad side effects trap, but you could also solve this problem with a linter, and maintain compatibility with normal c++ implementations.
Excellent. I got a lot of insight by reading your response and the Joe Duffy essay together. Thanks for the clear explanation.
I’m interested in using STM in a high level language, which can be designed to make safety and semantic guarantees, such as “fearless concurrency”. My interest in C++ is only from the perspective of interfacing to external libraries that already exist and are written in a systems language.
From that perspective, it seems to me that STM has an expressiveness / safety tradeoff. You could provide an STM api that is fully “safe”, meaning it guarantees the STM semantics. But you wouldn’t be able to perform general I/O inside an atomic block. You could only change the state of transactional data. That’s enforced by the implementation, maybe using an effects system.
In order to make new kinds of transactional data, like an ACID database, or remote transactional data using a distributed STM protocol, both of which require general I/O, you need an “unsafe” low level STM protocol. If the code using this protocol is buggy, then STM semantics will break. So, code using this protocol is either unsafe, meaning it’s up to the caller to use the API safely, or it is marked as “trusted”, meaning it is unsafe code on the inside but the API is safe to use. The unsafe, low level STM api lets you perform I/O and includes the explicit ‘retry’.
I thought maybe Epic was building a C++ compiler that makes C++ safe for STM, but maybe that is impossible even with CHERI hardware.
Take a look at ‘open nested transactions’. The main thing aside from safety is, you end up needing to make a stable interface to your tm, which involves encoding a whole bunch of assumptions about how the tm works. My tm attains wait-freedom and scalability by making certain assumptions about how transactional locations are represented and what operations can be performed on them; another tm might make different assumptions. So you say ‘includes the explicit “retry”’, but this glosses over the fact that it will be necessary to agree on a rather specific and potentially nonobvious interface (or else do a simple interface and get stuck with sucky performance characteristics and progress guarantees).
My take: don’t write anything in c++; just use one bootstrapped ‘high level’ language. Solve the disc and network problems once, systemically, for everybody (apropos disc, everything should be transparent persistence too). Interaction with alternate transactional protocols can be done with libraries, as usual, but should not be first-class interoperable.
If you just want to use c++ just to implement stm interfaces in an unsafe way, then you likely do not want or need any help making it safer—because the code that could use that help is going to be basically none of the code that you’re actually writing.
C++ safe for STM, but maybe that is impossible
Not impossible; they were just scared ;)
expressiveness / safety tradeoff
Interesting framing. I hadn’t thought of it this way before. Seems reasonable. But most tms are unsafe and inexpressive.
Solve the disc and network problems once, systemically, for everybody (apropos disc, everything should be transparent persistence too).
That’s exactly what I want.
Interaction with alternate transactional protocols can be done with libraries, as usual, but should not be first-class interoperable.
That’s harsh. Does that mean I can’t implement my safe STM compatible transparent persistence on top of SQLite, because it uses an alternate transactional protocol?
You can do whatever you want; I’m just saying what I think is a good idea.
You could transparently implement persistence in your system using sqlite as the storage backend (though it wouldn’t be a great idea, since sqlite doesn’t scale). And if you think it might be interesting to support multiple backends, then it might be useful to make the internal interfaces somewhat modular. All I’m saying is that I don’t think these interfaces should be stable or publicly exposed, because you want to allow tight coupling.
I don’t know exactly what your goals are for this system, but I’ll offer up a design I came up with for transparent persistence with transactions. Use thread-local heaps, but on escape, use replication. Let objects in the global heap have a different layout, with the requisite metadata to support transactions; now you can transact on any object (for thread-local objects, no metadata is required for transactions, since you’re the only one who can access them).
Keep and persist a log of committed transaction logs—every access to a global object has to be treated as a single-operation transaction, and a corresponding log logged; but most data are local, so the overhead should not be too high. There is no need to agree on an order for transaction logs, since the logs themselves should already contain enough information to order them post-hoc, so this logging is scalable. But you do want to be able to gc your logs, by periodically taking a coherent heap snapshot and then throwing out all the previous logs. This does require synchronisation, but it can be amortised, so it still scales—you have to establish a linearisation point, s.t. every transaction happened either before or after it. Then, to actually realise the new snapshot, you could go through the log and apply all the transactions to the last snapshot, but that would be slow; faster is to use the current state of the heap. Walk through and sample it, just one location at a time; if the location has not been changed since the time when the snapshot logically happened (which is very likely), then it goes into your snapshot; otherwise, you do have to look in the logs to see what the value was.
That takes care of the shared heap; what about the thread-local heaps? Before you snapshot the shared heap, synchronise with each thread separately and snapshot its heap. Aside from scaling well, this allows different sampling policies per thread; maybe a throughput-oriented thread wants to shut down while you snapshot it, whereas a latency-oriented thread wants to stay online, but temporarily switch to a slower mode in which it helps you do the snapshot. And if a thread hasn’t done much coordination, maybe don’t bother snapshotting it at all. Then, for each thread, you do have to keep logs of the transactions it performed between the time you snapshotted it and the time when you snapshotted the shared heap, but only the reads; the writes are no longer necessary.
The tone of my reply wasn’t great; sorry if it aggravated you.
That’s a lot of good ideas to consider.
My goal is a hobby-oriented programming language for “personal dynamic media”, as Alan Kay called it in his paper about Smalltalk and the Dynabook. It’s not industrial and I don’t intend to process web traffic, so the scaling problems of SQLite probably doesn’t affect me. I would like to periodically synchronize data across my devices. I want the language to describe a GUI, 3D graphics, audio, hypertext documents, and personal data, and to perform general computations on those things, related to my hobby activities. There’s a version controlled document store. It should be transparently persistent, so that my GUI session and the state of the debugger for whatever code I was debugging is restored after a shutdown. It would be cool if that GUI and debugger state could be synchronized or moved across machines, so that GUI sessions can migrate, but I haven’t figured out how to implement that. If I can at least seamlessly synchronize “documents” (the model part of model/view/controller), that would be cool.
The single-threaded, non-persistent prototype that I built represents data using immutable values, and processes data using pure functions. I am able to use reference counted objects (and no GC) for that prototype, even though that wouldn’t work for a Shared Mutable State language like Lisp or Smalltalk. I use copy-on-write and in-place mutation to efficiently implement functional operations that modify one element of a larger data structure. That technique relies on accurate reference counts.
Generalizing this sequential language into something that supports concurrency and I/O and transparent persistence and a versioned document store is a big change, so I’ve started looking at things like STM, Functional Reactive Programming and Capabilities to get an idea of how concurrency will work.
I like the idea of distinguishing the shared heap from thread-local heaps. I’ve had this idea before in the context of a different concurrency problem, and it seems powerful.
This conversation has given me a better idea of the diversity of STM implementations. Since I have immutable data, I should look at Clojure and Haskell implementations of STM. For example, I just looked at Revisiting Software Transactional Memory in Haskell. Compared with the original 2005 Haskell STM, they claim better performance, better forward progress guarantees, and a simpler implementation. Since I am a neophyte at this stuff, and it’s a one person project, the “simpler implementation” claim stands out. They say that immutable data simplifies the design, and that they don’t need nested transactions or nested logs.
May I have a link to your common lisp transactional memory library? Also, perhaps a small elucidation of how common lisp makes this possible would be super! [i am guessing the answer is conditions and macros ;) ]
The answer is macros and not conditions. A tm may be opaque or not; if it is opaque, then it never exposes an incoherent state to an in-progress transaction. If it is non-opaque, then it may expose an incoherent state to an in-progress transaction, but that transaction will abort when it tries to commit, so it seems like no harm will be done. The problem is that, in an unsafe tm, it is incumbent upon you to make sure that you do nothing ‘bad’ inside of a transaction, so now you have to make sure that you do nothing bad even in the face of incoherent state; this is actually an extremely programmer-hostile interface. Whereas with an opaque tm, you only ever have to think about nice, coherent states. At least, that’s the folklore.
The problem is—opacity costs; a tm which does not have to provide opacity can scale much better. I get around the problem by making a cl-to-cl compiler which, when you do something bad, checks if the state was incoherent; if it was, then it simply restarts the transaction; otherwise, it signals an error. Hence: fundamentally safe and scalable.
If cl treated conditions as effects and used them to implement all side effects, then that would almost suffice—almost, but not quite. Because nontermination is also a kind of effect; if you get into an infinite loop because you observed an incoherent state (where you wouldn’t have entered an infinite loop had you seen only coherent states), then I have to handle that too, but an infinite loop may never do any side effects. Obviously I can’t prove whether something is an infinite loop or not. But I can instrument the generated code to periodically check (at exponentially expanding intervals, to maintain the right asymptotics) whether the state it observed is coherent, and restart if not.
I disagree with this explanation. I think the correct explanation should at least try to convey the notion of “how a tensor transforms”, to go with the somewhat meme definition of “a tensor is something that transforms like a tensor”. To put my money where my mouth is, here is my shot at an explanation that tries to explain the “invariance principle” of tensors and “how coordinates transform” by using “memory location” as my coordinate system.
Suppose I implement a double ended queue using two pointers:
See that the state of the queue is technically three numbers, { memory, start, end } (Pointers are just numbers after all). But this is coordinate dependent, as start and end are relative to the location of memory. Now suppose I have a procedure to reallocate the queue size:
Notice that when I do this, the values of start and end can be completely different!
However, see that the length of the queue, given by (end - start) is invariant: It hasn’t changed!
In the exact same way, a “tensor” is a collection of numbers that describes something physical with respect to a particular coordinate system (the pointers start and end with respect to the memory coordinate system). “tensor calculus” is a bunch of rules that tell you how the numbers change when one changes coordinate systems (ie, how the pointers start and end change when the pointer memory changes). Some quantities that are computed from tensors are “physical”, like the length of the queue, as they are invariant under transformations.
Tensor calculus gives a principled way to make sure that the final answers we calculate are “invariant” / “physical” / “real”. The actual locations of start and end don’t matter, as (end - start) will always be the length of the list!
Physicists (and people who write memory allocators) need such elaborate tracking, to keep track of what is “real” and what is “coordinate dependent”, since a lot of physics involves crazy coordinate systems (https://en.wikipedia.org/wiki/Schwarzschild_metric#History), and having ways to know what things are real and what are artefacts of one’s coordinate system is invaluable. For a real example, consider the case of singularities of the Schwarzschild solution to GR, where we initially thought there were two singularities, but it later turned out there was only one “real” singularity, and the other singularity was due to a poor choice of coordinate system:
Although there was general consensus that the singularity at r = 0 was a ‘genuine’ physical singularity, the nature of
the singularity at r = rs remained unclear.
In 1921 Paul Painlevé and in 1922 Allvar Gullstrand independently produced a metric, a spherically symmetric solution of Einstein’s equations, which we now know is coordinate transformation of the Schwarzschild metric, Gullstrand–Painlevé coordinates, in which there was no singularity at r = rs. They, however, did not recognize that their solutions were just coordinate transforms
I think this bumps up against a problem with jargon: Physicists, in particular, say “tensor” when mathematicians say “tensor field”. Saying “a tensor is a thing that transforms like a tensor” makes some kind of sense when talking about tensor fields, as those live on a manifold and have to transform the correct way when we change coordinates on the manifold. As you point out, encoding these transformations is incredibly valuable when doing calculations, to the point that modern mathematicians will say that something is “geometric” if it can be expressed as a tensor field and don’t like to consider any other kind of object.
A “tensor field” is made up of “tensors” that vary from point to point. A “tensor” is something we made up to linearize multilinear maps of vectors: Given a vector space V over a field k and a map b : V x V -> k that is linear in each variable separately, there exists a vector space V o V (the tensor product of V with itself) along with a bilinear map V x V -> V o V and a linear map f : V o V -> k such that the composition V x V -> V o V -> k equals b. The upshot is that instead of having to deal with a bilinear map b, we can deal with a linear one f.
The latter kind, the standard mathematical linear algebra object, is what “tensors” in computer science are. There are no transformations or invariance under them going on. As the original post points out, it is valuable to consider “tensors” not only as multidimensional matrices, but as those plus some operations, but those operations are not the coordinate transformations of tensor fields.
In mathematics, a tensor is the multilinear linear map itself, not the grid of numbers that is isomorphic to the multilinear map upon choosing bases. This is literally why we need tensors, a map V x V -> F and a map V x V* -> F could have the same matrix under a choice of basis, but be entirely different linear maps, and will transform differently when the basis changes! This is not what is used in computer science, where we conflate the “grid of numbers” with the “linear map” in itself.
This is a great high-level explanation that gets across the fact that tensors aren’t merely n-dimensional arrays and why, and it makes me wonder what an explanation targeted at someone with a decent linear algebra background would look like. When I first really started learning what tensors are, I had a good grasp on vector spaces and an okayish grasp on dual spaces and I didn’t really feel like tensors clicked for me until I saw them expressed in the formulation of a tensor product of some number of vectors and covectors, but it took a longer duration of me feeling like I just wasn’t getting the concept than feels necessary in retrospect before the intuition hit me. Maybe that’s just how it has to go, but I retain this suspicion that a 3blue1brown-style exposition of tensors is possible, in the sense of there being a detailed explanation of them that of course doesn’t substitute for actually doing math but would serve as a really great intuitive framework with which to approach the subject in a more in-depth way. It’s something I’d like to take a crack at some day, but it seems like a non-trivial project and I’m certainly not lacking for those already.
Close, but one must also discuss contra-variance :
Let’s start with the view that a tensor is really a transformation of the coordinate axes between two spaces A and B.
In your queue example, the transformation is a linear translation (the memory offset), and the two spaces are really the same, our memory.
What if our transformation were a rescaling of the axis, e.g. changing representation from bytes to bits?
Then you would see that memory offsets are contravariant wrt this transformation: an offset of n bytes becomes an offset of 8 n bits, while our “reference” (bits vs bytes) has shrunk by a factor 8.
In full generality, a tensor is a transformation of coordinate frames that has both co- and contra-variant indices.
Work: Waiting for PLDI reviews for two of our papers, and preparing responses and polished code in anticipation.
We’re also organizing a compiler social at the Cambridge, so anyone interested in compilers / formal verification / hardware, please do drop by! (https://grosser.science/compiler-social-24-feb/)
Feel invited to drop by even if you have a passing interest in the topics. My research group has just moved to cambridge, and we have a culture of hosting these events to hang out with folks in the area where we are based ^_^
I personally will be very happy to hang out and chat about anything maths and proofs!
Does anyone have any other resources for how these things work? I found this years ago when trying to figure out how Coq’s termination checker works, but this one is pretty simple. I think I’ll try reimplementing it this week
Recall that Coq is more complex, as the kernel has various heuristics for how pattern matches on inductives ought to decrease. In particular, the term “coq guard condition” brings up the relevant literature. Unfortunately, I don’t know of a pedagogical reference, and would very much love to know one!
This is an area I’m very keen on learning better (PhD student here), so I’d love to know more references!
Buying cutlery for my new home in cambridge! Suggestions for places with nice, pre-owned cutlery welcome!
Other than that, continuing to hack on my Lean “IDE” (more like minimal LSP stress test): https://github.com/bollu/elide
I’ve also been thinking about crocheting as a stack based language, and it’s quite interesting! I think it even has a type system which tracks the number of loops, and the consumption of loop resources (forward versus backward loops). I might eventually write a small thing up for SIGBOVIK if this turns out to be fun enough.
There is a little cluster of charity shops on Burleigh St near the Grafton shopping centre. It’s also worth taking a look along Mill Road where many of the more interesting shops are. (I was about to suggest Cutlack’s, but sadly they seem to have moved to Ely.)
The “implicit surfaces” described sound a lot like signed distance fields; any relation?
Also the demo is cool but I’m a little sad that it doesn’t have a pre-made program for the fidget spinner in the intro screenshot. ;_; (also the 3D examples are cool, I think it’s some weird polar coord setup so it’s a bit… uh, fidget-y but you can rotate them by dragging right mouse button.)
I had the same question regarding implicit surfaces and signed distance fields, and it appears that they’re the same, but the term implicit surfaces is used in academic/mathematical contexts and the terms SDFs is used in industry/game development contexts.
Sounds plausible, yeah. My best guess was that implicit surfaces is the idea and signed distance fields was a particular implementation of the idea.
Not quite :) Mathematically, an implicit surface is a surface defined by the set of points
I(f) \equiv {x | f(x) = 0 }, for any functionR^n -> R. For example, a circle of radius2is the implicit surface of the functionf((x, y)) := x^2 + y^2 - 2. That is,I(f) := { (x, y) | x^2 + y^2 - 2 = 0 }, which is the set of points on a circle of radius 2.To recap: The operator
Ithat builds as implicit surface takes as input a functionf, and produces as output a surfaceI(f).Now, a signed distance function goes the other way round: It takes as input a surface
S, and produces as output a functionSDF(S). This function, when fed a pointp, gives the (signed) distance from the surfaceSto the pointp. You can define this non-constructively by just saying “please find the point on the surface with minimum distance”:SDF(S)(p) := min_{x in S} dist(p, x).As an example, if we choose the surface
Sto be the set of points on a circle of radius 3 union the set of points on a circle of radius 4, i.e.S := { (x, y) | x^2 + y^2 - 3 = 0 \/ x^2 + y^2 - 4 = 0}, then we can show that a signed distance function for this surface isg(p) = min(p.x^2 + p.y^2 - 3, p.x^2 + p.y^2 - 4).Of course, when we informally think of this, we are in the lucky situation where we blur the lines between all of these. For example, when I say “circle of radius
2, we don’t bother to distinguish between the polynomial that vanishes on the circle,f(x, y) := x^2 + y^2 - 2, the equation that cuts out the points of the circle,I(f) := { (x, y) | x^2 + y^2 - 2 = 0 }, and the signed distance function of this implicit surface, which also happens to bef. But this is merely a lucky situation, thatSDF(I(f)) = fin this case.In general, the type signatures of these are different!
The reason signed distance functions are useful is that they take geometric operations on surfaces and convert them to algebraic properties of functions:
SDF(S1 U S2) = min(SDF(S1), SDF(S2))SDF(S1 INTERSECT S2) = max(SDF(S1), SDF(S2)).–
A question whose answer I don’t know, and would like to be enlightened: When is
SDF(I(f)) = f? Is there a (categorical) adjunction betweenIandSDF? Feels vaguely algebro-geometric to me.So how does a whole research group moving work? Did you have the option to stay at Edinburgh?
This happens in grad school semi-regularly. In my case I stayed enrolled in my old school but was paid as a grad student in my new school. It’s all coming out of grants that travel with the lab anyway. Universities generally make it pretty painless as a matter of courtesy.
We were all given the option, and all but one of us chose to move to Cambridge :) It involved dropping out of Edinburgh and then re-applying to Cambridge.
This is a nice literate walkthrough. If one wants to know specifically how to implement
egg, I apparently hacked up a literate Monte module explaining that in detail. The paper to read is de Moura & Bjørner 2007 which introduces a virtual machine that can efficiently search e-classes.De Moura & Bjorner of Z3 fame?
Very nice, my previous implementation turned out to be incredibly messy, and you seem to have put some thought into making it non-messy: I especially like the idea of sealing the batching directly into the API. Super, will reimplement this and let you know how it goes!
In what language are you implementing this? Would you be open to sharing?
Sure, I’ll probably do it in lean4 and C++ : https://github.com/bollu/lean.egraphs
The repo contains two implementations, one in C++, and the other in Lean :)
Sweet!
Have you poked at this at all? The reimplementation?
Oh very cool!! I wonder if this helps with the built-in matching DSL that I didn’t bother to implement. How close is Monte to Python?
Monte is easily transliterable to Python; each
objectliteral needs its ownclass, and the pattern-matching one-liners have to be expanded into two or three lines of imperative actions. The resulting code will be missing most of the safety checks we built into the language, though.Very cool. Thank you
Excellent post! I would say that this is the interpreter design pattern, where one writes a pure function that returns commands such as
treeactions::SetupWindow, which can then be interpreted by different consumers (the real implementation, the test harness).Closely related is the “functional core, imperative shell” pattern, where the functional core produces pure commands that are impurely interpreted.
This is all generalized to abstract nonsense via the free monad/cofree comonad, or if one prefers, extensible effects/effect handlers. The key idea is that once again, the core says what effects ought to happen (e.g.
treeactions::SetupWindow) and an effect handlers decides how to implement this effect.I’m reminded of how I have effects take place in my stack machine interpreter for a BASIC dialect — the stack machine is parameterised by an
Effectstype, which for regular interpreted use just does the thing, in tests records output for later assertion, when running in an embedded context does the thing, but on UART, etc. :)oh thanks! i know what i am going to research next :)
Flying to austin to spend 3 months at the AWS’ automated reasoning group writing Lean! Pretty excited :) Hobby plan: implement “cutting to the chase” (https://leodemoura.github.io/files/cutsat.pdf), a solver for linear integer arithmetic in Lean.
there’s something strange going on here that I can’t place. Let’s cal f to be the function that takes our sum type and tells us what the config type should look like.
From the article, we agree that f(A + B) = 2 X A x B.
I now reason as follows:
But this leads to a contradiction, since I have both f(2) = 2, and f(2) = f(1 + 1) = 2 x f(1) x f(1) = 2 x 0 x 0 = 0!
A fix that suggests itself is that f(1) = 1, but this seems to suggest that one should crate a “dummy”, permanently selected option field for a thing a user can’t change, which I find weird
I think you are conflating cardinality (2 = boolean, 1 = unit, 0 = uninhabited) with bits of information (1 = boolean, 0 = unit). In terms of cardinality, f(1) = 1 makes sense to me. It’s a unit type so you are storing nothing, and the transformation is a no-op.
To be candid, I joined academia for programmer inspo. It’s been a very interesting time — I was both right and wrong for doing so. Ways I ways right: There are high quality conferences that publish work on accounts of it being “beautiful”. Ways I was wrong: There are high quality conferences that reject work on account of it not being impactful. I get the sense (from speaking to my peers and superiors) that if one favours beauty over impact, then one’s likelihood of being able to “make it” in academia is lowered. Regardless, I’m quite happy to publish in an area (interactive theorem proving) where a paper on building dependent type nonsense for verifying compilers can be published next to a paper on build maths nonsense for verifying a pure maths conjecture.
Settling the camera-ready for our paper about mechanizing MLIR semantics in the Lean proof assistant
Slowly upstreaming the theoretical development necessary to allow bitblasting multiplications in LeanSAT (Reference paper here)
Going to do a shit ton of admin for my J-1 Visa for a summer research internship for Amazon in the US! Excited about the research, not so much about the paperwork :(
Heading over to the tate modern in london, I’m super excited to see a light exhibition (https://www.tate.org.uk/whats-on/tate-modern/anthony-mccall)
Slowly setting up a stable benchmarking environment for a better reference counting algorithm (FBIP / frame limited reuse) for the Lean proof assistant.
Continuing to write a formally verified music synthesizer, whose UI is Rust and whose core data model is in Lean.
Learning how to carve soapstone here at a local artist at Cambridge!
I got a “lean (the programming language) core, rust shell” setup going: https://github.com/leanprover/lean4/pull/4271. I’m excited to implement a polished, fully keybindings based “piano roll” application for my jazz piano explorations.
In particular, I’m looking forward to having the manipulations for multiple cursors, undo/redo, and so on fully formally verified. This should prove theorems that every pair of operators one wants to be inverses to really be inverses (or at the worst, galois connections).
One hopes that this leads to a bug free, crash free, keyboard driven, piano roll DAW!
Waiting on tenderhooks about our submission results to ITP 2024, planning out the next two ish years of my PhD, and deciding what our paper sprint to POPL is going to look like!
Very cool! I love partial evaluation.
As usual, I am obligated to plug one of the neatest ideas in this biome of computing: the futamura projection. The key idea is that given a language
L, and a partial evaluatorpeval : L x L -> L, we can get a compiler, and even a JIT compiler out!A restriction that is sometimes glossed over is that one needs the condition that
pevalis metacircular: that is,peval in L. See that is not a necessary condition for something to be a partial evaluator: for example, an interpretive partial evaluator obeys the type signature peval:L x L -> Lbut could be implemented in another language.Anyway, given such a bobble, one can take an iterpreter, and partial evaluate a partially applied partial evaluator to get a JIT compiler :) I can’t explain the idea as well as this technical report can, so I link to “Partial Evaluation and Automatic Program Generation” (PDF).
Thanks for the links. Implementing a partial evaluator for a small language, capable of the Futamura projections, seems like an interesting hobby project?
Some caveats from the second link:
So what language M are you compiling your hobby language into? You’ll need a partial evaluator for M. For example, in order to use the Futamura projections to compile your hobby language into WASM, you would need an interpreter for the language written in WASM, and a partial evaluator that operates on WASM.
And that’s the problem the OP solves:
wevalis the partial evaluator you’d need for this.I enjoy this blog post regarding Futamura projections. There’s diagrams!
http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html?m=1
When I searched my link log for Futamura I found that blog post and a paper on Graal and Truffle
I have never seen a “link log” before. I think that is a really cool tool (and it is available for others). Does your search look at only the titles of the links?
The software is low-effort symbiosisware, barely serviceable for my own use, and so bad I would not wish it on my worst enemies. It’s basically a single-user pinboard or delicious.
The search is the stupidest thing that could possibly work: it splits the query into words and does substring matches on the titles and urls, and lists the matching entries with the words emboldened. It is absolute shit for brains and works really well.
The Futamura-oriented partial evaluators that I know of are
Are there any more?
It was a science-fictional idea for decades so it’s remarkable to see practical implementations spreading like this.
fwiw now Pypy is meta-tracing, not partial evaluation anymore
I’m sure @fanf meant RPython, the toolkit which builds PyPy and similar binaries, performs the first Futamura projection when translating to C. You’re allowed to not think of the JIT as a second Futamura projection, but it’s not a bad perspective when trying to understand how the JIT is optimizing one’s interpreter actions.
There’s also DeeGen, based on copy and patch, but it’s not released yet
Where does DeeGen use partial evaluation? I’m not seeing that in the source.
Ah, sorry, I may be wrong. Deegen takes “an interpreter” (but really the interpreter is your operational semantics encoded in C++) and generates both an interpreter and a compiler.
FWIW this thread on HN has a good discussion of the tradeoffs of the technique vs. traditional compilers: https://news.ycombinator.com/item?id=40408147
I used to think that this technique was magic, but now I think it gives you “A” compiler, but not necessarily a good compiler or the one you want. There are still a lot of engineering tradeoffs, and there’s a lot of work to do to make it fast
I still want to play with it (and weval actually sounds perfect for that), but I see it more as a “side quest”
All of lightweight modular staging (https://scala-lms.github.io/) is based off of the futamura projection, which in my mind was the “academic” establishment that this works “in practice”.
That looks like a nice JIT library to me. I couldn’t see anything about partial evaluation within the first handful of pages; do you have a more pertinent link?
Very nice man! Hats off to anyone that understands marching cubes - it’s still magic to me today :). (I haven’t really studied it at all.)
You may enjoy my SDF based modeler too. https://github.com/lf94/summonscript - uses raylib also (via Zig), and libfive for meshing.
As you’re probably aware, there are tons of us. :p
Marching Cubes isn’t very complicated, it’s basically a pattern match on each voxel (every voxel is one of a fixed set of triangles). It’s slightly complicated by the fact that the original paper (and patent!) had an error.
Marching
TrapeziumsTetrahedra[1] is basically the same algorithm, but has fewer cases and so is much easier to understand intuitively.[1] Edit: Stupid pre-coffee brain gets shape names confused when they start with the same letter, even if they have different numbers of dimensions and sides.
Got a reference to marching trapeziums?
No, because my pre-coffee memory was autocompleting the wrong shape name. Post coffee, the thing I was thinking of was Marching tetrahedra. This is the original paper. One of the books in the citations section at the end of the Wikipedia article was a coauthor of mine during my PhD, which is probably why the algorithm is more firmly entrenched in my brain than the name of it seems to be.
$work: modern 3D graphics pipelines and computational geometry. It’s very different from what I’ve been doing lately and hugely rewarding. Also very intimidating. Computational geometry was pretty low on my list of things to learn on my own back in uni, and nowhere in my curricula – I know my way around the basics but much of that was picked up informally over the years, from reading source code and the like. It’s a little foreign for someone whose math background was shaped by an EE curricula.
I’m moderately happy that, even though it’s gone largely unused for a few years, my math is still good enough that I can mostly approach this by reading selected chapters. Most of the basics (e.g. Euclidean vectors) are either second-nature or things that I was interested in back when I had more time for pure mathematics (e.g. quaternions) so I can generally google/textbook my way into anything.
$notwork: I’m playing with RISC-V. This is actually a good excuse to do some security/RE and OS development work, which is what I’ve always dreamed of doing. Back when I finished uni and had to stop being a pest in my parents’ home, the labour market in my area was hardly rewarding in these fields (it fluctuated between “absent” and “largely amateurish”, it still does in fact) so I ended up doing embedded development instead. I didn’t regret it one bit, I loved doing that; but now that the zombie apocalypse has made remote working somewhat more widespread, I’m kind of hoping to get into it a few years down the line. If the world of computer graphics doesn’t suck me in, that is; if it does, it’s still as rewarding a hobby as it was twenty years ago.
I’m very curious what $work is where you get work on computational geometry. I’m a huge fan, and I’ve been curious where in industry one gets to work on this type of thing (I’m still in academia), so having some insight into what you do would be super useful when I eventually go job hunting :)
The answer might be somewhat disappointing in strictly academic terms but $work = I’m making games :-). I can’t say much for obvious reasons but the game I’m working on has a CAD-like component of sorts; and in order for it to be fun, lots of things have to happen automatically. Think Kerbal Space Program but the rocket design module tries to do more of “the right thing” by itself.
I don’t think I’ll need to write too much original CG code in the next few months – it’s a little early to tell but I expect most of the stuff I need is already present in a library out there, that’s generally been the case so far. But I also can’t just codemonkey my way around it. Game players are notoriously unconstrained users, if your algorithm has a cornercase, they’ll find it, so even if all I end up doing is knitting third-party code, I need to be able to understand what it does and why.
That’s the most pressing concern, in any case. There’s a less pressing concern in the tooling department that may need some lower-level work. That’s for later down the road but I don’t want to cram for it, either.
This is interesting. I hope they open-source their changes to clang. (I understand this is currently a WIP.) Transactional memory is awesome, and so is being able to use foreign C++ code from a language with transactional memory, while preserving those semantics.
You probably don’t want to use this for c++; the main point of it is to be an ergonomic stopgap for implementing verse. In particular, the combination of:
means that the semantics is very much not what you want. If you ever access the same data both inside and outside of a transaction, your state will get silently fucked up; in particular:
These problems can’t be solved at the library level in c++—my common lisp tm library is safe and scalable in a way that java and c++ tm libraries aren’t and fundamentally can’t be—and they can’t be solved at the language/implementation level without being much more aggressive. But a library tm (multiple already exist) strikes a much more reasonable balance. You explicitly annotate your transactional data, and get ‘‘‘zero-cost’’’ access to everything else. The semantic problems I outlined above completely disappear. The only thing you have to make sure of is that, inside of a transaction, you don’t do any side effects except accesses to transactional locations or locations you allocated inside of the transaction. Which—sure, it’s nice they make bad side effects trap, but you could also solve this problem with a linter, and maintain compatibility with normal c++ implementations.
Excellent. I got a lot of insight by reading your response and the Joe Duffy essay together. Thanks for the clear explanation.
I’m interested in using STM in a high level language, which can be designed to make safety and semantic guarantees, such as “fearless concurrency”. My interest in C++ is only from the perspective of interfacing to external libraries that already exist and are written in a systems language.
From that perspective, it seems to me that STM has an expressiveness / safety tradeoff. You could provide an STM api that is fully “safe”, meaning it guarantees the STM semantics. But you wouldn’t be able to perform general I/O inside an atomic block. You could only change the state of transactional data. That’s enforced by the implementation, maybe using an effects system.
In order to make new kinds of transactional data, like an ACID database, or remote transactional data using a distributed STM protocol, both of which require general I/O, you need an “unsafe” low level STM protocol. If the code using this protocol is buggy, then STM semantics will break. So, code using this protocol is either unsafe, meaning it’s up to the caller to use the API safely, or it is marked as “trusted”, meaning it is unsafe code on the inside but the API is safe to use. The unsafe, low level STM api lets you perform I/O and includes the explicit ‘retry’.
I thought maybe Epic was building a C++ compiler that makes C++ safe for STM, but maybe that is impossible even with CHERI hardware.
Take a look at ‘open nested transactions’. The main thing aside from safety is, you end up needing to make a stable interface to your tm, which involves encoding a whole bunch of assumptions about how the tm works. My tm attains wait-freedom and scalability by making certain assumptions about how transactional locations are represented and what operations can be performed on them; another tm might make different assumptions. So you say ‘includes the explicit “retry”’, but this glosses over the fact that it will be necessary to agree on a rather specific and potentially nonobvious interface (or else do a simple interface and get stuck with sucky performance characteristics and progress guarantees).
My take: don’t write anything in c++; just use one bootstrapped ‘high level’ language. Solve the disc and network problems once, systemically, for everybody (apropos disc, everything should be transparent persistence too). Interaction with alternate transactional protocols can be done with libraries, as usual, but should not be first-class interoperable.
If you just want to use c++ just to implement stm interfaces in an unsafe way, then you likely do not want or need any help making it safer—because the code that could use that help is going to be basically none of the code that you’re actually writing.
Not impossible; they were just scared ;)
Interesting framing. I hadn’t thought of it this way before. Seems reasonable. But most tms are unsafe and inexpressive.
That’s exactly what I want.
That’s harsh. Does that mean I can’t implement my safe STM compatible transparent persistence on top of SQLite, because it uses an alternate transactional protocol?
You can do whatever you want; I’m just saying what I think is a good idea.
You could transparently implement persistence in your system using sqlite as the storage backend (though it wouldn’t be a great idea, since sqlite doesn’t scale). And if you think it might be interesting to support multiple backends, then it might be useful to make the internal interfaces somewhat modular. All I’m saying is that I don’t think these interfaces should be stable or publicly exposed, because you want to allow tight coupling.
I don’t know exactly what your goals are for this system, but I’ll offer up a design I came up with for transparent persistence with transactions. Use thread-local heaps, but on escape, use replication. Let objects in the global heap have a different layout, with the requisite metadata to support transactions; now you can transact on any object (for thread-local objects, no metadata is required for transactions, since you’re the only one who can access them).
Keep and persist a log of committed transaction logs—every access to a global object has to be treated as a single-operation transaction, and a corresponding log logged; but most data are local, so the overhead should not be too high. There is no need to agree on an order for transaction logs, since the logs themselves should already contain enough information to order them post-hoc, so this logging is scalable. But you do want to be able to gc your logs, by periodically taking a coherent heap snapshot and then throwing out all the previous logs. This does require synchronisation, but it can be amortised, so it still scales—you have to establish a linearisation point, s.t. every transaction happened either before or after it. Then, to actually realise the new snapshot, you could go through the log and apply all the transactions to the last snapshot, but that would be slow; faster is to use the current state of the heap. Walk through and sample it, just one location at a time; if the location has not been changed since the time when the snapshot logically happened (which is very likely), then it goes into your snapshot; otherwise, you do have to look in the logs to see what the value was.
That takes care of the shared heap; what about the thread-local heaps? Before you snapshot the shared heap, synchronise with each thread separately and snapshot its heap. Aside from scaling well, this allows different sampling policies per thread; maybe a throughput-oriented thread wants to shut down while you snapshot it, whereas a latency-oriented thread wants to stay online, but temporarily switch to a slower mode in which it helps you do the snapshot. And if a thread hasn’t done much coordination, maybe don’t bother snapshotting it at all. Then, for each thread, you do have to keep logs of the transactions it performed between the time you snapshotted it and the time when you snapshotted the shared heap, but only the reads; the writes are no longer necessary.
The tone of my reply wasn’t great; sorry if it aggravated you. That’s a lot of good ideas to consider.
My goal is a hobby-oriented programming language for “personal dynamic media”, as Alan Kay called it in his paper about Smalltalk and the Dynabook. It’s not industrial and I don’t intend to process web traffic, so the scaling problems of SQLite probably doesn’t affect me. I would like to periodically synchronize data across my devices. I want the language to describe a GUI, 3D graphics, audio, hypertext documents, and personal data, and to perform general computations on those things, related to my hobby activities. There’s a version controlled document store. It should be transparently persistent, so that my GUI session and the state of the debugger for whatever code I was debugging is restored after a shutdown. It would be cool if that GUI and debugger state could be synchronized or moved across machines, so that GUI sessions can migrate, but I haven’t figured out how to implement that. If I can at least seamlessly synchronize “documents” (the model part of model/view/controller), that would be cool.
The single-threaded, non-persistent prototype that I built represents data using immutable values, and processes data using pure functions. I am able to use reference counted objects (and no GC) for that prototype, even though that wouldn’t work for a Shared Mutable State language like Lisp or Smalltalk. I use copy-on-write and in-place mutation to efficiently implement functional operations that modify one element of a larger data structure. That technique relies on accurate reference counts.
Generalizing this sequential language into something that supports concurrency and I/O and transparent persistence and a versioned document store is a big change, so I’ve started looking at things like STM, Functional Reactive Programming and Capabilities to get an idea of how concurrency will work.
I like the idea of distinguishing the shared heap from thread-local heaps. I’ve had this idea before in the context of a different concurrency problem, and it seems powerful.
This conversation has given me a better idea of the diversity of STM implementations. Since I have immutable data, I should look at Clojure and Haskell implementations of STM. For example, I just looked at Revisiting Software Transactional Memory in Haskell. Compared with the original 2005 Haskell STM, they claim better performance, better forward progress guarantees, and a simpler implementation. Since I am a neophyte at this stuff, and it’s a one person project, the “simpler implementation” claim stands out. They say that immutable data simplifies the design, and that they don’t need nested transactions or nested logs.
May I have a link to your common lisp transactional memory library? Also, perhaps a small elucidation of how common lisp makes this possible would be super! [i am guessing the answer is conditions and macros ;) ]
It is not released yet.
The answer is macros and not conditions. A tm may be opaque or not; if it is opaque, then it never exposes an incoherent state to an in-progress transaction. If it is non-opaque, then it may expose an incoherent state to an in-progress transaction, but that transaction will abort when it tries to commit, so it seems like no harm will be done. The problem is that, in an unsafe tm, it is incumbent upon you to make sure that you do nothing ‘bad’ inside of a transaction, so now you have to make sure that you do nothing bad even in the face of incoherent state; this is actually an extremely programmer-hostile interface. Whereas with an opaque tm, you only ever have to think about nice, coherent states. At least, that’s the folklore.
The problem is—opacity costs; a tm which does not have to provide opacity can scale much better. I get around the problem by making a cl-to-cl compiler which, when you do something bad, checks if the state was incoherent; if it was, then it simply restarts the transaction; otherwise, it signals an error. Hence: fundamentally safe and scalable.
If cl treated conditions as effects and used them to implement all side effects, then that would almost suffice—almost, but not quite. Because nontermination is also a kind of effect; if you get into an infinite loop because you observed an incoherent state (where you wouldn’t have entered an infinite loop had you seen only coherent states), then I have to handle that too, but an infinite loop may never do any side effects. Obviously I can’t prove whether something is an infinite loop or not. But I can instrument the generated code to periodically check (at exponentially expanding intervals, to maintain the right asymptotics) whether the state it observed is coherent, and restart if not.
That’s interesting, and models something similar in vibes to the smash product of two join semattices!
If we think of Option(bool) as a join semilattice, none is the bottom, and just true, just false sit above the bottom in the Hasse diagram.
What this construction lets one do is to “collapse” the two bottom elements of none and just(none), which is honestly quite neat!
If we think of these as haskell functions, then:
Now we see that the results of forcing these computations are:
So this type of behaviour is useful when modelling call by (push) value!
I disagree with this explanation. I think the correct explanation should at least try to convey the notion of “how a tensor transforms”, to go with the somewhat meme definition of “a tensor is something that transforms like a tensor”. To put my money where my mouth is, here is my shot at an explanation that tries to explain the “invariance principle” of tensors and “how coordinates transform” by using “memory location” as my coordinate system.
Suppose I implement a double ended queue using two pointers:
See that the state of the queue is technically three numbers,
{ memory, start, end }(Pointers are just numbers after all). But this is coordinate dependent, asstartandendare relative to the location ofmemory. Now suppose I have a procedure to reallocate the queue size:Notice that when I do this, the values of
startandendcan be completely different!However, see that the length of the queue, given by
(end - start)is invariant: It hasn’t changed!In the exact same way, a “tensor” is a collection of numbers that describes something physical with respect to a particular coordinate system (the pointers
startandendwith respect to thememorycoordinate system). “tensor calculus” is a bunch of rules that tell you how the numbers change when one changes coordinate systems (ie, how the pointersstartandendchange when the pointermemorychanges). Some quantities that are computed from tensors are “physical”, like the length of the queue, as they are invariant under transformations.Tensor calculus gives a principled way to make sure that the final answers we calculate are “invariant” / “physical” / “real”. The actual locations of
startandenddon’t matter, as(end - start)will always be the length of the list!Physicists (and people who write memory allocators) need such elaborate tracking, to keep track of what is “real” and what is “coordinate dependent”, since a lot of physics involves crazy coordinate systems (https://en.wikipedia.org/wiki/Schwarzschild_metric#History), and having ways to know what things are real and what are artefacts of one’s coordinate system is invaluable. For a real example, consider the case of singularities of the Schwarzschild solution to GR, where we initially thought there were two singularities, but it later turned out there was only one “real” singularity, and the other singularity was due to a poor choice of coordinate system:
IMO this is so great that it needs a web page of its own somewhere. Maybe you’d like to add it to https://pixel-druid.com/articles/tensor-is-a-thing-that-transforms-like-a-tensor.html !
I think this bumps up against a problem with jargon: Physicists, in particular, say “tensor” when mathematicians say “tensor field”. Saying “a tensor is a thing that transforms like a tensor” makes some kind of sense when talking about tensor fields, as those live on a manifold and have to transform the correct way when we change coordinates on the manifold. As you point out, encoding these transformations is incredibly valuable when doing calculations, to the point that modern mathematicians will say that something is “geometric” if it can be expressed as a tensor field and don’t like to consider any other kind of object.
A “tensor field” is made up of “tensors” that vary from point to point. A “tensor” is something we made up to linearize multilinear maps of vectors: Given a vector space
Vover a fieldkand a mapb : V x V -> kthat is linear in each variable separately, there exists a vector spaceV o V(the tensor product ofVwith itself) along with a bilinear mapV x V -> V o Vand a linear mapf : V o V -> ksuch that the compositionV x V -> V o V -> kequalsb. The upshot is that instead of having to deal with a bilinear mapb, we can deal with a linear onef.The latter kind, the standard mathematical linear algebra object, is what “tensors” in computer science are. There are no transformations or invariance under them going on. As the original post points out, it is valuable to consider “tensors” not only as multidimensional matrices, but as those plus some operations, but those operations are not the coordinate transformations of tensor fields.
In short, the physicists are to blame.
I agree, and to add some clarification:
In mathematics, a tensor is the multilinear linear map itself, not the grid of numbers that is isomorphic to the multilinear map upon choosing bases. This is literally why we need tensors, a map
V x V -> Fand a mapV x V* -> Fcould have the same matrix under a choice of basis, but be entirely different linear maps, and will transform differently when the basis changes! This is not what is used in computer science, where we conflate the “grid of numbers” with the “linear map” in itself.This is a great high-level explanation that gets across the fact that tensors aren’t merely n-dimensional arrays and why, and it makes me wonder what an explanation targeted at someone with a decent linear algebra background would look like. When I first really started learning what tensors are, I had a good grasp on vector spaces and an okayish grasp on dual spaces and I didn’t really feel like tensors clicked for me until I saw them expressed in the formulation of a tensor product of some number of vectors and covectors, but it took a longer duration of me feeling like I just wasn’t getting the concept than feels necessary in retrospect before the intuition hit me. Maybe that’s just how it has to go, but I retain this suspicion that a 3blue1brown-style exposition of tensors is possible, in the sense of there being a detailed explanation of them that of course doesn’t substitute for actually doing math but would serve as a really great intuitive framework with which to approach the subject in a more in-depth way. It’s something I’d like to take a crack at some day, but it seems like a non-trivial project and I’m certainly not lacking for those already.
Close, but one must also discuss contra-variance :
Let’s start with the view that a tensor is really a transformation of the coordinate axes between two spaces A and B.
In your queue example, the transformation is a linear translation (the memory offset), and the two spaces are really the same, our memory. What if our transformation were a rescaling of the axis, e.g. changing representation from bytes to bits?
Then you would see that memory offsets are contravariant wrt this transformation: an offset of
nbytes becomes an offset of8 nbits, while our “reference” (bits vs bytes) has shrunk by a factor 8.In full generality, a tensor is a transformation of coordinate frames that has both co- and contra-variant indices.
Work: Waiting for PLDI reviews for two of our papers, and preparing responses and polished code in anticipation.
We’re also organizing a compiler social at the Cambridge, so anyone interested in compilers / formal verification / hardware, please do drop by! (https://grosser.science/compiler-social-24-feb/)
Feel invited to drop by even if you have a passing interest in the topics. My research group has just moved to cambridge, and we have a culture of hosting these events to hang out with folks in the area where we are based ^_^
I personally will be very happy to hang out and chat about anything maths and proofs!
I really want to attend, it’s a shame it was scheduled for the same day as State of Open Con. Next time…
Does anyone have any other resources for how these things work? I found this years ago when trying to figure out how Coq’s termination checker works, but this one is pretty simple. I think I’ll try reimplementing it this week
Yes, here is a reference for the isabelle termination checker: Finding Lexicographic orders for Termination Proofs in Isabelle/HOL (https://www21.in.tum.de/~krauss/papers/lexicographic-orders.pdf)
Recall that Coq is more complex, as the kernel has various heuristics for how pattern matches on inductives ought to decrease. In particular, the term “coq guard condition” brings up the relevant literature. Unfortunately, I don’t know of a pedagogical reference, and would very much love to know one!
This is an area I’m very keen on learning better (PhD student here), so I’d love to know more references!
Yeah, the pedagogical value of this paper is why I like it, despite the silly name. It’s super clearly written and makes sense to me.
Buying cutlery for my new home in cambridge! Suggestions for places with nice, pre-owned cutlery welcome!
Other than that, continuing to hack on my Lean “IDE” (more like minimal LSP stress test): https://github.com/bollu/elide
I’ve also been thinking about crocheting as a stack based language, and it’s quite interesting! I think it even has a type system which tracks the number of loops, and the consumption of loop resources (forward versus backward loops). I might eventually write a small thing up for SIGBOVIK if this turns out to be fun enough.
There is a little cluster of charity shops on Burleigh St near the Grafton shopping centre. It’s also worth taking a look along Mill Road where many of the more interesting shops are. (I was about to suggest Cutlack’s, but sadly they seem to have moved to Ely.)
Super, thanks a lot for the recomendation! By the way, I’d love to grab a cofee/pint this week :) Would you be available on thursday/friday?