Twisol

I remember this talk! The speaker recommended doing this with the tax code because it was one of the most mechanical -- very little inherent ambiguity, there's just a lot of surface area to cover, so it's a great candidate for actually applying formal methods to.

> Perhaps this is just my autism speaking, but am I the only one who gets completely freaked out by sentences like the above?

Hi, fellow autist here.

Yes, it feels like my brain hits some speedbumps with that particular pronoun. I wouldn't say I get "freaked out" though; it's just unfamiliar yet.

Despite what other comments claim, I doubt this is agrammatical. "It" is part of the same grammatical class (the class of pronouns!!) and so fits anywhere "he" or "she" does.

> "It" refers to inanimate objects, things which can't have free will

Could you bring yourself to see the choice of "it/its" pronouns exactly as a self-identification with things that feel no agency of their own? I don't know why Maia claims those pronouns, but I'd get this motivation for sure.

As a child, I re-read The Number Devil constantly. It introduced me to some really cool mathematical ideas, couched in a cute story. The very last chapter includes a picture of the Principia Mathematica's proof of 1 + 1 = 2 -- mostly for shock value, I think, but also "even this is within your reach". I recently got to see a friend's copy of the Principia, and I realized just how much of it I actually did understand, which was a really nice closing of the loop.

As an adult, Imre Lakatos' Proofs and Refutations gave me a much richer understanding of definitions in mathematics -- what job they're meant to do, and when it makes sense to change your definitions instead of adding premises to your theorems.

I could have made my argument without that line. Thanks for checking me.

> (and motivated)

Look, that's the important part, right? If I wanted to learn the material, I could. But I'm not really interested in learning the material right now, or following the arguments exactly. It's a great article when you're in that mindset.

Quanta, I don't have to be ready to learn the material. I can get a little awareness of what's going on, I don't have to follow specific arguments over a series of paragraphs -- it's news, not lecture. Sometimes that's what I need, to keep aware of what's going on without having to learn it straight up.

I'm a fan of channels like Mathologer and 3B1B, so I'm no stranger to sitting down and following a lovely argument all the way through. I just object to the idea that Quanta is serving the same need as this article and doing a worse job. I just think it's serving a different need altogether.

Even as someone with mathematical training, my eyes started skipping lines a few paragraphs in. This content is good, for sure, but you have to be in the right headspace to follow along. Quanta's material is serving a different need.

Quanta tells you about it. This article tells you it. Both are valuable!

The first thing I thought of when I saw the name was the opening theme for a 2011 anime called "Phi Brain", which uses the word "misskey" in its lyrics. (I don't think it has any meaning?)

Lo and behold, that's where the name comes from: https://misskey-hub.net/en/docs/misskey.html

> The name "Misskey" comes from a song called "Brain Diver" by a band that syuilo used to listen to at the time called May'n.

Also, for the benefit of the other discussion happening here:

> Who's that cute cat-eared girl that you see sometimes?

> It's Misskey's guardian deity, Ai.(They called Ai cute, yay!)

For want of context, this is the library described in the article.

And CALM stands for Consistency As Logical Monotonicity -- CRDTs evolve monotonically in a certain sense.

That makes a lot of sense -- thanks for contributing that nuance!

Gravitational attraction still dominates on even fairly large scales, and chemical bonds absolutely dominate over anything expansion could possibly do -- it would contribute an incredibly light force opposing any bonds. So no, we (and our galaxy) are in no danger of being inflated from the inside by space itself.

Yes, true -- the distance between two points doesn't grow linearly, but rather proportionally to itself :D

> Rather it's that the rate of expansion of the universe is accelerating, so that we're moving away from parts of it faster than its light can cover the distance to us.

From my understanding, it's not that we're moving away from parts of the universe, but that the distance between us is growing so fast that light sent from one part will find that after traveling toward us for some amount of time, the remaining distance to travel is actually more than than when it started.

One way for the distance between two objects to increase is indeed for those objects to literally be moving in opposite directions through space. But the expansion of the universe itself causes the distance between two otherwise-stationary points to nonetheless increase. Put differently, it's the cosmic yardstick that's shrinking, not the entities that must necessarily be moving.

(This is also why two points can be "moving apart" faster than light speed, the cosmic speed limit.)

I think both types can enjoy fun diversions. I think being a "simplifier" just means you can make a distinction between diversions and solutions.

For me, every additional moving part has a cost, and that cost needs to be amortized over sufficient use-cases. Sometimes writing your own OOP framework in C is just what the doctor ordered. Sometimes it isn't.

I goofed on my calculations a little bit -- steno boards are designed so that one finger can depress two keys at once, so in principle you can actually hit all 20 keys simultaneously. You can't just hit any two keys with the same finger, though, so I don't believe it gets quite to 2^20 possibilities.

(Also, I computed only 20 choose 10, when you can of course have any smaller subset as well. I guess the point here is, a stenotype gives you even more than 184k inputs.)

I also picked up a basic steno keyboard earlier in 2022 (the EcoSteno, I think). I'm no good with it yet (I'm still working through layout drills, honestly), but for me, the draw isn't in transcription or text input specifically, but in chord-based control over my computer more generally.

