> I would never say that lisp is not typed! I didn't say you would. What you said was... > > Having dynamic typing != no type system. > Actually no, not in

> I would never say that lisp is not typed! I didn't say you would. What you said was... > > Having dynamic typing != no type system. > Actually no, not in programming language theory. Which implies "having dynamic typing == no type system", which is just wrong, even in programming language theory. These two things are just completely orthogonal to each other. One is a compile-time thing and the other is a run-time thing. Any language can have either, or both, or neither. (And BTW, none of this has anything to do with my original objection, which was your abuse of the phrase "type system".) > the distinction (in lisp still) between something that is quoted (a next-stage computation encapsulated into what is currently data) and current-stage computation is pretty clear I'm sorry, but this is nonsense. Your understanding of Lisp seems to be about 50 years old. The only distinction between "something that is quoted" and something that is not quoted is that the former was produced by the reader (and in CL is stipulated to be immutable, but that is neither here nor there) while the latter may or may not have been. But even the Lisp reader can do arbitrary computations, at least in CL. So I have no idea what "current-stage computation" can possibly mean. You can run your entire program at read-time in Lisp if you want to. > i do believe there is a "deep underlying mathematical truth" in the sense that this sharp definition (typing is static) will help you to understand things because it's a deep concept. No, I disagree. Static typing is nothing more than a particular kind of partial evaluation under a set of constraints and assumptions that adhere to certain conventions. There is no magic in it. The study of type systems is nothing more than the study of the trade-offs that come from different sets of constraints and assumptions and conventions. At the end of the day, bits go in and bits come out, nothing more. Anything beyond that is just in the eye of the beholder. This is not to say that the eye of the beholder doesn't matter, only that the value of any structure you impose on your bit streams, whether you choose to call it a "type system" or not, is necessarily ultimately a subjective assessment, not a mathematical one. > Compilation of call-conventions, memory layout and memory allocation interfaces can be done at scale with type systems Sure, but not because type systems represent a deep mathematical truth, but rather because they constrain the programmer to write code that is easier to compile because it is amenable to certain kinds of partial evaluation. It's kind of like how the existence of roads makes it easier to design certain kinds of cars, and these cars all share certain design features, and this leads to certain significant economic benefits. It does not follow that there is no value in designing vehicles that don't need roads.