jonsterling

I wish to clarify this comment; what I said above is strictly correct, but several people have drawn an undesirable conclusion from it which leads me to find a clarification necessary.

It is not the case that trolling English speakers was the primary motivation of Huet. My understanding is that the trolling was a side-benefit to a name he would have chosen regardless of whether it evinced the double entendre.

In english at least, we call this a “double entendre” ;-)

Obviously the very purpose of double entendres is to troll those who will get the second meaning. duh!

To be clear, this name was chosen by the creator of Coq, Gerard Huet, with the intention of trolling. It wasn't an innocent French word.

There's nothing wrong with mutable data structures from a type soundness perspective. We know how to do it properly. But you need to get the type system right in order to include mutable data structures; often people get this wrong, and it leads to all sorts of frustration...

TypeScript, the language which only just this month added a flag to turn off their completely incorrect subtyping rules for functions! A flag!

I remember reporting this bug years ago, and they said it was "by design, since JS programmers prefer to think of functions as covariant in their input". Well, I prefer to think of 2+2 as equalling 5.

Not only this, but strangely it doesn't use standard methods or names in the categorical understanding of computer science. All this business about "CompFunc" as a category of sets and computable functions, but I see nothing about partial combinatory algebras or realizability.

For some of my documents which use opentype fonts, the difference is by a factor of 20-30 between xelatex and lualatex.

I think it is not just a minority opinion, but just plain wrong.

> I have to admit I have no idea what racket is, nor did I do much more than scan the article.

why have you commented then? Mao Zedong had a dope saying about this, "No investigation, no right to speak!"

-----------------------------

One answer to your questions, btw, is that macros are useful and interesting regardless of what kind of type system you have. Haskell has something called Template Haskell, which is really quite bad for a number of reasons, but it is certainly possible to imagine a version of Haskell with a well-designed macro system. It just so happens that Racket has an exceptionally well-designed macro system, so the partnership of the two ideas is very plausible and scientifically interesting.

Macros and types are not in opposition. However, macros induce a notion of PHASE which is not usually accounted for in type systems, though it may be possible to account for this in a principled/type-theoretic way using ideas from modal logic and kripke semantics.

You went straight from saying, “Don't assume I'm a running dog!” to literally proving that you are a running dog! So cool.

This is not true. Some of the best papers ever, I have benefited from reading many times, more than three.

You (and I) are not in the target audience for those books. She does very serious mathematics, which should be defended; she gave a very nice talk on Trimble n-categories to my research group on Friday, for instance.