tel

Genuine question, how does SPIR-V compare with CUDA? Why is SPIR-V in a trench coat less desirable? What is it about Metal that makes it SPIR-V in a trench coat (assuming that's what you meant)?

At the same time, if you want to use Claude to read the source and narrate how it works to you that’s trivial to do as a user.

If you're familiar with Zorn's Lemma, the construction is just to order bases by inclusion and to consider chains created by noting that there must be an independent dimension and adding it inductively. You can upper bound each of these chains by unioning the members of the chain (which preserves linear independence). By Zorn's Lemma that means there is a maximal linearly independent system and if an element existed outside of that system's span it would contradict that maximality.

Yeah, that's correct. You also often see it as having that for any method `X -> T<Y>` there's a corresponding method `T<X> -> T<Y>`. Or you can have that for any two arrows `X -> T<Y>` and `Y -> T<Z>` there's a composed arrow `X -> T<Z>`. All are equivalent.

Every monad is also an applicative and liftA2 does/is the same thing as liftM2. The only reason they both exist was due to Monad being popularized in Haskell earlier than Applicative and thus not having it as a superclass until the Functor-Applicative-Monad Proposal in Haskell 2014. It was obviously correct, but a major breaking change that also got pork barreled a bit and so took a while to land.

Monad tutorials are on the rise again.

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.

The more constrained your theory is, the fewer models you have of it and also the more structure you can exploit.

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’m not a huge fan of these, but this time I noticed that the best ones feel a lot like naturality arguments. As in, moving structural bits in a way that makes it clear that we’re not touching anything that ought to be universally quantifiable.

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!

Often it's easy to construct a family of sets representing something of interest. For example, we like to define integration initially as a finite process of breaking the integrand's domain into pieces, computing their area, and summing.

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...)

The quantification over T is still kind of weird, though. In a formulation like `for all T, (T and P consistent and T and neg P consistent)` is trivially false, just take `T = {neg P}` and now `{P, neg P}` is inconsistent.

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

Yeah, I agree. "Independence" is fundamentally a property of the formal system you're working within (or really, it's a property of the system you're using and of the axiomatic system under test, the system a proposition would be independent from). I'm holding out a bit to unify that with "undecidability" because undecidability takes on a particular character in constructive systems that happens to align with Turing's notion.

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".

Quantifying over T is probably not going to work. In informal terms that reads like "No logic exists where P is independent", which probably wasn't quite what you wanted, but also we can trivially disprove that with T = {}. As long as P is self-consistent, then "not P" should be too.

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

Independent and undecidable aren't quite the same, even in formal logic. Or rather, sometimes they are but it’s worth being specific.

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.

I really like TAPL but would recommend Harper’s Practical Foundations of Programming Languages (PFPL) first (though skip the first 2 chapters I think?).

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.

Sorry, Haskell’s “monad transformer library”. One of the earliest approaches to composability of multiple monadic effects. It’s pretty similar to an algebraic effect system allowing you to write effectual computations with types like `(Error m, Nondet m, WithState App m) => m ()` to indicate a computation that returns nothing but must be executed with access to error handling, nondeterminism, and access to the App type as state.

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).

They're pretty similar, but with different ergonomics. Algebraic effects are similar to some kind of "free" monad technique, but built in. For being built in they have nicer syntax and better composability, often. You can achieve the same in a language suitably dedicated to monadic approaches (Haskell being the poster child here) but it helps to have type class inference (giving you mtl-like composability) and built-in bind syntax a la Haskell's `do` or Scala's `for`.

I would also always use that in a mathematical context but feel it’s weird to hear, say, “proved in a court of law”.

Looking around, here's a post by the author on Twitter where he shows similar motion and states that the time-lapse is 10m at 1min/sec.

https://x.com/mag2art/status/1385940103189745669

I think that's right. At some level, any anticipation of a future state has to be measurable in some kind of confidence level.

