:) i was waiting for you to come all lisp on me! (eh i just realized your pseudo) [sorry for the long msg, i like this topic!] But this is just all staging! I

:) i was waiting for you to come all lisp on me! (eh i just realized your pseudo) [sorry for the long msg, i like this topic!] But this is just all staging! I would never say that lisp is not typed! Only perhaps streaming lisp interpreters (perhaps like lisp machines, don't know them very well) could be said truly untyped (actually: trivially statically typed). Dynamic vs static is more precisely seen as a sequentiality between stages, and you can have several stacked stages and even looping (as in lisp). But 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. Some function bodies eval quoted stuff and some build quoted computations and you can statically see that: you can type it (using a quoted vs normal modality on top of any type system you already have). We could also talk about erlang. In fact the trend is that for every convoluted language semantic that has traditionally been seen as dynamic/permissive/untyped, the research oriented world has come up with type systems explaining these languages. I talked about gradual typing earlier in the thread. There is static typing for memory state, complexity constraints, timing, validating interface checks, for well-typed macros and syntax reflection. Typing in some way is just structuring the mathematical semantic of your language. It can always be done, even after the fact, usually in tons of different ways. I see where you come from, but still, actually 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. And as any deep concepts usually when you think you hit it's limit, you understand that you can generalize it into something that is more abstract but still has the core properties. The concept is still there, just said in more precise terms (more precise, because you're taking more parameters and leaving more irrelevant choices open in the concept, hence more abstract). > In fact it is so-called "strongly typed" language that are lacking something, namely, the freedom to write code that does not conform to the constraints of the "type system". This is wrong if by "strongly typed" you mean the term of art: you'd have to be willing to go out of your way to write a compiler for a language without any appearance stuff that could be qualified static typing. Static scoping and dependency analysis is a strong type system where types are the number/name of free variables. Compilation of call-conventions, memory layout and memory allocation interfaces can be done at scale with type systems (the llvm one is well-known, you'd be quite in the minority saying that llvm constrains you not to write your "untypable" self-mutating program). For most part, in practice, type systems are not a feature of the language but of the compiler, as for tons of cool systems, types can be infered (by a complete deciding procedure). Static type systems are just the fact that you will annotate programs with some local invariants, whatever they might be, to ease manipulating and reasoning on some form of term representation (AST, call-graph, ..).