1. Introduction

本书关注 type system 这一 formal method.

Type systems: detecting errors, abstraction, documentation, language safety, efficiency.

A safe language is one that protect its own abstractions.
A well-designed statically typed language will never requirehuge amounts of type information to be explicitly and tediously maintainedby the programmer.