I suppose where I get lost is that, at least subjectively, I end up treating different anticipated return distributions differently. I want a mixture of risks, both in terms of their covariance and the absolute properties.

When I think of "speculation", I am intentionally shaping only a small portion of my personal portfolio toward high risk, high reward activities. And I only really feel comfortable doing that because a larger fraction of my personal risk is in safer vehicles.

Atop that, I also think a lot about liquidity time bounds. I want access to a reasonable amount of highly-liquid, low-risk investments. I need that flexibility to be safe in the event that I need to buy something.

To my eye at least, I qualitatively differentiate between speculative investments and these liquid/low risk ones. If I felt I only had one kind of risk, I would seek out the other in some proportion.

Yeah, that’s true. We invest in a lot of things, hoping for future value. But I guess I still treat those differently. I only hold enough USD for upcoming purchases. And I struggle to understand how investing in my marriage is speculative. For a variety of reasons I can’t (or wouldn’t want to) manage that risk like I would in normal speculative investment. I can’t hedge, size up, size down.

So I think I’m missing something. I feel like you’re suggesting that we should be more comfortable speculating because we do it all the time, but I’m not seeing how those are all the same.

Reading a bit about it from the Flo paper

- Describe a dataflow graph just like Timely - Comes from a more "semantic dataflow" kind of heritage (frp, composition, flow-of-flows, algebraic operators, proof-oriented) as opposed to the more operationally minded background of Timely - Has a (very) different notion of "progress" than Timely, focused instead of ensuring the compositions are generative in light of potentially unbounded streaming inputs - In fact, Flo doesn't really have any notion of "timeliness", no timestamping at all - Supports nested looping like Timely, though via a very different mechanism. The basic algebra is extremely non-cyclic, but the nested streams/graphs formalism allows for iteration.

The paper also makes a direct comparison with DBSP, which as I understand it, is also part of the Timely/Naiad heritage. Similar to Timely, the authors suggest that Flo could be a unifying semantic framework for several other similar systems (Flink, LVars, DBSP).

So I'd say that the authors of Flo are aware of Naiad/Timely and took inspiration of nested iterative graphs, but little else.

It’s been a minute since I used my mlua integration. I recall more packaging difficulty, investigating LuaJIT and Luau for a while. I had to make more decisions around my API, whether it was OO or a package, what libraries to allow. When introducing my domain types, there were more ways to fail and more subtle documentation to read and grok.

Nothing was hard, but Rhai was easier.

If I were to write a system in my embedded trading strategy language, if I cared about extensibility and composition, maybe Lua’s complexity would begin to pay its way. But I’m not, I just want simple, hot-reloadable logic to drive some fast Rust code.

I’m already writing a Rust system. I’ve tried integrating with mlua. It works, but Rhai is simpler to embed. Simpler to build.

(I also tried Piccolo which is very cool but also not simple.)

Rhai also doesn’t include a lot of complexity that Lua does. It encourages you to write extension types in Rust, which is what I want.

Rhai doesn’t have GC, just refcounts. Rhai also can disable a lot of features, say if you just want an expression language.

I use it to write trading logic. I like that it’s stripped down and simple.

A function from a fixed input is a monad (called the “Reader” monad). If you constrain all IO to happen underneath that function then it will be deferred until you evaluate the result.

In those senses, these are the same. You can emulate the IO monad in this way.

Haskell provides guarantees that make this stronger. There is no way to perform IO-like side effects except via the IO monad. And no way to “evaluate” the IO monad except to declare it as your main entry point, compile, and hit play.

(Except unsafePerformIO, of course, the highly discouraged escape hatch).

These restrictions are actually what makes the use of the IO monad powerful. As you show, it’s easy to “add” it to a language, and also almost valueless. The value is in removing everything that’s not in the IO monad.

Generally, when we construct models we do so by defining what probability they give to the data. That's a function that takes in your data set and returns some number, the higher the better.

