7 ms·

I study type systems and programming language theory at university, and I encourage friends studying CS to at least have some understanding of type theory, such

I study type systems and programming language theory at university, and I encourage friends studying CS to at least have some understanding of type theory, such as well-known type systems (simply-typed, System F) and properties like soundness or uniqueness of typing. Why? Because as programmers we argue to death comparing the expressiveness and properties of type systems of our favorite programming languages, or we're picking up a language with features like traits or type inference. Type theory really lets you learn the heart of such features in a small, idealistic setting and specifies things rigorously and uniformly, (since languages tend to come up with their own names and examples for things like ad-hoc polymorphism, AKA typeclasses/traits/protocols/concepts), and they appear no matter the paradigm.

duped 5y ago
The notation is an insurmountable barrier to many.
- lapinot 5y ago
  Looking at java, rust or assembly i find this argument hard to swallow ;) It's really worth it to learn some sequent calculus basics to be able to read typing rules. Its mostly the same thing as a grammar, or a weird inductive type ("enum").
  - duped 5y ago
    It shouldn't be hard to swallow. Monospaced ascii text that is (usually) unambiguous with extensive documentation is night and day from formal notation. At least BNF grammars are legible
  - klibertp 5y ago
    Look at APL, K, and J. The notation based on keywords is not a problem; the problematic notations are the ones which abuse strange characters or ideograms, because they require you to re-learn the process of reading.
- steego 5y ago
  It's interesting how calling it insurmountable both panders to and insults the people you're talking about. Maybe a better way to describe the notation is "off-putting"?
  - duped 5y ago
    It's not supposed to be insulting. I think the notation is more than offputting, and describing it as a barrier to entry is appropriate. Like many kinds of formal notation it almost requires a class in a university to have it explained. The same is true of other fields dense in notation where you need to learn the conventions as much as the basics.
    - BlackFingolfin 5y ago
      In my experience, any sufficiently deep study of any subject requires introduction of at least some degree of specialized terminology ("jargon") to be able to express things precisely and concisely. Sure, you can try to avoid this and use just "generic" language, but you almost always have to sacrifice one or both of these, at least partially. That can very well be worth it in certain cases (e.g. in an introductory text). But the site being discussed here is a list of specific (counter)examples. It would seem counterproductive to me to "dumb it down" given that it's primary purpose seems to be to discuss very specific situations; indeed, one common feature among many of these examples are subtle differences in what things mean in different parts of a language specification -- i.e., one of the reasons why domain experts invariably start using jargon. That said, of course jargon often is als abused, or used in cases it doesn't have to be, etc. -- that's s bad! And many papers and books suffer from this and would be improved by using less jargon. But in general I find this negative stance against formal notation, and the expectation that one should be able to dive into subtle and advanced examples without a need of at least some "studying" (not at all necessarily at a university!) quite odd, and unrealistic.
      - klibertp 5y ago
        My main question here is: why is conciseness a good thing? Precision is a must, no argument here, but conciseness, to me, seems like a premature, and harmful, optimization. Is it really that much harder to stay within standard ASCII(EDIT: I mean "stay within the characters that the reader already knows how to read", which on the second thought doesn't have to be ASCII at all...)? Do you really need to express concepts with a single strange character? What does it buy you, given that the downsides for readability are quite obvious? There are arguments that using a full word for something would be confusing due to other/overloaded meanings of the word, but then I go read some papers and I see the same ideograms used in drastically different meanings, too. Jargon is ok. Jargon is what happens when you want to be precise while re-using brain machinery for reading. The exotic notations are, on the other hand, just jargon put in a form which you have to (re)learn how to read, for the sake of conciseness alone. That conciseness may pay off if you're going to be working with the notation 8h/day for 10 years (or a year, or maybe even half a year), but if you just want to read and understand concepts and learn facts... To paraphrase: you wanted a banana, but what you got was gorilla holding the banana and the whole jungle along with it. Hence my question: isn't creating exotic, one-character == 2.5 concepts, notations simply optimization which is harmful to the vast majority of potential readers?
- siraben 5y ago
  Many introductory texts, such as Types and Programming Languages explain the notation thoroughly and start really simple, even starting from the inference rule notation, then talking about reduction of untyped arithmetic expressions, building up to the standard notation type theory.
- BugsBunny1991 5y ago
  I think it's easier to do if you work up to it gradually. I read Logic by Wilfrid Hodges a few years back on a whim from some recommendation on HN. I didn't think much of the book at the time, though I recently picked up Benjamin Pierce's Types and Programming Languages. Having seen notation like that before made digesting the book much easier (along with starting with other introductory texts like Friedman and Wand's Essentials of Programming Languages).
  - siraben 5y ago
    Yeah, Essentials of Programming Languages is also another great implementation-oriented text, it has some formal things like inductive sets (which pop up in PLT anyway) and also lots of programming exercises.
