Programming Language Theory in Agda
wenkokke.github.io
wenkokke.github.io
Wadler himself seems to dislike calling this "computer science": "You don't put science in your name if you're a real science." I'm quite sure he meant it differently, but it fits my argument to quote him out of context :)
The book itself is still unfinished obviously. Most of it seems to be a formalization of the absolute basics of constructive logic currently. I'm also not sure how far they are really going to go here; feasibly formalizing the meta theory of agda (Martin-Löf type theory) in agda itself seems to be an open problem. Yes, seriously.
I found agda much less opaque than coq and especially isabel. It seems much more cumbersome to work with in practice though. I doubt agda will ever be used for serious proofs beyond hello world or very specialized areas as long as there is not more automation... at which point you're back at a variant of coq.
Unfortunately, most texts on PL theory, and this one does not seem to be an exception, do not explain what a formal system is -- namely what syntax is, what semantics is, and what the relationship between them is. This leads to confusion later on.
This document is called "programming language theory". I would expect from this the study of programming languages in general. Yet only a tiny fraction of programming languages are studied, namely exactly one: The simply typed lambda calculus. So I think it's fair to say that the authors seem to think that the the simply typed lambda calculus is absolutely central. Yet among existing programming languages with real world adoption, the pure simply typed lambda calculus is completely irrelevant. Nobody programs in it. So I can't take this as a description of the status quo of "programming languages". Then how am I to interpret the mere existence of this, if not as an endorsement?
> Unfortunately, most texts on PL theory, and this one does not seem to be an exception, do not explain what a formal system is -- namely what syntax is, what semantics is, and what the relationship between them is. This leads to confusion later on.
I doubt you'll find a general definition of what a type system is. You'll find many examples, sure, but no general definition. (BTW, thanks for assuming I'm confused about this. I think I've talked with enough type theory researchers to conclude that they are the confused ones.) Case in point: The plethora of papers whose first sections have to introduce the type system in question. This also relates to your first point, where you argue that PL theory is not normative. If the type theory in question has to be introduced, it automatically means that the reader has to be convinced that what he's reading is not just random noise encoded as formulae and proofs. 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.
Finally, take some of Wadler's papers. If "Theorems for free" (spoiler: the theormes there are not freer than other theorems) or "Linear types can [!] change the world" are not endorsements, I don't know what is.
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".
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.
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.
Could you explain what you mean by opaque? In Coq you have to memorize a number of tactic names, and if you don't know the tactics, reading a proof script is useless. And even if you do, it's really hard to reconstruct the proof state in your head from reading the tactic script. So I guess that's "opaque", but I don't see how Agda proof terms are more transparent.
I find Isabelle/Isar proof scripts reasonably readable in contrast. But I don't think we have found the good proof assistant yet. (Note to self: Check out Lean already.)
EDIT: Ah, forgot about the equational proof style in Agda. That's nice. Pretty much the same is available in Isabelle too. And the niceness breaks down quite quickly:
+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ m zero rewrite +-identity′ m = refl
+-comm′ m (suc n) rewrite +-suc′ m n | +-comm′ m n = refl
It does. For example, this theory identifies when and how incorrectly designed programming languages fail to enforce abstractions, very much like how the theory of database normalization identifies when and how incorrectly designed database schemata fail to enforce data integrity constraints.
But perhaps what you mean is “it doesn't try to view existing programming languages under an unwarranted positive light”.