Technically, these functions need to satisfy a bunch of properties, but those properties matter mostly for people doing the business of building and comparing models. If you just have a model someone already made for you, then "the higher the better" is good enough.

It's also the case that these models have "parameters". As a simple example, the model of a coin flip takes in "heads" or "tails" and returns a number. The higher that number, the more probable it claims that outcome to be. When we construct that model, we also choose the "fairness" parameter, usually setting it so that both heads and tails are equally likely.

So really, it's a function both of the data and of its parameters.

Now, "maximum likelihood estimation" (MLE) is just the method where you fix the data inputs to the model to whatever your training data is and then find the parameter inputs that maximize its output. This kind of inverts the normal mechanism where you pick the parameters and then see how probable the data was.

Presumptively, whatever parameterization of your model makes the data the most likely is the parameterization that best represents your data. That doesn't have to be true, and often is only approximately true, but that presumption is exactly what makes MLE popular.

Finally, it's worth describing the origin of the name. When we look at our model after fixing the data inputs and consider it a function of its parameters instead we call that function a "likelihood". This is just another name for "probability" except it's used to emphasize that likelihoods don't meet all the technical properties I skipped up above. So "maximum likelihood estimation" is just the process of estimating the parameters of your model by maximizing the likelihood.

Just my lack of experience here, but I'm trying to verify I'm successfully using sold. The mold linker claims it leaves metadata in the .comment section, but on mach-o does that exist? Is there a similar evaluation command using objdump as the mold readelf command?

So you're looking for a way for a future to make use of temporary access to state just while being polled? The issue being that since a future captures references in self you can't have multiple futures able to reference the same data via a &mut pointer. Instead you need to use Rc.

If I'm understanding, then I don't yet follow the use case. You want to have multiple actors reading from the same message queue? Or different concurrent chunks inside of the actor?

This feels to me to strain against the actor design pattern a lot. I feel this often, that futures are somewhat in tension with actors. There are too many options.

What is a first-class resume argument? How does it enable &mut State and non-sequential messaging within Rust's current futures design?

It's clear that there's some beginning of this in place. They reference it as initial in the docs there and it's missing quite a bit. I'm not a huge fan of what I'm seeing here where each actor is implicitly itself and a supervisor (i.e., ActorRef makes reference to the actor's children). I think I saw that first in Akka and while it makes sense in theory, I don't like the practice.

To me, your supervision tree should be dedicated to that purpose and forms a superstructure relating entirely to spawning, resource provisioning, restarting, shutdown. Part of what makes it nice in Erlang is that it's consistent and thoughtless, just part of designing your system instead of being behavior you have to write or worry about much.

Here with Ractor they've built a special monitoring channel and callbacks into Actor (`handle_supervisor_evt`). This implies at some point one might write a nice supervisor in their framework that hopefully has some of those properties.

I'm always most curious with these frameworks how they're considering supervision. That's the real superpower of OTP, especially over Rust.

To me, Rust has adequate concurrency tooling to make ad hoc actor designs roughly on par with more developed ones for many tasks, but supervision is both highly valuable and non-trivial. Briefly, I'd say Rust is top-notch for lower-level concurrency primitives but lacks architectural guidance. Supervisor trees are a great choice here for many applications.

I've tried implementing supervision a few times and the design is both subtle and easy to get wrong. Even emulating OTP, if you go that route, requires exploring lots of quiet corner cases that they handle. Reifying this all into a typed language is an additional challenge.

I've found myself tending toward one_for_all strategies. A reusable Fn that takes some kind of supervisor context and builds a set of children, potentially recursively building the supervision tree beneath, tends to be the best design for typed channels. It forces one_for_all however as it's a monolithic restart function. You can achieve limited (batch-y) rest_for_one by having the last thing you boot in your one_for_all be another one_for_all supervisor, but this feels a little hacky and painful and pushes back against more granular rest_for_one designs.

You then probably want a specialized supervisor for one_for_one, similar to Elixir's DynamicSupervisor.