Hacker News Reader

I did think about trying to sneak a type checker in here too, but it's just too much for a first book on languages and interpreters.

If you're looking for a book on statically typed functional languages, I think Appel's book[1] is canon. From what I've heard, the C and Java ones aren't very great. It's worth learning enough ML to get through that version because ML is clearly the language Appel thinks in.

[1]: http://www.cs.princeton.edu/~appel/modern/

> 20-30 year-old textbooks

I assume you're talking about something like "Modern Compiler Implementation in ML"? That book is still a good starting point, and once you get a basic implementation going you'll be in a good position to start learning about and implementing more advanced features. You'll end up teaching yourself as you figure out how to add features to your own codebase.

edit: fix title

You definitely want https://www.cs.princeton.edu/~appel/modern/ml/.

There's nothing more "advanced" about statically typed languages. Static typing and type inference are straightforward and can make implementation details simpler than dynamic languages (because you're greatly reducing or removing the unknowns you have to deal with at runtime). This is assuming you're making a batch-style compiler, as most implementors do, and not an interactive system.

If you're focused on benchmark numbers, dynamically typed languages are much more challenging to squeeze performance out of better code generation.

You can also add static type inference and consistency checking to a dynamic language, and indeed some systems do in the name of better

I meant "advanced static-typing" (e.g, like System F, which is advanced to someone learning PL). Not that it was more advanced, although I think in fact it is from a learner's point of view. It's incredibly simple to throw together a Scheme, or even a more complex interpreted dynamic language.

Add in a static typing, type inferencing, and type checking, and that all becomes much more complicated, at least from this learner's point of view. From how highly upvoted my comment is, I suspect I'm far from being alone here. Learning, understanding, and implementing Hindley-Milner by itself was harder for me than learning how to put together a basic interpreter for a simple scheme. And I think a big part of that is the dearth of learning materials for things like Hindley-Milner and related concepts, whereas there are 100 books and tutorials on how to implement a Scheme interpreter in language X.

Finally, if you're talking about language performance, then yes clearly it's much harder to squeeze performance out of dynamic languages. But I'm talking about learning exercises here, not production programming languages.

   dearth of learning materials for things 
   like Hindley-Milner

What's wrong with the original paper [1]? It's really basic and boiled down to the essence (in true Milner style). I give it to all my students interested in typing systems as first paper. (There is a typo on Page 211.)

[1] L. Damas, R. Milner, Principal type-schemes for functional programs.

Eric Lippert[0] is doing an "excessive explanation" of this paper[1], where he breaks the entire paper down, line by line, with examples that C#/Java people would recognize. It's nice for people like myself who are strong on concepts, but weak on notation.

ex:

  map  : ∀α ∀β ((α → β) → (α list → β list))

Which I previously couldn't read, but I could easily explain the concept.

[0] - Former C# language designer, Roslyn compiler team, etc.

https://www.reddit.com/r/programmerchat/comments/37qwmm/i_am...

https://ericlippert.com/about-eric-lippert/

[1] - https://ericlippert.com/?s=excessive&submit=Search

Thank you, that's an interesting point.

The thought that somebody would not be able to understand the type of map had not occurred to me, because I'm surrounded by people with a strong maths/FP background. Shows just how narrow-minded I am.

While I agree that compilation of dynamically typed languages is more challenging, inference for advanced typing systems is full of problems:

- How to ensure that the inference algorithm is correct.

- How to design typing systems that are expressive, yet lightweight, and have enough type inference to be usable in practise.

- How to deal with concurrency and parallelism.

None of these problems is really solved. In practise even making type inference fast is a challenge, e.g. in older versions of the Scala compiler, type inference was really slow due to implicits.

> Pierce's Types and Programming Languages

Pierce's book is as approachable as you're likely to see with respect to type systems. You mostly just have to dig in.

Yeah, I suspect you're correct at the moment. In fact, TaPL looks pretty approachable for an academic book.

But it seems to be there's a place for a more popular book on type systems and making a statically-typed language, in the vein of this Crafting Interpreters book (and others like it).

Perhaps I'll read TaPL, write a nice statically-typed language, and then write the book I'm looking for.

I'm reading TaPL, done 4 chapters.

I think you can replace the math with intuitive diagrams and be a little less rigorous and that would be a book for the masses.

TaPL requires you to learn a lot between coding sessions too which may put off more practically minded folk.

I want this too, but is weird to me that is a huge chasm in this area, where a lot of material stop at the most basic, and then it cover a niche that is complicated (like for example, type inference).

If I wanna to implement a dialect of ML, I haven't' find a simple explanation in how implement product/sum types, modules & pattern matching.

Yet, tons of type inference and other less common things.

ie: The basics stop fast and suddenly jump into something else.

> If I wanna to implement a dialect of ML, I haven't' find a simple explanation in how implement product/sum types, modules & pattern matching.

Exactly. I mean, how in the world to implement pattern matching in ML-like languages? And ADTs? These are exactly the kind of subjects I'd like to see covered in a more advanced book on building interpreters or compilers for statically-typed languages.

Writing a type-checker is fun and pretty interesting. For that, I recommend you get acquainted with formal semantics and judgements (that's just the language for describing type-systems). You'll probably be interested in then looking up

  * simply typed lambda calculus
  * Hindley-Milner type inference
  * bidirectional typing

After that, there are all sorts of cool things like linear/affine types, system F, dependent types, etc. which can be picked up.

All of this (except maybe the first part) is easily learnable either from Wikipedia, the original papers, or recent tutorials.

Notes only tell half the story, but these are good notes on the first two topics.

https://www.cs.cornell.edu/courses/cs4110/2016fa/schedule.ht...

Those are very good notes that have come up frequently in my Google searches.

Shameless plug: If you know OCaml, then I wrote this tiny implementation of Hindley-Milner[0] for a tiny functional language.

It's (hopefully) very well commented, so it should clarify a bunch of concepts for newcomers.

[0] - https://github.com/prakhar1989/type-inference

I'm starting a series of blog posts on making first a dynamic Lisp and then adding a type system to it, then type inferencer, etc. I'd be interested in what resources you found helpful and easy to read.

Are you going to share the links once you're done?

I can share now if you like. They're at http://bernsteinbear.com/blog/lisp/ -- still a work in progress. I hope to be done with Primitives II tonight.

> more advanced, static type systems

Are static type systems more advanced than dynamic type systems? This sounds surprising, given how much more one can do with a dynamic type system.

The quality of a type system isn't measured solely by what it allows you to do. After all, no type system at all would allow you to do anything and write as many bugs as you want-- not great, right? Instead, a better type system will let you make guarantees about your code, while still allowing correct programs to run. Can you guarantee there are no type errors? Can you guarantee arrays aren't accessed out of bounds? That sort of thing.

Basically, yes. You can do more with a dynamic type system than a static type system because you don’t need to (and actually, aren’t allowed to) prove that your code is consistent. Advancements in static checking and inference mean you can prove more things about your programs, so you don’t have to fall back on dynamic types and data structures so much.

Well, you could look at a dynamic type system as just a static type system with 1 type—a sum type of everything. Looking at it that way, a dynamic type system is much less powerful.

   Anyone up for writing such a high-quality 
   book as this one on statically-typed languages,

Not a book, but maybe "The Essence of ML Type Inference" by Pottier and Remy [1] is of interest. It's a bit more in-depth than TAPL.

[1] gallium.inria.fr/~fpottier/publis/emlti-final.pdf