Twisol

E-graphs are pretty awesome, and worth keeping in your back pocket. They're like union-find structures, except they also maintain congruence relations (i.e. if `x` and `y` are in the same set, then `f(x)` and `f(y)` must likewise be in the same set).

https://egraphs-good.github.io/

(Incidentally, union-find structures are also great to know about. But they're not exactly "new".)

> I've seen interleaved lexing and parsing, where the recursive descent parser asks for the next token, which is computed on demand.

You even get this for free in a lazy language like Haskell, where your parser can accept a list of tokens `[Token]` whilst the list itself is only computed on-demand whenever the parser tries to get the next one.

Well, except for the context-sensitive option:

> (and as a consequence, it's natural to let lexing be context-sensitive where needed).

They almost shuttered in 2002, it looks like!

https://lwn.net/Articles/5409/

Hosted by good ol' Dirk!

(For those not in the know, this is an in-joke originating at least from the Hello Internet podcast, with CGP Grey and Brady Haran. "Veritasium" is, indeed, the correct spelling.)

I'm a bit wary of offering a logical explanation for something that is less reasoned and more habitual/cultural, but if I had to, I'd say corporations present a single unified posture that is not necessarily reflective of the posture of any single constituent of the corporation. Thus, it is somewhat fallacious to attribute that (carefully curated) posture to any(/many/most/all) of the individuals within that corporation.

Incidentally, I think it's funny (but justifiable) that you used "is" here:

> But Facebook as a company is plural

On introspection, I think I would/have used both "it" and singular (agender) "they" for corporations.

I've heard some people (I think mostly in the UK?) treat corporation names as count nouns, as in "Jagex are" (or "Facebook are") rather than "Jagex is". I can see how this makes sense if you think of a corporation as fundamentally comprising a group of individual people, but it still sounds very strange to my ear.

Unfortunately, I have absolutely heard people say "this datum" and "these data" -- admittedly not "three data", but certainly in the style of a count noun, and not in the style of a mass noun. If they used it as a mass noun, they would say "this data", not "these data".

Even in English, depending on who you talk to, "data" might be either count or mass. (I am solidly in the mass camp.)

That's a good question -- this result is arguably the one that made Georg Cantor a legend. (It's called Cantor's theorem, after all!) I had to refresh myself on the proof, but it boils down to a less obvious kind of "diagonalization" (this time to construct a counterexample).

We can show that S has a strictly smaller cardinality than 2^S by showing that no function from S to 2^S can hit every value in 2^S. That is, there's going to be some element of 2^S that no element of S gets mapped to.

Suppose, as one does, to the contrary: that there is a function, call it F, that hits every element of 2^S. We'll construct a particularly pathological element of 2^S, call it B, the set {s in S | s not in F(s)} of values of S that are not members of the subset F picks out for them. (Remember that 2^S is the set of subsets of S, so it is meaningful to ask whether any s is a member of F(s).) If this smells like Russell's paradox, good -- follow your nose!

Now, since B is a subset of 2^S, and F is presumed to hit every subset, there's going to be some element b such that F(b) = B. We ask the critical question: is b in B? If it is, then b is not in F(b) -- but F(b) is B, contradicting our assumption. If it isn't, then b is in F(b) -- but F(b) is B, contradicting our assumption.

Since we end up at a contradiction no matter which way we resolve "is b in B", and we know this question must be answered one way or the other, we must admit that our supposed function F must not have the property we asked for; it must not hit every element of 2^S. So 2^S really is "bigger" than S, in that no matter how we pair every element of S with an element of 2^S, we run out of elements of the former before we've exhausted the latter.

Not in terms of cardinality, at least. Consider the set of natural numbers {0, 1, 2, ...}. This set is clearly of infinite size. If we remove 0, then we have a set {1, 2, ...} with, in principle, one less element than we started with -- yet it is also clearly infinite.

However, these sets have exactly the same number of elements (i.e. "infinity-1 is the same size as infinity") -- I can pair 0 with 1, 1 with 2, 2 with 3, and so on, so that every number in the first set is uniquely paired with a number in the second set, and vice versa.

Arithmetically, I can write `f(x) = x + 1` to go from the first set to the second set, and `g(x) = x - 1` to go from the second set back to the first set, and "clearly" we don't lose any information performing `f` followed by `g` -- no two elements land in the same place in either direction.

> There are only two types of infinities: countable and uncountable.

That's not true, either. For any infinite set S, the powerset 2^S is also infinite, but there is no injection from 2^S to S. Therefore, the cardinality of 2^S is bigger than the cardinality of S. You can iterate this and get a tower of arbitrarily many distinct types of infinity.

"Countable infinity" describes the cardinality of the set of natural numbers. "Uncountable infinity" describes any infinite cardinality that is not that of the natural numbers -- it just means "not countable".

> Both reals and rationals are not countable

The rationals are countable, by a diagonal construction. Take an Excel spreadsheet with rows labeled 1, 2, and so on; and columns labeled 1, 2, and so on. In every cell, write the cell's row over the cell's column as a fraction. By construction, every rational number n/m will exist in this spreadsheet, at row n and column m.

Now walk the spreadsheet in diagonals: first the first diagonal (just 1/1), then the second diagonal (1/2, 2/1), then the third (1/3, 2/2, 3/1), and so on. This yields a sequence (i.e. a mapping from naturals to ratios) where every ratio is guaranteed to appear at some finite index. But because every ratio appears in this sequence, we can go backwards, taking a rational number in reduced form and finding its index in the sequence, giving us an inverse map from rationals to naturals.

Every rational number therefore gets its own unique natural. Since this is an injection, the set of rationals must be no bigger than the set of naturals. (In fact, it's the same cardinality, but my argument is a little too imprecise to show that the rationals are no smaller than the set of naturals -- two naturals in this construction may land on the same rational number. We would fix this by just skipping ratios not in reduced form.)

FWIW, at this point, the initialism has kind of become the name. It's like POSIX -- I doubt a lot of people know what it stands for, but it doesn't matter, because there's only one POSIX and it's the portable operating system interface.

> Very dismissive statement that misses the person's point.

I read it as acknowledging that you shouldn't feel like you have to spend time on things that provide you no value. That seems to directly acknowledge the point I took from the earlier comment, which is that they keep spending time on it and coming away with no idea what they even should be getting from it, much less getting anything specifically.

(I like category theory, but it's a reasonable reaction for most people. I'd love for more people to engage with it on its merits, but also, people have finite time and may rather spend it on things they derive joy from.)

> I got confused by the infix definition of "~>*".

Aaah, I'm sorry -- I thought you meant the theorem body -- the proof itself -- was hard to parse. (Which it also is!)

Yes, custom infix operators are just one of many novelties you can find in these languages. I think Haskell is the only "mainstream" (hah) language I'm familiar with that has anywhere close to the same degree of syntax customization.

All these things together really do make for a steep learning curve...

Scott Wlaschin's "F# For Fun and Profit" website is a great resource for strongly-typed (yes) data modeling with sum types as a fundamental tool.

https://fsharpforfunandprofit.com/series/designing-with-type...

By the third entry in the linked series, we've motivated the use of a sum type with three variants in the example domain model.

> My intuition is: evaluating in Lean and embedding the result in the toy language is identical to big step evaluation in the toy language.

Yes, I think that's right.

> But I can't parse the theorem.

I think there's a bit of a divide between languages with tactic-based proofs and languages without tactics, and it looks like both Lean and Isabelle use tactics.

I've gotten very comfortable with Agda over the past year. Agda doesn't have a real tactics metalanguage; but I honestly prefer working with proof terms, since it's easier (I feel) to write comprehensible proofs. While tactics make for very compact proofs, I think giving a proof some space to breathe is a good thing -- I'm interested in why it's true, not only that it's true.

I think the analogous theorem in Conor McBride's Agda version of this development is here [1]:

    ev=>* : {t : Ty} (x : Exp t)
          -> x =>* ve (ev x)

where "eval _" in Lean becomes "ev x", and "_.embed" becomes "ve _".

The theorem body is heavily commented (nice!), and each case is handled explicitly and in full. While the development is probably a little bit longer than in Lean or Isabelle, I find it easier to approach.

[1] https://github.com/pigworker/Samizdat/blob/main/ExampleSeman...

> I could not write this stuff. It looks simple but it isn't.

True that. I bounced a number of times off of proof assistants before it stuck. Like I said, I feel very comfortable with Agda now; but I won't claim this is easy.

I agree most of the time, but it can make sense in certain contexts. One common example is comparison methods:

   if (x1 < y1) return true;
   if (x2 < y2) return true;
   if (x3 < y3) return true;
   return false;

I wouldn't want to replace the last two lines with `return (x3 < y3)`, even though that's functionally the same thing.

In this contrived example, we could just return a single compound condition, but hopefully it's clear that there are cases where doing so would make more of a mess, too.

I didn't find the playerbase very hostile at all -- although I wasn't involved in most PVP combat activities, which IIRC is also where most of the "pay to win" is focused.

(never did save up enough to buy wings, though)

> this is the same country that has the national power grid introduce "hum" (or whatever it is technically callled) in the signal so that a time reference can be decoded from it.

I don't think that's intentionally introduced. My understanding was that mains hum in any grid is an artifact of a noisy signal that just happens to be useful as a forensics fingerprint.

https://en.wikipedia.org/wiki/Mains_hum

Cook! If you're who I think you are, I bet you don't recognize me under this name, but hi from an old b'crat :)

The MOV-only CPU [1, 2] is probably about as close to this as you can get. If you think about it, every structured programming affordance is sugar for writing a state machine. MOV-only pushes all control flow into a state machine, and does so without using any branches itself. It's all MOVs all the time.

[1] https://github.com/xoreaxeaxeax/movfuscator

[2] https://harrisonwl.github.io/assets/courses/malware/spring20...

Is this another way of putting what you're saying?

In functional programming, we think of computation as reducing an expression; a computation is complete when it can't be reduced anymore. In imperative programming, we think of computation as updating a store of data; a computation is complete when we run out of steps to perform.

When you're partway through execution, the "rest of the program" in an imperative system is captured by the current state of the store (including the stack). In a functional program, the "rest of the program" is just the program expression itself, reduced as it has been up to this point.

I tend to like the functional model, myself, but I can see the mental appeal of keeping the program text fixed, and isolating all changes to a separate store of data.

State is made of data. The difference is that state is data together with a persistent identity (morally, a location), and the data associated with that identity may change over time.

I was starstruck enough just sitting next to Daniel Friedman ^_^;

Good question. "Do notation" is sometimes referred to as "the programmable semicolon", because how you go from one statement to the next depends on which monad you're in. (In the List example, the assignment `x <- [1, 2, 3]` forked execution three ways before proceeding to the next assignment.)

In Java, the semicolon is pretty much fixed; you can't change the relationship between statements in any meaningful way. So you have to play tricks. You can implement the List example in a crafty but leaky way:

    do(() -> {
      var x = choose(1, 2, 3);
      var y = choose(4, 5, 6);
      return x + y;
    });

When `choose` is called for the first time, it remembers which choice it returns to you. When you `return` from the block, your result is stored, and then the function is re-executed -- except this time, `choose` will now return a different value (the next one). You can implement this in a rather small handful of lines, but it's very tight and clever code, and not at all obvious how it works at first glance.

There's another way to do this, with chained `flatMap` calls, like:

    list(1, 2, 3).flatMap(x ->
      list(4, 5, 6).flatMap(y ->
        list(x + y)));

...but that's so different from "normal" use of a language like Java that readers and writers alike are likely to balk to some extent.

Not exactly (although maybe you could implement that pattern with the right choice of monad).

    do
      x <- [1, 2, 3]
      y <- [4, 5, 6]
      return (x + y)
    -- [5, 6, 7,  6, 7, 8,  7, 8, 9]

Here we have a series of assignments followed by an expression computing a result. You can't tell directly, but this is using do-notation in the List monad -- an assignment `x <- [...]` picks a value from the list, then continues. In fact, this code is run once for every possible choice from the given lists, and all of the results are aggregated into a list.

The earlier commenter referred to the Identity monad, which would look like:

    do
      x <- 3
      y <- 5
      return (x + y)
    -- 8

No special lists this time -- what you put on the right is what gets stored in the variable on the left. This is what you're used to in any imperative language.

I suspect `bb` is a little more special, because Ron mentioned it has similarities to LOOP. I'd guess it supports recursive definitions somehow, but it's not clear what the difference actually is.

As a complement to my other reply to you, I'll note that I developed a simulation system in Java (a very common language), and strove to keep it small, avoid complexity, and generally make it approachable -- but for a long time I remained the only one who understood how the system worked, because you simply had to understand the business domain in order to understand why things worked the way they did.

This is my personal opinion, but I think that domain expertise is a much stronger component of bus factor than language choice is. You can write unmaintainable code in any language. But good code often still has prerequisites to understanding. Meanwhile, if you have the domain expertise, you can get quite far in understanding semi-bad code just by pattern matching on manifestations of your domain.

I was referring to the discipline as a whole, not scouting at the granularity of a single team. Also refer to take three: working in an industrial team is not a prerequisite for an application of programming to be valid.

But to your very specific point: I have in the past developed prototypes in Rust whilst on a Java-only team. It's actually a good thing: these prototypes were meant to be thrown away, so working in a different language (and one that helped me model things effectively) meant we were forced to throw it away then write it right in Java once we knew what we were doing.

(We did the same thing for another feature, but it was someone else and they preferred Python. Again, we were able to prototype more rapidly and then implement a solid solution in Java once we knew how things should shake out.)

Take one: We need people moving together just as much as we need scouts who can push ahead and find the best paths for the rest of us.

Take two: Working in the best fit for your brain is not incompatible with working with others -- enough companies are Java shops, why can't there be CL shops? (There are assuredly Clojure shops at the very least.)

Take three: Not everything has to be about work. Programming is a skill, not an occupation; there are lots of ways to apply programming as a skill that don't require you to build large edifices in teams.