A standard computer keyboard layout has ~100 keys. You can use various modifier keys (Ctrl, Alt, Shift, Meta) and combinations thereof to assign multiple meanings to each key, which morally organizes the keyboard into layers depending on which modifiers are active, but most layers are inconvenient to reach -- anything beyond two modifiers gets annoying and sees limited use. You're almost always on the unmodified layer.

A stenotype board has only ~20 keys, but the unit of input is an entire set of keys rather than a single key. In principle, you can comfortably enter chords of up to 10 keys at once, giving ~184,756 (20 choose 10) inputs. This is modified a bit by ergonomics, but it's still orders of magnitude more possibilities than an idealized keyboard with modifiers (something like 1,600).

That kind of space for addressing commands begs for some kind of principled organization. The Plover community calls assignments of commands to chords "dictionaries", and they generally follow an internally-consistent set of rules called a "theory". If you're working with English input, for example, you'll learn a theory that lets you almost always reason out the chord for a word.

There's nothing that limits stenographic input to transcription, though. You can assemble, say, a dictionary of Emacs commands, and assign related commands chords that share a common subset of keys. (Emacs is kind of like this already IMHO, but I am not a fan of the modifier+key system -- it feels like the addressing space is too small, and I'm afraid to customize the default keymap.)

Moreover, you aren't limited to single-chord input either. Multi-chord input is common; you can easily define entries in the dictionary which are based on a sequence of chords. I believe (but lack the experience to confirm) that English dictionaries tend to be organized around syllables or syllable clusters; the normal English stenotype layout specifically has sections for initial consonent, vowel, and terminal consonant, and theories tend to organize around that structure. Again, there's no reason you can't apply the same tools to non-transcription inputs.

I think this is a really cool input system, and for my interests, complementary to a regular QWERTY keyboard. I still want to learn a proper English theory (to avoid having to switch frequently between multiple keyboards!), but I mostly just want to have the option of chorded input in the first place.

As I understand it, submissions are moderated (albeit lightly -- not to the degree of formal peer review). So, since it's on the arXiv, we can assume that the moderators felt it belongs there.

I've seen a number of other book-length items on the arXiv before, including e.g. Seven Sketches in Compositionality [1], so this isn't a particularly new trend, either.

[1] https://arxiv.org/abs/1803.05316v3

> It felt to me more like ‘I had some ideas about programming languages after 20+ years of Haskell and research. Here’s my plan to unify logic programming with more normal functional programming (also we’re getting rid of monads). By the way my boss cares about the metaverse.’ But maybe that is too cynical.

For what it's worth, Tim Sweeney (the "boss" in this story) has been thinking about Verse or something like it since at least 2006: https://www.st.cs.uni-saarland.de/edu/seminare/2005/advanced...

It seems much less like SPJ getting funding from a big-bucks metaverse boss, and much more like Tim Sweeney getting together a dream team to make his dream language in one form or another.

You can sort of justify "the Amazon River" as "the Amazon river" -- i.e. the river that happens to be in the Amazon rainforest. The other two don't really act like "adjective + noun".

This is one of those titles that doesn't make sense when HN drops the leading word. It should be:

> Why I start taking English classes at the age of 46

I'm still waiting (agonizingly) for pattern matching in switch to actually land as a non-preview feature. We're looking at a fourth preview in Java 20 (March 2023), so we probably won't get it for realsies until at least Java 21 (September). And that's assuming the associated record patterns JEP is also ready to go after just two previews; it seems like they want them to land together.

> Category theory is literally the mathematics of boxes (objects), arrows (morphisms), and composition.

As I've learned more about category theory (and its applications), I've found string diagrams to be a really nice tool. But string diagrams flip the above around -- morphisms are boxes, and objects are wires. A wire is just a point-to-point link; it doesn't do anything on its own, it just connects a port of one type with a matching port on another site. It's the graphical realization of the composition operation itself.

Meanwhile, morphisms are the things that actually have behavior and real identities, so we draw them as boxes with inputs and outputs and give them names. This lines up with my understanding that in category theory, it's the morphisms that matter; the objects are no more than labels governing how you can stick the morphisms together. You may as well call the morphisms "widgets" or "components", and call the objects "interfaces", because that's literally correct.

