3 ms·

I’ve heard a lot of recommendations for this book from programming language designers - is it (and the subjects it covers) useful for everyday programmers (i.e.

by pansa2 5y ago

I’ve heard a lot of recommendations for this book from programming language designers - is it (and the subjects it covers) useful for everyday programmers (i.e. language users), or just for language designers? For the latter, I assume type theory would be essential if you’re trying to design a language like Haskell, but irrelevant if you’re trying to design a dynamically-typed language like JavaScript? Would it be useful for the designers of “in-between” languages, like Java or Go?

keskadale 5y ago
> if you’re trying to design a dynamically-typed language like JavaScript i think the first lesson on programming language design is to not design a language like javascript
- pansa2 5y ago
  OK then, Lua. Or Python before type hints.
  - BlackFly 5y ago
    So it starts from the generic untyped lambda calculus and then shows that it is possible to reach erroneous states: so far so much like any dynamically typed language (so javascript, lua, python). Bear in mind javascript is also quite weakly typed, but that doesn't matter much for the point I am trying to elucidate. You introduce types to try to describe the program state in a way that a static analyser is able to prove that the program will not reach erroneous states. You learn that types limit computing: the simply typed lambda calculus always halts. Note that a human reader is a type of static analyser. You start introducing more advanced types to try to get back that unbounded possibility: to be a real programming language, you need the halting problem--a real server doesn't halt. Anyways, after some chapters you learn that you may need a lot of rather advanced type theory to truly describe some of the complex things that some crazy people did in previously dynamically typed languages. That's why python type hints and typescript sometimes (but not usually) need some really crazy stuff: people were able to and did do all kinds of crazy things. Arguably, there are easier ways to solve a problem than the way that requires advanced type theory to describe. The dynamic languages don't make it easier to write, verify and reason about such code other than the fact that many static languages prevent it outright.
- awestroke 5y ago
  Why?
  - caaqil 5y ago
    There is the obvious error of thinking that JS was designed.
bjourne 5y ago
This type of questions - "is this knowledge useful?" - is hard to answer. Is music theory useful for musicians? But Jimi Hendrix didn't know music theory! You can get by without reading this book, most language designers probably hasn't read it either, and lots of programming languages were invented long before type theory was a real thing. The formalisms introduced in the book are absolutely applicable to dynamically typed languages (such as JavaScript) and "less strict" statically typed languages like Java and Go. The book teaches you that there is a logic framework which you can use to analyze any programming language you can think of. It's not something you use in everyday life but it is very interesting!
- jpitz 5y ago
  Jimi Hendrix may not have had a conventional education in music theory, but it seems obvious to me that he had an internalized model of it.
  - rsrsrs86 5y ago
    This. You do not need music theory if you have a very special ability to know what sounds come from your playing. It becomes muscle memory. And you need a pretty good ear.

by pansa2 5y ago

keskadale 5y ago

> if you’re trying to design a dynamically-typed language like JavaScript i think the first lesson on programming language design is to not design a language like javascript

pansa2 5y ago
OK then, Lua. Or Python before type hints.
- BlackFly 5y ago
  So it starts from the generic untyped lambda calculus and then shows that it is possible to reach erroneous states: so far so much like any dynamically typed language (so javascript, lua, python). Bear in mind javascript is also quite weakly typed, but that doesn't matter much for the point I am trying to elucidate. You introduce types to try to describe the program state in a way that a static analyser is able to prove that the program will not reach erroneous states. You learn that types limit computing: the simply typed lambda calculus always halts. Note that a human reader is a type of static analyser. You start introducing more advanced types to try to get back that unbounded possibility: to be a real programming language, you need the halting problem--a real server doesn't halt. Anyways, after some chapters you learn that you may need a lot of rather advanced type theory to truly describe some of the complex things that some crazy people did in previously dynamically typed languages. That's why python type hints and typescript sometimes (but not usually) need some really crazy stuff: people were able to and did do all kinds of crazy things. Arguably, there are easier ways to solve a problem than the way that requires advanced type theory to describe. The dynamic languages don't make it easier to write, verify and reason about such code other than the fact that many static languages prevent it outright.
awestroke 5y ago
Why?
- caaqil 5y ago
  There is the obvious error of thinking that JS was designed.

bjourne 5y ago

This type of questions - "is this knowledge useful?" - is hard to answer. Is music theory useful for musicians? But Jimi Hendrix didn't know music theory! You can get by without reading this book, most language designers probably hasn't read it either, and lots of programming languages were invented long before type theory was a real thing. The formalisms introduced in the book are absolutely applicable to dynamically typed languages (such as JavaScript) and "less strict" statically typed languages like Java and Go. The book teaches you that there is a logic framework which you can use to analyze any programming language you can think of. It's not something you use in everyday life but it is very interesting!

jpitz 5y ago
Jimi Hendrix may not have had a conventional education in music theory, but it seems obvious to me that he had an internalized model of it.
- rsrsrs86 5y ago
  This. You do not need music theory if you have a very special ability to know what sounds come from your playing. It becomes muscle memory. And you need a pretty good ear.