9 ms·

Developing a Statically Typed Programming Language (2017)

143 points by proxybop 7y ago

macintux 7y ago
2017
shpongled 7y ago
Pierce's Types and Programming Languages is a phenomenal textbook. I'm almost done with my implementation of System F-omega (polymorphic lambda calculus with higher kinded types and type operators), featuring a full handwritten lexer/parser with helpful diagnostics. My end goal is to use it as one phase of IR for a functional language compiler.
- azdavis 7y ago
  Another similar book is Harper's Practical Foundations for Programming Languages[1]. I had the privilege of taking a course[2] about this kind of stuff with Prof. Harper at CMU. [1]: https://www.amazon.com/Practical-Foundations-Programming-Languages-Robert/dp/1107150302/ https://www.amazon.com/Practical-Foundations-Programming-Lan... [2]: https://www.cs.cmu.edu/~rwh/courses/ppl/ https://www.cs.cmu.edu/~rwh/courses/ppl/
- proxybop 7y ago
  Congrats!! I’ve been trying to study the basics of type theory but without a more formal background in some of the mathematics/proofs i’m in a little over my head with those books. The red dragon book seems to have simpler / less mathematical explanations of basic type stuff so far
  - shpongled 7y ago
    I have no formal education in type theory (or computer science), but I found the textbook I mentioned to be perfect for self-learning. There are some bits that are over my head (especially the proofs), but I've found it to be exceptionally accessible otherwise.
  - birthdaywizard 7y ago
    I would recommend "Software Foundations" also by Pierce. It covers a lot of the same material but in Coq. I found it much more approachable not having as much of formal background. Having proofs machine checked with error messages is a god send for your sanity when you don't have a professor there to validate you.
Scramblejams 7y ago
Suggest removing the anchor from the link, as it drops you into the middle of the piece. That, or add “Type Rules” to the title.
AdieuToLogic 7y ago
Cool article. While I cannot find the exact quote from Martin Odersky[0], I do believe he once said something along the line of, "it takes about ten years to make a complete typed language." If anyone also recalls this and has a link to the quote, I would much appreciate the pointer to it. 0 - https://en.wikipedia.org/wiki/Martin_Odersky https://en.wikipedia.org/wiki/Martin_Odersky
LessDmesg 7y ago
I started reading but stopped when I saw "succ n" and "prev n". Unary numbers are so academic and disconnected from reality that I lose interest in any paper that uses them. Lambda calculus makes me yawn too. Guess I'll be making a programming language on my own to see how far I get without reading TAPL or any CS papers :-)
- quickthrower2 7y ago
  I found TAPL too hard so I know where you are coming from. I knocked up this programming language in a few hours. https://github.com/mcapodici/badlanguage https://github.com/mcapodici/badlanguage
  - LessDmesg 7y ago
    It's not so hard as it is hard to read because of the formalism. Instead of introducing lambda calculus and the fraction-like thingies with Greek letters, CS scientists should just use Python and write an implementation on the fly.
hhas01 7y ago
Curious: from what I can see, a type system is really just an embedded declarative DSL for doing set algebra. So is there a technical reason why education and implementations always intertwine it with a larger client language, rather than treating it as a complete, self-contained entity in its own right? Or is that lack of decomposition just oversight?
- _se 7y ago
  Try it yourself. It's much more difficult than you seem to think it is.
  - hhas01 7y ago
    Well, isn’t that true of everything? Being a bear of very little brain, it’s why I’m always searching for ways to decompose the larger problem into smaller, simpler, self-contained chunks. Plus, a less common perspective sometimes yields insights that the mainstream may miss. Thanks for the inputs, folks. Will cogitate further.
- chrisseaton 7y ago
  > a type system is really just an embedded declarative DSL for doing set algebra I vaguely remember that there is some maths that tells us that types aren't sets, but can't recall the details. Something to do with Russel's Paradox and function types that refer to themselves as an argument? (I'm not a mathematician.)
- black_knight 7y ago
  Some type systems have set theoretical semantics, but this does not usually correspond to the semantics of the program. For instance the type ∀ A. (A → A) → A would be empty in the set theoretical semantics, but in many programming languages there are terms of this type – the fixed point operator. A better framework for semantics of many programming languages is domain theory[0]. But it also has its limitations. The type system types the terms of the language. Thus it has to be intertwined with them. One of the purposes is to allow only well-typed terms, which then have a better understood semantics. [0]: https://en.wikipedia.org/wiki/Domain_theory https://en.wikipedia.org/wiki/Domain_theory

