4 ms·

> It doesn't assert how they ought to be (theorists, like everyone else, may express their opinion but this is not what the theory studies). It is a study of fo

• rntz 8y ago
  > Most of the type systems studied are not used in the wild, so they can't be interesting because they describe something people are already interested in. The only other possible explanation for the relevance of these papers is that the authors hope to improve upon what already exists. Your argument here amounts to: if it's not descriptive, it must be prescriptive. By this argument, the entirety of pure mathematics is prescriptive. Is the idea of a semiring a description of a particular natural object? But it makes little sense to claim the idea of semirings is normative. After all, math studies many structures that don't satisfy the semiring laws, as well! Likewise, computer science studies many forms of "computation" which aren't physically realistic. Is computational complexity theory "normative" in studying Turing machines, or PRAM machines? No, they are merely convenient abstractions which get at the essence of a particular problem. The lambda calculus is similar: it is a convenient abstraction which gets at the essence of a particular way of computing. It's a useful starting point for a certain kind of PL theory because its semantics are relatively simple. But it's certainly not the case that all PL theory studies the lambda calculus. PL theory includes work on verification of imperative programs; on macro expanders; on compilation techniques; and on pure logic. What is certainly true is that many people who study PL theory do have normative (usually aesthetic) ideas about PL design, and these seep into the kinds of systems they tend to study. I agree that computer science isn't a natural science. But it isn't as simple as "anything not descriptive is normative", or that (quoting a sibling comment) PL theory is just "a theory of some variant of the lambda calculus".
  • mbid 8y ago
    > Your argument here amounts to: if it's not descriptive, it must be prescriptive. By this argument, the entirety of pure mathematics is prescriptive. Is the idea of a semiring a description of a particular natural object? But it makes little sense to claim the idea of semirings is normative. After all, math studies many structures that don't satisfy the semiring laws, as well! Yes, to some extent, mathematics is prescriptive. Publishing a paper on semirings or computable functions means that you think these objects are interesting and should be studied. But pure mathematicians usually stop here, they don't pretend their research has value because it related to the real world somehow. It's just supposed to be interesting on its own. On the other hand, type theorists push their theory with the expectation that it is useful for creating computer programs despite decades of contrary, if any, evidence. I wouldn't mind types studied the same way that, say, first order predicate logic is studied. The fact that most of the type theory researchers seem to hail from CS departments seems to suggest that types would simply fade into irrelevance however. I also see a difference in the extent that mainstream mathematics is prescriptive vs descriptive. Certainly you would agree that most mainstream maths, say number theory or differential topology, is much less definition-heavy than type theory is. And most definitions in pure maths have auxiliary character, they are only interesting in that they help clarify proofs. Sometimes it happens that definitions turn from auxiliary to interesting in their own right; this happens mostly when the same construction makes sense in multiple context. In type theory, on the other hand, definitions, and not of the auxiliary kind, make up most of the work. The proofs are usually mere bureaucracy, with definitions set up so that the facts the researcher wants to hold do so essentially by definition. Thus the definitions, i.e. the prescriptive part, is really the main contribution of type research. > But it's certainly not the case that all PL theory studies the lambda calculus. PL theory includes work on verification of imperative programs; on macro expanders; on compilation techniques; and on pure logic. Well, the linked document is called "PL theory", so I simply assumed that it would cover all of it to some depth and not just a particular subfield. May impression is that the "type" paradigm is the dominant one in PL research and I simply assumed the authors of the linked paper have the same impression given their selection of material. I certainly didn't mean to discredit the other fields you mentioned, I simply can't have an informed opinion about them.
• pron 8y ago
  Most researchers are advocates for their work, but you're right that Wadler is more vocal and enthusiastic in his advocacy than many (but maybe less than others, like Bob Harper). Programming language theory is unable -- and does not attempt to -- assign a value to languages, to say which is good and which is bad (even assuming such a value exists and isn't completely contextual); programming language theorists, on the other hand, can have personal preferences like anyone else. I agree that PL theorists, perhaps more than others, like to blur the wide gap between theory and practice, their preference and their research, sometimes even in a way that can detract from their work. As to confusion about types, you are also right (and I wasn't assuming anything). What types are in a formal language is pretty clear: they're syntactic derivation rules for determining which terms are well-formed by assigning them sorts. This is what theorists who study typed languages mean when they say "type". However, in programming types play several roles, some or all of them are also served by other mechanisms, like dynamic types (which are not formal types at all), and so there are different types of types.