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.
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.
> 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 (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.
Sorry for my harsh comment; here's what I'm thinking of...
In math, you are dealing with many different kinds of object, not just numbers. In fact, one of the big realizations that led to modern mathematics is that not all mathematical objects can even be coded as numbers!
Your remark about "arrow" being more general than function is correct; but functions do not map only between sets of numbers, but between arbitrary sets, some of which contain elements that are not numbers, or even encodable as such.
Hmm, I think you should aim for sentences to be correct on their own and be arranged such that understanding & precision is built incrementally (in the way you suggest). This is harder, but that's what good writing does---I want my "simplified" parts to be real approximations of the precise parts; we mustn't settle for the simplifications failing to approximate the precise versions.
It may be easy for experts to avoid getting confused by a literally false claim, which is clarified in the next paragraph. But your paper will often be read by people who are not experts in the paper's topic, so some will end up being confused by this.
It's stressful for me to read that kind of paper, since it causes a lot of cognitive dissonance as you read! Maybe it's not like that for everyone, but I prefer to read papers that don't use the approach you appear to suggest.
That paper is just a bit of bureaucracy which demonstrates that total programs behave the same in a total language as when they are embedded into a partial language (which is an intuitive result, and it's nice that they worked out the details!). It's also a nice demonstration of the logical relations proof technique.
But sadly this paper is pulled out all the time by people who I suspect don't understand what is going on, to justify sleight of hand & dodgy reasoning which has little to do with the result in the paper. (Not claiming that's what's happening in the above comment! But I bristle a bit when I see this paper come up in amateur/Haskell circles.)
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.