Name: Types and Programming Languages
ISBN: 9780262162098

Types and Programming Languages

A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems--and of programming languages from a type-theoretic perspective -- -has important applications in software engineering, language design, high-performance compilers, and security. This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation, available via the Web. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material. The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages.

What Hacker News says

antonvsOct 2026

Following on from the above, this statement is also incomplete at best:

> Types are groups of related values.

This is an operational perspective which misses one of the most important aspects of types: in a statically typed language, types are a way to classify terms, i.e. they're not just about values.

As an example of why this distinction matters, consider this expression: 1 + "hello". In most statically typed languages, this will be rejected at compile time. It doesn't have to be evaluated (i.e. at runtime) to be rejected - it's invalid because the types of the terms - 1 and "hello" - aren't compatible.

This compile-time rejection is only possibly because types apply to terms, and terms aren't values. This is critical to the usefulness of statically-typed languages - without this, they'd have to run the program to detect type errors.

Benjamin Pierce's book "Types and Programming Languages" has some great coverage of this topic.

thread

kserrecSep 2026

I am a software developer and most of my work is in AWS. I don't have a CS degree, but have taken a handful of lower level courses. I haven't studied PLT much at all, but I really like the lambda calculus.

As for books, I don't have many to recommend beyond Michaelson's book except maybe a few classics like Cormen's Introduction to Algorithms, Structure and Interpretation of Computer Programs, and Types and Programming Languages.

What have you made that was cool? And what are some books you recommend?

thread

kccqzyJul 2026

Types and Programming Languages (TAPL) by Benjamin C. Pierce. Basically IMO the main differentiator between languages is their type system. It’s basically table stakes now for programming languages to provide generics so users can write their own type-safe containers, and one simply cannot implement this without some theoretical background like TAPL.

In contrast you can easily skim Chapter 7, Semantic Analysis and realize this book gives extremely rudimentary information on type systems. Even if you were to design a dynamically typed language, this book doesn’t cover user-defined structs let alone modern essentials like user-defined sum types or closures.

thread

skydhashApr 2026

> separate effect full code from pure logic

That’s a feature of the abstract machine. TM and Von Neuman is very reliant on a global (and locals) state. Lambda calculus does not and instead requires evaluation (or reduction in symbolic terms).

Best bet for this is some book on computation theory, but as the name says, they’re full of theory, but it’s kinda the foundation of everything.

> separate state and code

Not really possible. The name “code” cames from the fact that you’re encoding logic and data to represent a process. It’s a closed system and the above books explain how and why it works.

> ai native debugger

What does that mean? A debugger is mostly the capability to stop a process and inspect the current state. How does AI helps?

> native deterministic simulation testing

What does that means?

> coding proofs

Again, the books on computation theory will helps. Most of them will only explain the context free grammars (tightly coupled to TM). There’s a bunch of abstraction on top of that that leads to C, JavaScript and Python. There’s also the various other systems like Horn clauses, lambda calculus, and relational algebra. All have mathematical models that are the basics of such proofs.

> explicit type system

The main book I can recommend is Types and Programming Languages by Pierce. It also requires a good knowledge of basic computation theory. Quick note: Computation does data transformation, types helps with proving that.

> repl

While not impossible, it clashes with the above. Explicit typing is cumbersome to write while REPL is all about quick iteration. Some simple software like ed and ksh can help there.

> wasm target

Going from assembly to C is about design abstractions, compiling C to assembly is building those abstractions. Targeting wasm is about design what would take you to go from wasm to you abstract machine that is capable of executing your language and then starting to build it.

thread

dupedApr 2026

> types and typing

Types and Programming Languages, Benjamin C Pierce

> object files, executables, libraries and linking

Linkers and Loaders, John R Levine

thread

ks2048Oct 2025

A related book (seems to be more often cited) is Types and Programming Languages by Benjamin C. Pierce. That seems to be more concrete (as opposed to theoretical), with chapter titles like "An ML Implementation of {some concept}".

thread