maxiepoo

Clearly a Kool-aid enjoyer

do you really have 20+ tabs of LLMs open at a time?

Isn't it more differential geometry?

Basically, Evan decided he wanted Elm to be a pre-packaged closed ecosystem where it was easy to develop very simple standalone apps, but made it very difficult to impossible to actually integrate with any existing JavaScript code or libraries. This was a baffling decision to people who thought Elm was supposed to be a practical language.

Blaming everything on "entitlement" from people who bought Elm's marketing about "making functional programming practical" is ridiculous. Thankfully there are now plenty of languages with better type systems than Elm (Rust, OCaml) that deploy to the web just fine.

You can do something like this with OCaml/SML's module system.

And certainly from an abstraction point of view you can do this in any dependently typed language like Idris/Agda/Coq, but these don't have great implementations.

Typed functional languages like Haskell (data)/ML (type) do have a built-in way to define new tree types, and so does Rust (enum). It's one of the biggest things I miss when I'm not using these languages, especially when combined with some metaprogramming (deriving/derive) to get some functions defined for these new types very quickly.

It is very bad that abortion is illegal but thousands of people have not been imprisoned for violating abortion laws afaik.

I'll be surprised if none of the bigger beer companies ends up buying it for the brand and history alone. But maybe it doesn't have as much name recognition as I thought.

It really is remarkable. I think the most remarkable fact about it is that the intensional identity type was invented by Martin Lof in the 70s, the groupoid model was discovered in the 90s and then finally in the late 2000s various people made the connection that Martin Lof's original system from the 70s was in a sense already a type theory for abstract homotopy theory. This led to an explosion of new ideas in type theory (univalence, higher inductive types, modalities) that took a somewhat obscure field of math/cs to the thriving research community it is today.

How can roots be changed without a redo of the universe?

This is a very interesting question and I think reflects a mismatch between how we commonly think about of foundations of mathematics and what role foundations actually play in mathematics. There's no recording online but I recommend looking at the slides to Mike Shulman's talk from JMM 2022 where he discusses this point: http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf . Mike works on, among other things, homotopy type theory, the subject of the original article.

His basic point is that we should think of math more like programs that we can "compile" to various backends. If your math is high level it's not necessarily tied to a particular "architecture" like ZFC.

Even emscripten, which compiles LLVM to WASM has to use a relooper algorithm to get around the lack of jumps.

Austrian economics is truly indistinguishable from parody

This would allow you to do things like compile other assembly languages to webassembly.

One of the main reasons it's not really an assembly language is that it doesn't support jumps! This is fixing a defect!

nonsense trends like an "assembly" language supporting jumps?

WASM is not really an assembly language. Before this, WASM didn't have jump at all, and so tail calls are adding a form of jump (jump with arguments). This makes WASM a much better compilation target.

Basic results that are useful on a day-to-day basis: 1. Yoneda's Lemma, and the corollary that objects defined by universal property are unique up to unique isomorphism 2. Right adjoints preserve limits and more generally, Kan extensions

