https://www.realsenseai.com/products/real-sense-depth-camera...

That said, I don't think splats:voxels as pixels:vector graphics. Maybe a closer analogy would be pixels:vectors is the same as voxels:3d mesh modeling. You might imagine a sophisticated animated character being created and then animated using motion capture techniques.

But notice where these things fall apart, too. SVG shines when it's not just estimating the true form, but literally is it (fonts, simplified graphics made from simple strokes). If you try to estimate a photo using SVG it tends to get messy. Similar problems arise when reconstructing a 3d mesh from real-world data.

I agree that splats are a bit like pixels, though. They're samples of color and light in 3d (2d) space. They represent the source more faithfully when they're more densely sampled.

The difference is that a splat is sampled irregularly, just where it's needed within the scene. That makes it more efficient at representing most useful 3d scenes (i.e., ones where there are a few subjects and objects in mostly empty space). It just uses data where that data has an impact.

For example, the camera orbits around the performers in this music video are difficult to imagine in real space. Even if you could pull it off using robotic motion control arms, it would require that the entire choreography is fixed in place before filming. This video clearly takes advantage of being able to direct whatever camera motion the artist wanted in the 3d virtual space of the final composed scene.

To do this, the representation needs to estimate the radiance field, i.e. the amount and color of light visible at every point in your 3d volume, viewed from every angle. It's not possible to do this at high resolution by breaking that space up into voxels, those scale badly, O(n^3). You could attempt to guess at some mesh geometry and paint textures on to it compatible with the camera views, but that's difficult to automate.

Gaussian splatting estimates these radiance fields by assuming that the radiance is build from millions of fuzzy, colored balls positioned, stretched, and rotated in space. These are the Gaussian splats.

Once you have that representation, constructing a novel camera angle is as simple as positioning and angling your virtual camera and then recording the colors and positions of all the splats that are visible.

It turns out that this approach is pretty amenable to techniques similar to modern deep learning. You basically train the positions/shapes/rotations of the splats via gradient descent. It's mostly been explored in research labs but lately production-oriented tools have been built for popular 3d motion graphics tools like Houdini, making it more available.

And yeah, I agree. Practically, it's the thing that annoys me the most day-to-day. I've mostly got wrapping set up to handle it now, but it remains a little finicky.