This ends up really nice in the context of distributed systems, where concurrency gives you a monoidal category. In string diagrams, concurrently is quite literally the result of putting two diagrams side-by-side, rather than connecting them end-to-end. It's lovely, and some of the research I'm doing right now is actually founded on formalizing the message-passing causal diagrams distsys researchers and practitioners use every day, and using them as a vehicle for building programs that are more amenable to being proven correct. (Distributed systems are hard to verify for both humans and computers; I'd like to think that what I'm doing will be just as good for giving human practitioners a good framework for convincing themselves their code is correct -- or better, making bugs more obvious.)

"Functor" has been used in multiple ways in different fields. It's apparently a term of art in linguistics; we call C++ classes implementing `operator()` "functors"; Prolog terms have parts called "functors" (apparently imported from linguistics); and of course category theory has them.

As far as mathematics is generally concerned, I think the category theory concept is the origin. Monoids, on the other hand, did exist before category theory; the modern conception as one-object categories is nice, but it's definitely an import.

> Mathematics is the mathematics of abstraction.

> Category theory is the mathematics of composition.

I don't know why you're being downvoted (tone?) but you're right. Categories formalize exactly and only the notion of composition; its power is that this notion appears everywhere when you know what to look for. Most mathematical abstractions have composition baked in at one level or another, so I think the author should be pardoned for their phrasing; but I find yours more enlightening.

I second this recommendation; Cheng's book is probably the most approachable of the recent wave of category theory texts which does not assume the whole edifice of abstract algebra as a starting point.

Most CT texts introduce categories around page 1, and the Yoneda lemma a handful of pages in. Cheng's book builds up intuitions until chapter 8, where categories are defined over the course of several pages, and supposedly (I'm not there yet) ends the book with the Yoneda lemma.

You might think this means the book is mostly fluff. First: if you read it and think that, you're probably a more advanced reader than she's targeting. Second: goodness no, it's packed to the brim with categorical intuitions; there's a whole way of thinking that she's trying to motivate. Categories are just a formalization of this way of thinking; if you're not onboard with the thinking, the formalization is going to be hollow to you no matter what.

Do recommend.

I think learning the essentials of another field can be more valuable than expected, whether it's a mathematician learning to program or a software engineer learning patterns of abstraction. When you've gone deep on one field, going even deeper has diminishing returns.

Software engineers and (non-categorical) mathematicians are both forced to deal with patterns of abstraction on a regular basis, so they naturally pick up a lot of what category theory concerns itself with. This can make category theory sound like quite a lot of words for very little gain. But I do think that formalizing one's intuition -- taking something understood implicitly and giving it explicit form -- can be a useful tool in its own right.

Most of the material out there on category theory attempts to formalize the algebraist's intuition. Software engineers then have to learn algebra just to learn category theory. I don't think that's essential to category theory, and I think we're starting to see more and more "elementary" category theory that doesn't take some other whole edifice as given. The fact that so many software engineers exist who do find value in a categorical perspective (it's more than you'd expect!) suggests that we'll get there eventually.

> However, it turns out that category theory is equivalent to type theory (ie, what computers use).

Just to elaborate on this a little, a program of type B in context of variables of types A1, A2, ..., An, can be modeled as an arrow (A1 * A2 * ... * An) -> B. (More elaborate type theories get, well, more elaborate.) The various ways you might put programs together (e.g. if-expressions, loops, ...) become various ways you can assemble arrows in your category. Sequential composition in a category is the most fundamental, since it describes dataflow from the output side of one program to the input site of another; but the other ways of composing programs together appear as additional structure on the category.

Categories take "semicolon" as the most primitive notion, and that's all a category really is. In fact, if you've heard monads called "the programmable semicolon", it's because any monad induces a related category whose effectful programs `a ~> b` are really pure programs `a -> m b`, where `m` is the monad.

> you really need to use haskell.

Or Scala. They're the only two common-use languages I'm aware of whose type systems are expressive enough to define what a monad (or a category, or a ...) is internally. Of course you can identify particular monads (or ...) in any language, but you can't talk about them inside most languages.

I don't know for certain, but I suspect it simplified the language's grammar, since C's "declaration follows use" rule means you can basically repurpose the expression grammar for declarations instead of needing new rules for types. This is also why the function pointer syntax is so baroque (`int (*x)();` declares a variable `x` containing a pointer to a function taking no parameters and returning an int).

For sure, skip ahead :) Math textbooks are not generally meant to be read front-to-back (and math papers even less so). This one lends itself well to a straight-line readthrough, but what's important is what you get out of it.

As the sibling comment notes, if you skip too far ahead, the technical material will make you very well aware of that fact. But I think chapter 8 is a good place to jump in -- the material up to that point is mostly setting up intuitions and analogies. I think those are important to pick up, but they're also the kind of thing you pick up from sufficient exposure to mathematics of any flavor, so there's no harm.

Chapters 9 through 13 show how lots of other things can be seen as categories, so if you're already aware of some of them from undergrad math, you're probably good to go.