Programming Language Theory in Agda(wenkokke.github.io)
wenkokke.github.io
Programming Language Theory in Agda
https://wenkokke.github.io/sf/
13 comments
> I found agda much less opaque than coq and especially isabel.
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:
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 doesn't try to analyze and compare existing programming languages.
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”.
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”.
Programming language theory has no concept of "correctly-" or "incorrectly-designed." It may show some properties of some languages, and researchers may express their opinion that they believe those properties are inadvisable for programmers. Programming language theory does not define a metric for what's good or bad, and, in fact, programmers are often (though not always) better judges of that than theorists.
I certainly didn't mean to imply that the programming languages ignored by these reasearchers are any good, on the contrary. It's just that I find the way these researchers sell themselves questionable. They don't have a theory of programming languages, they have a theory of some variant of the lambda calculus. It would be more honest to call it just that.
The lambda calculus is a very simple set of rules which is Turing complete— whichever kind of programming language you prefer can be broken down to lambda calculus.
Let me clarify---some version of typed lambda calculus. The document linked here doesn't seem to deal with the untyped lambda calculus and much less so with properties that are stable under change of representation of computable function.
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 formal systems; basically, it's formal logic under a different name: A formal system is defined, and its properties studied; another system is defined and its properties are studied, and so on.
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.
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 think Practical Foundations for Programming Languages [0] does a good job on that front.
[0] https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf
[0] https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf
> 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 formal systems; basically, it's formal logic under a different name: A formal system is defined, and its properties studied; another system is defined and its properties are studied, and so 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.
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.
> 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".
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".
> 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.
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.
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.
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.
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.