The "big" theorem of basic category theory is probably the adjoint functor theorems which, once you realize that so many constructions in math are adjoint functors, gives very useful technical conditions to construct such an adjoint (ctrl-s for "applications" here for examples: https://math.stackexchange.com/questions/844131/adjoint-func...).

The most delightful surprising results to me come from categorical logic because that is what I am most familiar with. Here is one: any elementary topos is a model of intuitionistic higher-order logic, and also extensional dependent type theory. This vastly expands the domain of applications of logic if you are used to thinking only in terms of set-theoretic models. It also gives us applications of constructivism that are entirely independent from any philosophical debate about the nature of truth. This means that you can take many mathematical fields such as differential geometry, algebraic geometry, topology, as embodied in some category C, embed them into a sheaf topos and then use intuitionistic logic to do constructions and theorems in this area that are vastly simpler than the usual formulations. For instance you can do this with differential geometry and get an intuitionistic logic where you can work explicitly with infinitesimal numbers to calculate derivatives in a completely rigorous fashion. Ingo Blechschmidt has written some expository material in this vein (his main work being in using this in algebraic geometry): https://arxiv.org/abs/2204.00948

On the "surprising" side, I think the most surprising things for me where seeing how existing mathematical structures were examples of generalized categories: metric spaces are a kind of enriched category and topological spaces are generalized multicategories for the ultrafilter monad.

It sounds like category theory likely has no direct impact on your life. So you can move on.

But please do not let this bleed into a criticism of category theory as used in mathematics. Category theory from the very beginning was developed to help manage the complexity of modern mathematical fields like algebraic topology. It was then famously used by Grothendieck in algebraic geometry where some of the basic notions (schemes) were defined in terms of category theoretic concepts (functors). It's been applied to many other fields, since, including yes computer science, and mainly for the same purpose: giving precise terminology to common patterns (monads functors etc) and giving us the right concepts to design new functional programming languages. As someone who is an expert on these topics I find some of the popular sentiments about programmers using category theory to be a bit silly, but I'll admit it's overall probably good for my field because it cultivates a lot of interest in students. It probably plays a similar role to pop science/math in other fields: not very deep but fun and can be a gateway to "the real thing".

The popular perception of category theory is a bit bizarre to me though. It is a beautiful theory with many useful results. But you don't see the same excitement or resentment towards fields like order theory or abstract algebra, which are very closely related to, and just as abstract as, category theory and are used in similar ways.

It doesn't have to be one or the other :). OCaml and Haskell are two great languages that the Rust designers were familiar with.

The big thing IMO that makes Rust feel like Haskell is the pervasive use of traits and `#[derive(...)]` which is directly analogous to the pervasive use of typeclasses and `deriving` in Haskell.

For context, Matt Might is formerly a professor whose research was in programming languages/program analysis. Professors like to code too!

I think OP is really overstating things. "the definitive underlying field of math replacing set theory" is something Lawvere was trying in the 60s and it never really took off.

Category theory isn't really a replacement for set theory any more than order theory is a replacement for set theory. What is important is not what your "foundational system" is, but that just like there are many concepts we learn in the context of set theory but are just very generally useful (equivalence classes, cardinality, injective/surjective functions), there are also similarly very useful concepts in category theory like adjoint functors, limits and universal mapping properties.

I think the concept you are looking for is a ["torsor"](https://en.wikipedia.org/wiki/Principal_homogeneous_space).

Basically,

1. You have a 0 time delta, and you can add and subtract them satisfying some natural equations. (time deltas form a group)

2. You can add time deltas to a datetime to get a new datetime, and this satisfies some natural equations relating to adding time deltas to each other (time deltas act on datetimes).

3. You can subtract two datetimes to get a time delta satisfying some more natural equations (the action is free and transitive).

I have to plug my favorite "explanation" of the Y combinator, which is called "Lawvere's fixed point theorem".

In a cartesian closed category, if there is a function p : A -> (A -> B) that has a left-inverse, i.e., e : (A -> B) -> A with p o e = id_(A -> B) then B has a fixed point combinator Y : (B -> B) -> B, i.e., every function from B to itself has a fixed point: Y(f) = f(Y(f)).

The proof is like the Y combinator in untyped lambda calculus, but with extra ps and es. This is because one way to understand untyped lambda calculus is that you are working with a single type D that satisfies D = (D -> D) (so p,e are identities).

I like this because it makes the connection between the Y combinator and diagonalization arguments like Cantor's theorem explicit.

For instance, Cantor's theorem says that the powerset of a set always has higher cardinality. We can reformulate this as saying that there is no onto function p : X -> (X -> 2) because a subset of X is the same as a function from X to booleans (2 = {true, false}). An onto function has a left inverse (using axiom of choice) and so if we have an onto function X -> (X -> 2) then every function (2 -> 2) has a fixed point, but this isn't true! If we took Y(not) we would construct a boolean b : 2 such that b = not(b), which is impossible so we have a contradiction. I found this helpful in understanding why the "not" appears in just the right place in the classical proof.

"Just Wrong" is a bit harsh. Monads are there to simulate side effects within the language, as opposed to the side effects that are built in to the language.

WARNING: the below contains math. Ignore if math makes you mad.

If "side effects" means the availability of certain operations such as mutating state, throwing errors etc, then monads certainly do have something to do with side effects in that these operations can often be described by an algebraic theory and algebraic theories have a direct correspondence to certain kinds of monads (the monad of free algebras of the theory).

Not sure about unloading the dishwasher but unpacking was pretty fun: https://www.unpackinggame.com/

Sure but it's worth emphasizing that Go language designers gave these built-in collections the exorbitant privilege of being parameterized by a type and declaring that any new type created by a mere programmer has to be monomorphic.

The mushroom is an ideal food...Low in fats, sugars and calories...

It's funny to see "low calorie" as a positive for an ideal food. From the perspective of getting people enough food to live, things like grains, corn/maize and potatoes are "ideal" foods because they can cheaply get us a significant portion of our needed calories.

Oh I see, so still pretty large since both countries are large, but if one of the bordering countries were small the distance would be small.

Wouldn't that make countries like the USA and Canada extremely far apart because they are both large countries? The distance you would get is the distance from Hawaii to somewhere on the northeastern edge of Nunavut/Newfoundland/Labrador

The analogy goes much further if you take it as "open set" =~ "semidecidable property", i.e., you can determine in finite time that something is in the subset, but may not halt on an input that is not in the subset. A closed set is one whose complement is semidecidable, i.e., "co-semidecidable". This gives some intuition to the finite intersection vs arbitrary union property (though in computability you would restrict to a kind of "effective" union, but still one that could be infinite). Then sets that are closed and open are the decidable properties.

Then the inverse-image definition of a continuous function is clearly satisfied by computable functions. A function f : A -> B is continuous if for any semidecidable property O on B, the property { x \in A. f(x) \in O } is semidecidable (since f is a computable function).

There's some very cool ideas here like Hausdorff == Diagonal is closed =~ the equality predicate is co-semidecidable, i.e., you can implement a partial inequality function that always returns true if the inputs are not equal.

See Martín Escardó's work for more details: https://www.cs.bham.ac.uk/~mhe/papers/barbados.pdf