2 ms·

No, that would not satisfy me. It's not that I don't understand the concept you are trying to convey, or even that I disagree with it. What I object to is the

by lisper 5y ago

No, that would not satisfy me. It's not that I don't understand the concept you are trying to convey, or even that I disagree with it. What I object to is the co-opting of the word "type" to mean something other than it means in common usage. I understand that "type system" is a term of art within a certain research community, but this is not that community. HN is much broader than that, and within the context of that audience, "type system" already has an established meaning that encompasses things that happen both at compile time and at run time, and which applies to both terms and data [1]. > 'data' is a runtime concept (some programs might be data, but some others are computations) And how do you distinguish between runtime and non-runtime? It's true that most languages have a distinction between compile-time and run-time but this is purely artificial, a design choice, not a reflection of any deep underlying mathematical truth. Common Lisp notably does not have a sharp distinction between the two. Compilation can trigger macro-expansion, which can in turn trigger arbitrary computations. This process can even loop back on itself: the computations triggered by a macro expansion can themselves invoke the compiler, and can even define new macros. So when you say "Common Lisp does not have a type system" what you really mean is "the structure of Common Lisp is different from what is currently being studied by a group of researchers who have chosen to call the object of their study 'type theory'." The problem with phrasing it the way that you do is that it implies that Common Lisp is lacking something (a type system, according to your narrow definition of what a type system is). It isn't. Common Lisp isn't lacking anything, it is just structured differently. But this is a feature, not a bug, because if you want to avail yourself of the technology of what in academic circles is called "type systems" in Common Lisp you very easily can. But you don't have to. 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". [1] https://en.wikipedia.org/wiki/Type_system https://en.wikipedia.org/wiki/Type_system

lapinot 5y ago
:) 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, ..).
- lisper 5y ago
  > 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.
lapinot 5y ago
tldr of my long response: the misunderstanding between the "common usage" and "some research usage" stems from the belief that by strong/static we mean a restrictive definition (like the common usage of "strong typing"), our "static typing" is much flexible than "strong typing", to the extent that everyone is using some because it's useful.
kazinator 5y ago
... By "output", I mean "static output": a property of the syntax. A programming language in which we don't know what the output will be of every relevant node of the program's graph is "unoutputted". How anyone can tolerate unoutputted languages this day and age is beyond me; don't you want to know that the output is wrong before running the program? We have the tools and everything.
- lisper 5y ago
  Huh? Are you sure you posted this in the right place?

by lisper 5y ago

lapinot 5y ago

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

lisper 5y ago
> 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.

lapinot 5y ago

tldr of my long response: the misunderstanding between the "common usage" and "some research usage" stems from the belief that by strong/static we mean a restrictive definition (like the common usage of "strong typing"), our "static typing" is much flexible than "strong typing", to the extent that everyone is using some because it's useful.

kazinator 5y ago

... By "output", I mean "static output": a property of the syntax. A programming language in which we don't know what the output will be of every relevant node of the program's graph is "unoutputted". How anyone can tolerate unoutputted languages this day and age is beyond me; don't you want to know that the output is wrong before running the program? We have the tools and everything.

lisper 5y ago
Huh? Are you sure you posted this in the right place?