3 ms·

This looks like it's (going to be) about a theory of programming languages as based on some form of the lambda calculus. I think it doesn't get pointed out enou

by mbid 8y ago

This looks like it's (going to be) about a theory of programming languages as based on some form of the lambda calculus. I think it doesn't get pointed out enough that this is not a descriptive science but more of a normative theory with mathematical elements. It doesn't try to analyze and compare existing programming languages. It asserts how they ought to be and derives consequences from this. In this sense, it's less like the theory of evolution and more like a political or aesthetical movement. 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.

pron 8y ago
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.
- chas 8y ago
  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 https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf
- mbid 8y ago
  > 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.
  - 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".
catnaroek 8y ago
> 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”.
- mbid 8y ago
  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.
  - empath75 8y ago
    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.
    - mbid 8y ago
      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.
- pron 8y ago
  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.
tom_mellior 8y ago
> 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: +-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 At this point we're nearing "opaque" territory again.

by mbid 8y ago

pron 8y ago

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.

chas 8y ago
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 https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf
mbid 8y ago
> 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.
- 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".

catnaroek 8y ago

> 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”.

mbid 8y ago
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.
- empath75 8y ago
  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.
  - mbid 8y ago
    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.
pron 8y ago
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.

tom_mellior 8y ago

> 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: +-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 At this point we're nearing "opaque" territory again.