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.