- agumonkey 5y ago
  ah notation is such a subtle and often sad topic when you click you never give a damn about notation but before you do it's such a drag it's like monads
- smasher164 5y ago
  The notation really isn't as bad as it originally looks, trust me. I was in the same boat recently, but after cracking open TAPL, on page 26 you basically get all the notation you need for the rest of the book. Inference rules just transform the traditional format of (A && B) -> C into A B --- C This format allows you to stack rules on top of each other when writing out the derivation of some term, without running out of page space.
  - duped 5y ago
    It seems absurd to care about 'page space' when discussing computer science notation...
chestervonwinch 5y ago
What is a good an introductory text (or other resource) for learning? What's the relationship between programming language theory and type theory? Is type theory a special topic, or would it be considered a core topic in programming language theory (e.g., like integration in calculus)?
- pansa2 5y ago
  > What is a good an introductory text (or other resource) for learning? The usual recommendation seems to be "Types and Programming Languages" by Benjamin C. Pierce.
- cle 5y ago
  I love “Types and Programming Languages” by Benjamin Pierce and always recommend it for people who want to dip their toes into formal type theory. To me it’s basically the K&R for type theory.
- codeismath 5y ago
  I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university but have picked up many books along the way. I'm usually quite lost within the first 10 or 20 pages until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube. But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it. If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.
- siraben 5y ago
  As others have said, I also recommend Types and Programming Languages. > What's the relationship between programming language theory and type theory? I'd say programming language theory is more broad than type theory, for instance topics such as compilation techniques and runtime systems are more distant from type theory (though you might prove some type-theoretic thing like type preservation). There's also a range of type theory books because it's a field that spans pure logic to programming languages, so you can find books like Type Theory and Functional Programming by Thompson that elaborate things like dependent types early on.

duped 5y ago

The notation is an insurmountable barrier to many.

lapinot 5y ago
Looking at java, rust or assembly i find this argument hard to swallow ;) It's really worth it to learn some sequent calculus basics to be able to read typing rules. Its mostly the same thing as a grammar, or a weird inductive type ("enum").
- duped 5y ago
  It shouldn't be hard to swallow. Monospaced ascii text that is (usually) unambiguous with extensive documentation is night and day from formal notation. At least BNF grammars are legible
- klibertp 5y ago
  Look at APL, K, and J. The notation based on keywords is not a problem; the problematic notations are the ones which abuse strange characters or ideograms, because they require you to re-learn the process of reading.
