ionfish

Here is the cartoon Knuth refers to.

http://www.danzigercartoons.com/archive/cmp/2002/danziger141...

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.

https://github.com/beastaugh/hatt/blob/1.5.0.3/src/Data/Logi...

Then there are other modules like Parser which just exposes a single function, but of course makes use of the core types.

https://github.com/beastaugh/hatt/blob/1.5.0.3/src/Data/Logi...

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.

https://github.com/beastaugh/hatt/blob/1.5.0.3/src/hatt.hs

It's pretty common in the UK these days.

No, the default backend is the native code generator. You need to use the -fllvm flag to enable the LLVM backend.

http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/code-...

"[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."

Coming from a set-theoretic perspective, I suppose I've got so used to Tarski's theorem that I consider it intuitive.

As far as Tychonoff's theorem goes, you might find this paper interesting:

http://matwbn.icm.edu.pl/ksiazki/fm/fm113/fm11313.pdf

Lots. For example, that every set has a cardinality (is bijective with some aleph). That's pretty intuitive, too, as (I think) are the following.

* Let X and Y be sets. Then either they have the same cardinality, or one is smaller than the other.

* Let X be an infinite set. Then there is a bijection between X and the cartesian product of X with itself, X × X.

* Tychonoff's theorem: every product of compact topological spaces is compact.

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.

I don't care that nobody cares. I care that they pretend that they do. Fake friendliness is annoying, and good service is not formulaic.

AC is equivalent to a lot of things. There's a collection of them on the Wikipedia page.

http://en.wikipedia.org/wiki/Axiom_of_choice#Equivalents

Something I find pretty interesting is that some of these equivalences break down in weak systems.

http://www.math.uchicago.edu/~antonio/RM11/RM%20talks/mummer...

The history of the proof is a little messy; the Wikipedia page has a decent summary.

http://en.wikipedia.org/wiki/Cantor–Bernstein–Schroeder_theo...

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.

That's a really nice way to show that, thanks. I may borrow it for future use.

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).

The set of fractions isn't larger than the set of whole numbers, so how good an explanation could it be?

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.

You probably shouldn't. :)

Oh, I think it was mainly trivial stuff. I'm afraid I don't remember the specifics, this was two years ago.

Yes, although there is one subtlety here: should `flip` return a curried function, or an uncurried function? This isn't an issue in Haskell since it only has unary functions.

Yes, it does. This is true in Haskell too, of course.

    subtract :: (Int, Int) -> Int
    subtract (n, m) = n - m
    
    fiveMinus = (curry subtract) 5
    minusFive = ???
    
    subtract' = \n m -> n - m
    fiveMinus =   \m -> 5 - m
    minusFive =   \m -> m - 5

It has a few more functions that operate on lists, but it's missing a lot of the general utility functions that Underscore has.

Roy looks interesting, thanks for the link.

It seemed unnecessary, yes, although I suppose there are possibly some circumstances where one might want a `first` function—for example if one were folding over a list of lists.

That's very cool, although you have to use another dialect of JavaScript if you want to modify the source code, with all the disadvantages that entails.

Patches for these would be welcome; I did mean to add them, but I got distracted by other projects, and then by my PhD.

To be honest, I completely agree with you. But it wouldn't be a JavaScript functional programming library if it didn't have the curry function.

I'm pretty familiar with Underscore, just wasn't happy with a couple of the design decisions, otherwise I would have just used that. Udon actually came out of various hacky functional JS libraries that I'd written over the years, and part of the motivation was to pull those together into a clean and coherent codebase.

Of course it would. Patches which improved the documentation would be very welcome.