I wouldn't confuse modules with modularity. Think of it like this: types are the primary API for the program. In fact, I tend to call the modules that perform this function in my code something like 'Core'. Since they're a shared language that allow different parts of the code to communicate without knowing any implementation details, these types actually make it possible to write code that is more modular, not less. Different parts of the program can go about their business and perform specialised tasks, while still being interoperable (and composable) with other parts of the program (and, hopefully, code not yet written—although this very much depends on how well your types model your problem domain).
I'm not sure the author's explained this point quite as clearly as it could have been. One doesn't want to expose every type used in the program across all modules: there are many that are just used in internal representations within particular modules.
Here's an example from a project of mine, which is a command line program to produce truth tables. There's a Core module which contains the types shared across the whole program, and the most fundamental operations on them.
The command line program itself is defined as a Main module, which imports the pure library modules and does all the I/O. It has a few types of its own but these aren't shared across the program, because the library doesn't need to know about all this stuff.
"[The LLVM backend] is an alternative backend that uses the LLVM compiler to produce executable code. It generally produces code as with performance as good as the native code generator but for some cases can produce much faster code. This is especially true for numeric, array heavy code using packages like vector. The penalty is a significant increase in compilation times."
Having written the following, I now wonder whether you meant something more specific by computation than I did, so I'm not certain whether my point is really a response. Could you spell out the details of your comment a bit more, and perhaps touch on the approach which Wolfram argues for?
* * *
Offloading computation only works when you understand what the computations are and why we do them. That's something that must be learned, it's not knowledge that springs fully formed into our minds as soon as we step into a classroom.
Carrying out computations thus gives us explicit and implicit knowledge of how the things we may eventually automate actually work. But it's also valuable because it trains us to compute in a precise and effective manner—a capability that remains useful later on. For instance, in logic it's often important to be able to carry out syntactic manipulations (e.g. into normal forms) in one's head, or even tacitly.
I'm sure there are plenty of examples from other areas of mathematics where computation is important, it's just that we do it so automatically that we don't think about it. Often I've found that students have trouble following proofs that take logically and computationally innocent steps without saying what's going on. Here I don't mean things like applying AC in the background, but just simple tricks like de Morgan's laws or taking the contrapositive. They have difficulty because they haven't taken those steps often enough themselves to have internalised them.
Yes, it does rely implicitly on Cantor–Schröder–Bernstein. That might be a downside, but I think when working informally (that is to say, when not teaching a set theory course) one can simply assert that if there exist injective functions from sets A and B into one another then they are equinumerous.
That being said, although important in the theory of the order of the cardinal numbers, Cantor–Schröder–Bernstein doesn't show that the cardinals are totally ordered. That statement is actually equivalent to the Axiom of Choice, whereas as far as I'm aware Cantor–Schröder–Bernstein holds in ZF.
I think this becomes much more intuitive once one understands that the cardinality of any nondegenerate closed interval is the same as the cardinality of the continuum.
The usual way this is done is by selecting a canonical representation for the reals in the list. It's pretty much the same thing as you said, but I don't think you're putting it in the right terms.
The list you're diagonalising (in Cantor's diagonal argument that the reals are uncountable) is a list of real numbers. Each of those reals has a canonical representation, and the reals in the list are ordered according to an order defined on those representations. The argument then demonstrates a method of constructing from those representations a representation of a new real which, by definition, cannot be one of the reals in that list.
Put in those terms it feels a lot less arbitrary than simply excluding certain strings.
Like I said in my response to pndmnm, in my view if someone "[would] think that the cardinals also formed a set with an (infinite) cardinality of its own" then they haven't really grasped the theorem yet. It's built into it that if we're always allowed to form the powerset of a set then regardless of how large a cardinal you can find, you can always take its powerset and obtain a larger cardinal.
I'm not saying it's not interesting—in fact, I think it's fascinating—but all of this is implicit in Cantor's Theorem. "Harder question" to me implies there's something there that goes beyond the fundamental result that the powerset of a set X has strictly larger cardinality than X. One might think that it's just harder to understand, but I would dispute that too: if someone thinks they get Cantor's Theorem but has trouble grasping that there is no set of all sets, or largest cardinal number, it just shows that they don't really understand the theorem itself yet.
Why is that a harder question? It's a direct corollary of Cantor's Theorem that there is no largest cardinal number (assuming the powerset axiom, of course).
I don't think one can ignore that and also focus on practicality. Using these JS dialects is a practical issue. Learning them and remembering how they work imposes a certain amount of overhead, albeit a reasonably small one. Of greater concern is maintaining projects written in these dialects: what if the support around key parts of your toolchain goes away? Of course they're open source, so you can maintain them yourself—but that may be a lot of work, and will rarely be the highest priority. Ultimately it may be more effort than it's worth, even if it's a lot more enjoyable to write than vanilla JavaScript. I'm not saying that this will always be the case, but it's an issue that does need to be addressed before jumping in and using them on a major project.
Anyway, Udon was really just a personal library which I tidied up and documented in case it might be of use to somebody. I think this is generally good practise: it encourages one to write clean, maintainable code, some documentation, and a test suite with reasonable coverage. In principle one should always do these things, but somehow putting it somewhere public makes it more likely that they'll actually happen. I was actually quite surprised to see it on Hacker News today, since I first wrote it two years ago and last made any changes to the source code over a year ago.
In other words, I'm not exactly falling over myself to promote it to the wider world or make it fit people's needs other than my own. Patches to increase the functionality of the library or improve the documentation would of course be welcome, and several good suggestions have already been made on this thread. But I'm not too concerned about convincing people here or elsewhere that they should be using it. In fact, they probably shouldn't: as you and others have said, most or all of its functionality is provided by other libraries which are far more actively maintained (this is really just a corollary of my first point).
However, I would be interested in hearing what you think is strange about the documentation and usage.
> having to write Udon.curry everywhere sort of takes away from that cleanliness you are trying to recreate.
This is true, and I considered your approach when writing functions like `elem`. There were two reasons for this. Firstly, I wanted to avoid introducing more closures than necessary. Secondly, I wanted to keep the source code reasonably transparent (if admittedly rather terse).
There is definitely a place for your approach, and it may even be the better one in practise. It's hard to say without writing large projects in both.
http://www.danzigercartoons.com/archive/cmp/2002/danziger141...