The point of effect systems isn't to stratify the behaviour of the operating system (it's the Wild West out there). It's to stratify the behaviour of your program. A function that has a DB effect isn't telling you that it will make Postgres queries (which can do anything!), it's telling you that it wants to make DB queries so you need to pass it a handler of a certain form to let it do that, hexagonal architecture style.
But you can also stratify in the other direction. ‘Pure’ functions aren't real outside of mathematics: every function can have side effects like allocating memory, possibly not terminating, internal (‘benevolent’) mutation, et cetera. When we talk about ‘pure’ functions we usually mean that they have only a particular set of effects that the language designer considered ‘safe enough’, where ‘enough’ is usually defined with reference to the ergonomic impact of making that effect explicit. Algebraic effects make effects (and importantly effect composition — we got here in the first place because we were fed up of monad transformers) more ergonomic to use, which means you can make more effects explicit without annoying your users.
As far as I know the shiniest implementations in the effect typing world at the moment are Koka and Effekt, which are both languages in their own right. They each have their own ideas about implementation to make effects (mostly) zero-cost.
Arguably an effect monad is an EDSL that has algebraic effects :)
But the things these languages are experimenting with are low-level implementation details that wouldn't be amenable to embedding. There's no escaping the Haskell GC.
Atom [1] is an EDSL that escaped Haskell GC. Note that Atom takes ideas from Bluespec which compiles to hardware circuits, where GC is not availble.
[1] https://hackage.haskell.org/package/atom
One can make a Haskell EDSL with effects and everything and output a C (or some compiler's IR) code.
These languages you mentioned repeat Rust's mistake.
Rust's type system includes rules that remove definitions from the scope/environment. This is inherent and obligatory for uniqueness/linear types type systems.
At the time Rust was conceived, Haskell had HList library [2] and Beyond Monads [3] extended state monad. Combining both would embed into Haskell most, if not all, Rust at the time, allowing to pursue research of how to combine borrow logic with algebraic effects. But Rust's developers preferred to go OCaml implementation (syntax first) way and not to pursue complexity issues of semantics.
> Another limitation of programming languages is that they are poor abstraction tools
> Programming languages are implementation tools for instructing machines, not thinking tools for expressing ideas
Machine code is an implementation tool for instructing machines (and even then there's a discussion to be had about designing machines with instruction sets that map more neatly to the problems we want to solve with them). Everything we've built on top of that, from assembly on up, is an attempt to bridge the gap from ‘thinking tools for expressing ideas’.
The holy grail of programming languages is a language that seamlessly supports expressing algorithms at any level of abstraction, including or omitting lower-level details as necessary. Are we there yet? Definitely not. But to give up on the entire problem and declare that programming languages are inherently unsuitable for idea expression is really throwing the baby out with the bathwater.
As others in the comments have noted, it's a popular and successful approach to programming today to just start writing code and seeing where the nice structure emerges. The feasibility of that approach is entirely thanks to the increasing ability of programming languages to support top-down programming. If you look at programming practice in the past, when the available implementation languages were much lower-level, software engineering was dominated by high-level algorithm design tools like flowcharts, DRAKON, Nassi–Shneiderman diagrams, or UML, which were then painstakingly compiled by hand (in what was considered purely menial work, especially in the earlier days) into computer instructions. Our modern programming languages, even the ‘low-level’ ones, are already capable of higher levels of abstraction than the ‘high-level’ algorithm design tools of the '50s.
In addition to the other comments here, note that in PL circles ‘syntax’ typically denotes _everything_ that happens before translation/execution, importantly including type checking. ‘Semantics’ is then about explaining what happens when the program is run, which can equivalently be described as deciding when two programs are equal, mapping programs to mathematical objects (whose ‘meaning’, or at least equality, is considered to be well understood), specifying a set of transformations the syntax goes through, et cetera.
In pure functional languages saying what value an expression will evaluate to (equivalently, explaining the program as a function of its inputs) is a sufficient explanation of the meaning of a program, and semantics for these languages is roughly considered to be ‘solved’. Open areas of study in semantics tend to be more about doing the same thing for languages that have more complicated effects when run, like imperative state update or non-local control (exceptions, async, concurrency).
There's some overlap in study: typically syntax is trying to reflect semantics in some way, by proving that programs accepted by the syntactic analysis will behave or not behave a certain way when run. E.G. Rust's borrow checker is a syntactic check that the program under scrutiny will not dereference an invalid pointer, even though that's a thing that is possible by Rust's runtime semantics. Compare to Java, which has no syntactic check for this because dereferencing invalid pointers is simply impossible according to the semantics of the JVM.
The ‘three tribes of programming’ [1] strike again!
This thread is full of claims that ‘programming is really engineering’ (in accordance with the article), ‘programming is really building’, or ‘programming is really philosophy/mathematics’. They're all true!
It's not that one of them is the True Nature of software and anyone doing the others is doing it wrong or at a lower level. These are three different things that it is completely reasonable to want to do with software, and each of them can be done to an amateur or expert level. But only one of them is amenable to scientific analysis. (The other two are amenable to market testing and formal proof, respectively.)
On second thought the tribal testing framework here is a bit simplistic, and there's some cross-tribe pollination, to varying levels of success.
The ‘maker’ tribe also tests with HCI assessments like GOMS and other methods from the ‘soft’ sciences like psychology and sociology, not just economics/business science.
Model-checking and complexity proofs (and complexity type systems) are mathematical attempts to apply mathematician-programmer methods to engineer-programmer properties.
Cyclomatic complexity is an attempt to measure mathematician-programmer properties using engineer-programmer methods.
When Kubernetes exposed its APIs as declarative configuration objects, I get the impression that they didn't originally mean for people to write the configuration by hand. The YAML/JSON/… is a conveniently universal interchange format for interfacing with Kubernetes from bindings, and representing target state as documents is just a good way to encode idempotence in the API.
I'd be interested to hear from someone involved with early Borg/K8s development what the original intention was.
One of the big promises of HTMX is that the client doesn't have to understand the structure of the returned data since it's pre-compiled to the presentation layer, and it feels like this violates that quite heavily since now the calling page needs to know the IDs and semantics of the different elements the server will return.
This isn't really a criticism of Datastar, though: I think the popularity of OOB in HTMX indicates that the pure form of this is too idealistic for a lot of real-world cases. But it would be nice if we could come up with a design that gives the best of both worlds.
That doesn't seem to be the ‘standard’ way to use Datastar, at least as described in this article?
If one were to rerender the entire page every time, what's the advantage of any of these frameworks over just redirecting to another page (as form submissions do by default)?
It's the high performance way to use Datastar and personally I think it's the best DX.
1. It's much better in terms of compression and latency. As with brotli/zstd you get compression over the entire duration of the connection. So you keep one connection open and push all updates down it. All requests return 204 response. Because everything comes down the same connection brotli/zstd can give you 1000-8000x compression ratios. So in my demos for example, one check is 13-20bytes over the wire even though it's 140k of HTML uncompressed. Keeping the packet size around 1k or less is great for latency. Redirect also has to do more trips.
2. The server is in control. I can batch updates. The reason these demo's easily survive HN is because the updates are batched every 100ms. That means at most a new view gets pushed to you every 100ms, regardless of the number of users interacting with your view. In the case of the GoL demo the render is actually shared between all users, so it's only rendering once per 100ms regardless of the number of concurrent users.
3. The DX is nice and simple good old View = f (state), like react just over the network.
So even though HTTP/2 multiplexes each request over a single TCP connection, each HTTP connection is still compressed separately. Same with keep alive.
The magic is brotli/zstd are very good at streaming compression thanks to forward/backward references. What this effectively means is the client and the server share a compression window for the duration of the HTTP connection. So rather than each message being compressed separately with a new context, each message is compressed with the context of all the messages sent before it.
What this means in practice is if you are sending 140kb of divs on each frame, but only one div changed between frames, then the next frame will only be 13bytes because the compression algorithm basically says to the client "you know that message I sent you 100ms ago, well this one is almost identical apart from this one change". It's like a really performant byte level diffing algorithm, except you as the programmer don't have to think about it. You just re-render the whole frame and let compression do the rest.
In these demos I push a frame to every connected client when something changes at most every 100ms. What that means, it effectively all the changes that happen in that time are batched into a single frame. Also means the server can stay in charge and control the flow of data (including back pressure, if it's under to much load, or the client is struggling to render frames).
Category theory is popular in computer science because, at a fundamental level, they're very compatible ways of seeing the world.
In computing, we think about:
- a set of states
- with transformations between them
- including a ‘do nothing’ transformation
- that can be composed associatively (a sequence of statements `{a; b;}; c` transforms the state in the same way as a sequence of statements `a; {b; c;}`)
- but only in certain ways: some states are unreachable from other states
This is exactly the sort of thing category theory studies, so there's a lot of cross-pollination between the disciplines. Computation defines interesting properties of certain categories like ‘computation’ or ‘polynomial efficiency’ that can help category theorists track down interesting beasts to study in category theory and other branches of mathematics that have their own relationships to category theory. Meanwhile, category theory can give suggestions to computer science both about what sort of things the states and transformations can mean and also what the consequences are of defining them in different ways, i.e. how we can capture more expressive power or efficiency without straying too far from the comfort of our ‘do this then do that’ mental model.
This latter is really helpful in computer science, especially in programming language or API design, because in general it's a really hard problem to say, given a particular set of basic building blocks, what properties they'll have when combined in all the possible ways. Results in category theory usually look like that: given a set of building blocks of a particular form, you will always be able to compose them in such a way that the result has a desired property; or, no matter how they're combined, the result will never have a particular undesired property.
As an aside, it's common in a certain computer science subculture (mostly the one that likes category theory) to talk about computing in the language of typed functional programming, but if you don't already have a deep understanding of how functional programming represents computation this can hide the forest behind the trees: when a functional programmer says ‘type’ or ‘typing context’ you can think about sets of potential (sub)states of the computer.
> - with transformations between them
>
> - including a ‘do nothing’ transformation
>
> - that can be composed associatively (a sequence of statements `{a; b;}; c` transforms the state in the same way as a sequence of statements `a; {b; c;}`)
And this right here is that monoid in the famous "A monad is just a monoid in the category of endofunctors" meme.
Still, what's in your opinion, the advantage of thinking in category theory rather than set theory? (For programming, not - algebraic geometry.)
I mean, all examples I heard can be directly treated with groups, monoids, and regular functions.
I know some abstract concepts that can be defined in a nice way with CT but not nearly as easy - set theory, e.g. (abstract) tensor product. Yet, for other concepts, including quantum mechanics, I have found that there is "abstract overhead" of CT with little added value.
In my opinion, the important advantage of category theory over set theory in (some!) computational contexts is that it allows you to generalize more easily. Generalizing from sets and functions to objects and morphisms lets you play around with instantiating those objects and morphisms with a variety of different beasts while maintaining the structure you've built up on top of them, and you can even use it to modularly build towers of functionality by layering one abstraction on top of another, even if you choose later to instantiate one of those layers with good old sets and functions. By contrast, it's hard to imagine treating something like async functions with plain old set theory: while there is of course a way to do it, you'd have to reason about several different layers of abstraction together to get all the way down to sets in one step.
1. COBOL systems are typically written on a much shallower software stack with less room for unreliability
2. banking systems have a ton of effort put into reliability over decades of development.
reply