It has no inline formatting, only 3 levels of ATX headers (without trailing #s), one level of bullet points using only asterisk and not dash to delimit, does not merge touching non-whitespace lines (thus expecting one line per paragraph), and supports only triple-backtick fenced preformatted text areas that just flip on and off.

Maybe the biggest change is that links are necessarily listed on their own line, proceeded by a `=>` and optionally followed by alt-text.

My gemtext parser is maybe 70 lines and it is arguably 95% of what one needs from Markdown.

Let's start with function composition. We know that for any two types A and B we can consider functions from A to B, written A -> B. We can also compose them, the heart of sequentiality. If f: A -> B and g: B -> C then we might write (f;g) or (g . f) as two different, equivalent syntaxes for doing one thing and then the other, f and then g.

I'll posit this is an extremely fundamental idea of "sequence". Sure something like [a, b, c] is also a sequence, but (f;g) really shows us the idea of piping, of one operation following the first. This is because of how composition is only defined for things with compatible input and output types. It's a little implicit promise that we're feeding the output of f into g, not just putting them side-by-side on the shelf to admire.

Anyway, we characterize composition in two ways. First, we want to be clear that composition only cares about the order that the pipes are plugged together, not how you assemble them. Specifically, for three functions, f: A->B, g: B->C, h: C->D, (f;g);h = f;(g;h). The parentheses don't matter.

Second, we know that for any type A there's the "do nothing" identity function id_A: A->A. This doesn't have to exist, but it does and it's useful. It helps us characterize composition again by saying that f;id = id;f = f. If you're playing along by metaphor to lists, id is the empty list.

Together, composition and identity and the rules of associativity (parentheses don't matter) and how we can omit identity really serve to show what the idea of "sequences of pipes" mean. This is a super popular structure (technically, a category) and whenever you see it you can get a large intuition that some kind of sequencing might be happening.

Now, let's consider a slightly different sort of function. Given any type types, what about the functions A -> F B for some fixed other type F. F here exists to somehow "modulate" B, annotate it with additional meaning. Having a value of F B is kind of like having a value of type B, but maybe seen through some kind of lens.

Presumably, we care about that particular sort of lens and you can go look up dozens of useful choices of F later, but for now we can just focus on how functions A -> F B sort of still look like little machines that we might want to pipe together. Maybe we'd like there to be composition and identity here as well.

It should be obvious that we can't use identity or composition from normal function spaces. They don't type-check (id_A: A -> A, not A -> F A) and they don't semantically make sense (we don't offhand have a way to get Bs out of an F B, which would be the obvious way to "pipe" the result onward in composition).

But let's say that for some type constructors F, they did make sense. We'd have for any type A a function pure_A: A -> F A as well as a kind of composition such that f: A -> F B and g: B -> F C become f >=> g : A -> F C. These operations might only exist for some kinds of F, but whenever they do exist we'd again capture this very primal form of sequencing that we had with functions above.

We'd again capture the idea of little A -> F B machines which can be plugged into one another as long as their input and output types align and built into larger and larger sequences of piped machines. It's a very pleasant kind of structure, easy to work with.

And those F which support these operations (and follow the associativity and identity rules) are exactly the things we call monads. They're type constructors which allow for sequential piping very similar to how we can compose normal functions.

Monads, I think, offer enough structure in that we can exploit things like monad composition (as fraught as it is), monadic do/for syntax, and abstracting out "traversals" (over data structures most concretely, but also other sorts of traversals) with monadic accumulators.

There's at least one other practical advantage as well, that of "chunking".

A chess master is more capable of quickly memorizing realistic board states than an amateur (and equally good at memorizing randomized board states). When we have a grasp of relevant, powerful structures underlying our world, we can "chunk" along them to reason more quickly. People familiar with monads often can hand-wave a set of unknowns in a problem by recognizing it to be a monad-shaped problem that can be independently solved later.

I still don’t love this sort of thing being presented as “proof”, but I thought that idea is interesting. Is there a way to formalize naturality into technical diagrams? Probably!

To compute the contribution of some piece indexed i, we measure the size of its domain, call it the area Ai, and then evaluate the integrand, f, at some point xi within that domain, then the contribution is Ai * f(xi).

Summing all of these across i produces a finite approximation of the integral. Then we take a limit on this process, breaking the domain into larger and larger families of sets with smaller and smaller areas. At the limit, we have the integral.

This process seems intuitive, but it contains an application of the axiom of choice---in the limit, we have an infinite number of subsets of our domain and we still have to pick a representative xi for each one to evaluate the integrand at.

It's quite obvious how to pick an arbitrary representative from each set in a finite family of sets: you just go through one-by-one picking an element.

But this argument breaks down for an infinite family. Going one-by-one will never complete. We need to be able to select these representative xis "all at once". And the Axiom of Choice asserts that this is possible.

(Note: I'm being fast-and-loose, but the nature of the argument is correct. This doesn't prove integration demands AoC or anything like that, just shows how this one sketch of an argument would. Specifically, integration normally avoids AoC because we can constructively specify our choice function - for example, picking the lexicographically smallest point within each axis-aligned rectangular cell. Generalize to something like Monte Carlo integration, however...)

We're never trying to show P is independent of all theories, just some specific one.

So at some level, this was just an acknowledgement that "undecidability" in this form is well represented in formal logic. In that sense, at least in constructive logics, it's not just a synonym for "independence".

We're interested in a proposition's status with respect to some theory that we enjoy (i.e. Zermelo–Fraenkel set theory).

A proposition P being independent of a theory T means that both (T and P) and (T and not P) are consistent. T has nothing to say about P. This may very well be what Gödel was indicating in his paper.

On the other hand, undecidable has a sharper meaning in computation contexts as well as constructive logics without excluded middle. In these cases we can comprehend the “reachability” of propositions. A proposition is not true or false, but may instead be “constructively true”, “constructively false”, or “undecidable”.

So in a formal logic without excluded middle we have a new, more specific way of discussing undecidability. And this turns out to correspond to the computation idea, too.

https://www.cs.cmu.edu/~rwh/pfpl.html

It’s far more directed than TAPL, so I think it’s easier to read from start to finish. TAPL feels better as a reference.

There are a few drawbacks to it, but it is a pretty simple way to get 80% of the ergonomics of algebraic effects (in Haskell).