143 points by proxybop 7y ago

2017

Pierce's Types and Programming Languages is a phenomenal textbook. I'm almost done with my implementation of System F-omega (polymorphic lambda calculus with higher kinded types and type operators), featuring a full handwritten lexer/parser with helpful diagnostics. My end goal is to use it as one phase of IR for a functional language compiler.

azdavis 7y ago
Another similar book is Harper's Practical Foundations for Programming Languages[1]. I had the privilege of taking a course[2] about this kind of stuff with Prof. Harper at CMU. [1]: https://www.amazon.com/Practical-Foundations-Programming-Languages-Robert/dp/1107150302/ https://www.amazon.com/Practical-Foundations-Programming-Lan... [2]: https://www.cs.cmu.edu/~rwh/courses/ppl/ https://www.cs.cmu.edu/~rwh/courses/ppl/
proxybop 7y ago
Congrats!! I’ve been trying to study the basics of type theory but without a more formal background in some of the mathematics/proofs i’m in a little over my head with those books. The red dragon book seems to have simpler / less mathematical explanations of basic type stuff so far
- shpongled 7y ago
  I have no formal education in type theory (or computer science), but I found the textbook I mentioned to be perfect for self-learning. There are some bits that are over my head (especially the proofs), but I've found it to be exceptionally accessible otherwise.
- birthdaywizard 7y ago
  I would recommend "Software Foundations" also by Pierce. It covers a lot of the same material but in Coq. I found it much more approachable not having as much of formal background. Having proofs machine checked with error messages is a god send for your sanity when you don't have a professor there to validate you.

Scramblejams 7y ago

Suggest removing the anchor from the link, as it drops you into the middle of the piece. That, or add “Type Rules” to the title.

AdieuToLogic 7y ago

Cool article. While I cannot find the exact quote from Martin Odersky[0], I do believe he once said something along the line of, "it takes about ten years to make a complete typed language." If anyone also recalls this and has a link to the quote, I would much appreciate the pointer to it. 0 - https://en.wikipedia.org/wiki/Martin_Odersky https://en.wikipedia.org/wiki/Martin_Odersky

LessDmesg 7y ago

I started reading but stopped when I saw "succ n" and "prev n". Unary numbers are so academic and disconnected from reality that I lose interest in any paper that uses them. Lambda calculus makes me yawn too. Guess I'll be making a programming language on my own to see how far I get without reading TAPL or any CS papers :-)

quickthrower2 7y ago
I found TAPL too hard so I know where you are coming from. I knocked up this programming language in a few hours. https://github.com/mcapodici/badlanguage https://github.com/mcapodici/badlanguage
- LessDmesg 7y ago
  It's not so hard as it is hard to read because of the formalism. Instead of introducing lambda calculus and the fraction-like thingies with Greek letters, CS scientists should just use Python and write an implementation on the fly.

hhas01 7y ago

Curious: from what I can see, a type system is really just an embedded declarative DSL for doing set algebra. So is there a technical reason why education and implementations always intertwine it with a larger client language, rather than treating it as a complete, self-contained entity in its own right? Or is that lack of decomposition just oversight?

_se 7y ago
Try it yourself. It's much more difficult than you seem to think it is.
- hhas01 7y ago
  Well, isn’t that true of everything? Being a bear of very little brain, it’s why I’m always searching for ways to decompose the larger problem into smaller, simpler, self-contained chunks. Plus, a less common perspective sometimes yields insights that the mainstream may miss. Thanks for the inputs, folks. Will cogitate further.
chrisseaton 7y ago
> a type system is really just an embedded declarative DSL for doing set algebra I vaguely remember that there is some maths that tells us that types aren't sets, but can't recall the details. Something to do with Russel's Paradox and function types that refer to themselves as an argument? (I'm not a mathematician.)
black_knight 7y ago
Some type systems have set theoretical semantics, but this does not usually correspond to the semantics of the program. For instance the type ∀ A. (A → A) → A would be empty in the set theoretical semantics, but in many programming languages there are terms of this type – the fixed point operator. A better framework for semantics of many programming languages is domain theory[0]. But it also has its limitations. The type system types the terms of the language. Thus it has to be intertwined with them. One of the purposes is to allow only well-typed terms, which then have a better understood semantics. [0]: https://en.wikipedia.org/wiki/Domain_theory https://en.wikipedia.org/wiki/Domain_theory