mkehrt

Aha, thanks!

You've exactly described the answer, but to people who don't know much about dependent types, this may be a little unclear. The point is that there are two sorts of dependent types.

When people who don't know much about them think of dependent types, they are probably thinking of functions, which can take a value on the left hand side to be used in the type on the right. Confusingly, these are normally called "dependent products" in the type theory. However since this is confusing and they are generally written with a capital Pi, they are often just referred to as "Pis". For example

    Pi x:nat . Vec x string

is a function that takes a nat (non-negative number) and returns a Vector whose length is that nat and which is encoded in the type.

On the other hand, you are talking about pairs (confusingly: "dependent sums", here "sum" being something like a union/enum in type theory), often called "Sigmas". These are pairs (2-tuples) of values in which the type of the second value depends on the value of the first. So, your example, a pair where the vector length is held in the first element and the vector itself in the second. In this contrived example, Vector may not know its own length at runtime, so we need to package them up together.

        Sigma x: nat . Vec x string

These are both "dependent types", but people who are only passingly familiar with them might mostly know about the first.

(Why are functions "dependent products" and pairs "dependent sums"? I've never understood this but I've heard hand-wavy explanations that infintitary products are functions and infinitary sums are products ¯\(ツ)/¯)

To me as an American this sounds perfectly fine.

I’m not sure that’s true. We have literal billions of years of training.

I absolutely cannot remember the details, but we did typesafe, macro based generic data structures in C in an undergrad class I took ~20 years ago (CMU Operating Systems). The idea has definitely been around, though I don't know if the implantation was the same.

Take it up with Isaac Asimov, I guess.

Well, we were using it to talk about things like cache invalidation and lax memory models rather than properties of algorithms.

As other comments have pointed out, this is just not true in general usage.

When I was a grad student studying this stuff (~20 years ago), we used "parallelism" to mean running on different cores at the same time and "concurrency" to mean preemptive multithreading on a single processor.

> You could literally "reduce" and array of integers to a cancellation token, or a state object, or anything else

This is what reduce does, though? It reduces a list to a single thing. It seems like you're thinking of filter.

You can disable this misbegotten feature with

stty -ixon

This is a readline feature. You can enable it in bash (and other shells?) with:

bind '"\e[A": history-search-backward'

bind '"\e[B": history-search-forward'

Interesting; I assumed the write to stdout would just hang for the writing program.

Sorry, by "official support" I mean that there is support within MSR to investigate these tools as a research project, no that there is a plan to actually do the conversion.

As I pointed out in a sibling comment, the plan isn't for it to work. This is a job posting for a researcher at MSR to investigate what it might look like someday.

It's less one guy's plan and more one Microsoft Research team's research goal to investigate technologies that might enable that in a few years. So probably more institutional support than just some guy, but less actually planning on succeeding in the full ambitious goal.

I enjoyed this Terence Tao post the other day.

The relevant quote is

> one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?"

And later

> But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided by any human expert in the field X resides in, has created an unprecedented divergence between the production of answers, and the production of insight, to the point where the two questions have become _negatively correlated_:

https://mathstodon.xyz/@tao/117208618508728654

I don't understand what you're saying? An LLM is a transformer model trained on a large corpus of natural language, often with some post-training. An image model is a different type of transformer model. What's controversial here?

Sure, and those aren't LLMs?

This isn’t talking about correctness of SQL. It’s talking about correctness of queries.

So www.catb.org/~esr/jargon/html/M/mu.html

I think this is true when you realize "customer" means "coworker" or "person on the next team over" or "management" or "your intuition about the problem". Which all sort of have the same shape.

There are in fact rough breathing marks there on the articles, stacked under the inverted breve accents. Which is an alternate form of tilde.

Sort of. Romans didn't handwrite like that. See https://en.wikipedia.org/wiki/Roman_cursive . Note that the "u" character in both ancient and late ancient Roman cursive is more like the modern "u".

(Source: not an expert in any way)

Absolutely that is not the point of programming. The point of programming is finding good abstractions, writing clear and concise code, creating beautiful algorithms.

If I wanted to make a product, I'd be a product manager.

Jack regularly mixes up words to humorous effect, so knowing that may help with the joke. But yeah, I agree the joke doesn't really work here.

Outlets benefit from standards, however. Every device (well kind of) uses the same few plug types, and a different plug would be a disadvantage.

On the other hand, having a bunch of different languages is an advantage. People can pick the best tool for the job, and experiment with new language features.

Do you think writing books (and Wikipedia articles, and stack overflow articles, and github repos, and, and, and, and ...) is not a value add?? What terrible claim.

Well, that's literally what "vibe coding means", no?

What exactly are you “getting done”? I’m really curious what you’re doing with so many tokens.

One thing that has happened is that "AI" has been an academic discipline since literally the 1950s. The term was originally used in the hope that we would soon be able to emulate human minds. This turned out to be hard, but the name stuck to the discipline.

Now, suddenly, this name has been broadcast to every human in the world more or less. To them, it's a new term, and it obviously means something human mind-like. But to people who work on AI, that's not generally what it means. (Which isn't to say that some of them don't think we're near to achieving that; they just use other terms like "AGI" for that goal). So the name, which has a long history, is deceptive to people who aren't familiar with computer science.