steego 5y ago
It's interesting how calling it insurmountable both panders to and insults the people you're talking about. Maybe a better way to describe the notation is "off-putting"?
- duped 5y ago
  It's not supposed to be insulting. I think the notation is more than offputting, and describing it as a barrier to entry is appropriate. Like many kinds of formal notation it almost requires a class in a university to have it explained. The same is true of other fields dense in notation where you need to learn the conventions as much as the basics.
  - BlackFingolfin 5y ago
    In my experience, any sufficiently deep study of any subject requires introduction of at least some degree of specialized terminology ("jargon") to be able to express things precisely and concisely. Sure, you can try to avoid this and use just "generic" language, but you almost always have to sacrifice one or both of these, at least partially. That can very well be worth it in certain cases (e.g. in an introductory text). But the site being discussed here is a list of specific (counter)examples. It would seem counterproductive to me to "dumb it down" given that it's primary purpose seems to be to discuss very specific situations; indeed, one common feature among many of these examples are subtle differences in what things mean in different parts of a language specification -- i.e., one of the reasons why domain experts invariably start using jargon. That said, of course jargon often is als abused, or used in cases it doesn't have to be, etc. -- that's s bad! And many papers and books suffer from this and would be improved by using less jargon. But in general I find this negative stance against formal notation, and the expectation that one should be able to dive into subtle and advanced examples without a need of at least some "studying" (not at all necessarily at a university!) quite odd, and unrealistic.
    - klibertp 5y ago
      My main question here is: why is conciseness a good thing? Precision is a must, no argument here, but conciseness, to me, seems like a premature, and harmful, optimization. Is it really that much harder to stay within standard ASCII(EDIT: I mean "stay within the characters that the reader already knows how to read", which on the second thought doesn't have to be ASCII at all...)? Do you really need to express concepts with a single strange character? What does it buy you, given that the downsides for readability are quite obvious? There are arguments that using a full word for something would be confusing due to other/overloaded meanings of the word, but then I go read some papers and I see the same ideograms used in drastically different meanings, too. Jargon is ok. Jargon is what happens when you want to be precise while re-using brain machinery for reading. The exotic notations are, on the other hand, just jargon put in a form which you have to (re)learn how to read, for the sake of conciseness alone. That conciseness may pay off if you're going to be working with the notation 8h/day for 10 years (or a year, or maybe even half a year), but if you just want to read and understand concepts and learn facts... To paraphrase: you wanted a banana, but what you got was gorilla holding the banana and the whole jungle along with it. Hence my question: isn't creating exotic, one-character == 2.5 concepts, notations simply optimization which is harmful to the vast majority of potential readers?
siraben 5y ago
Many introductory texts, such as Types and Programming Languages explain the notation thoroughly and start really simple, even starting from the inference rule notation, then talking about reduction of untyped arithmetic expressions, building up to the standard notation type theory.
BugsBunny1991 5y ago
I think it's easier to do if you work up to it gradually. I read Logic by Wilfrid Hodges a few years back on a whim from some recommendation on HN. I didn't think much of the book at the time, though I recently picked up Benjamin Pierce's Types and Programming Languages. Having seen notation like that before made digesting the book much easier (along with starting with other introductory texts like Friedman and Wand's Essentials of Programming Languages).
- siraben 5y ago
  Yeah, Essentials of Programming Languages is also another great implementation-oriented text, it has some formal things like inductive sets (which pop up in PLT anyway) and also lots of programming exercises.
agumonkey 5y ago
ah notation is such a subtle and often sad topic when you click you never give a damn about notation but before you do it's such a drag it's like monads
smasher164 5y ago
The notation really isn't as bad as it originally looks, trust me. I was in the same boat recently, but after cracking open TAPL, on page 26 you basically get all the notation you need for the rest of the book. Inference rules just transform the traditional format of (A && B) -> C into A B --- C This format allows you to stack rules on top of each other when writing out the derivation of some term, without running out of page space.
- duped 5y ago
  It seems absurd to care about 'page space' when discussing computer science notation...

chestervonwinch 5y ago

What is a good an introductory text (or other resource) for learning? What's the relationship between programming language theory and type theory? Is type theory a special topic, or would it be considered a core topic in programming language theory (e.g., like integration in calculus)?

pansa2 5y ago
> What is a good an introductory text (or other resource) for learning? The usual recommendation seems to be "Types and Programming Languages" by Benjamin C. Pierce.
cle 5y ago
I love “Types and Programming Languages” by Benjamin Pierce and always recommend it for people who want to dip their toes into formal type theory. To me it’s basically the K&R for type theory.
codeismath 5y ago
I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university but have picked up many books along the way. I'm usually quite lost within the first 10 or 20 pages until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube. But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it. If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.
siraben 5y ago
As others have said, I also recommend Types and Programming Languages. > What's the relationship between programming language theory and type theory? I'd say programming language theory is more broad than type theory, for instance topics such as compilation techniques and runtime systems are more distant from type theory (though you might prove some type-theoretic thing like type preservation). There's also a range of type theory books because it's a field that spans pure logic to programming languages, so you can find books like Type Theory and Functional Programming by Thompson that elaborate things like dependent types early on.