Chapter one: Introduction

Type System

Some argue that a “type system” is an effective syntax for classifying statements according to worthy types to find program defects or bad behavior.

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

There are a few points worth debating about this definition.

First of all, this definition says that type systems are for “programming,” but they have broader applications in mathematics, logic, and philosophy. However, this book focuses on type systems in programming.

Secondly, even type systems in programming have two directions of study: application and theory. The book focuses on the applied direction, while the theoretical direction may examine the correlation between various pure typed lambda calculi and different logic. In practice, for example, many programming languages do not support recursive function definitions, and theoretical research will certainly look at a complete type system.

Finally, it should be added that the type system can be viewed as a static approximation of the runtime behavior of a program. As a result, sometimes errors can occur, such as the following code:

if <complex test> then 5 else <type error>
Copy the code

If

always returns true, then

will never be executed. But the type system will let you fix the

anyway.


This is because the type system is a static approximation and cannot compute the runtime results of

. As a result, the type system can only find some of the bad behavior in your program. For example, the type system will tell you that an argument must be a number, that an object is missing an attribute, but the type system can’t find that the dividend is zero, that an array is out of bounds, and so on.

Bad behavior that can be eliminated by a given language’s type system is often referred to as Runtime type errors. While there is a lot of overlap between runtime type errors in most languages, each language has its own runtime type errors that it wants to avoid, so the safety or Soundness of the type system is not the same for each language.

Advantages of type systems

Detect errors

The type system can detect errors before the code is run, thus avoiding more errors that might occur after it is run.

This makes it easy to refactor code, so if a programmer needs to change the definition of a piece of data in a large project, he doesn’t have to search around because the type system tells him or her all the inconsistencies.

abstract

Another benefit of type systems is that they force programmers to think more critically. Especially on large projects, the link between modules and components is entirely held up by type systems, such as the interfaces and classes provided by modules.

The document

The type system allows programmers to read code faster.

Language security

Unfortunately, the concept of “security” for a language is more controversial than a “type system,” because the understanding of security varies greatly from language to language. In this book, “language security” refers to a language that provides protection for abstractions. Every high-level language abstracts hardware, so security in this book refers to a language’s ability to ensure the accuracy and completeness of its abstractions, as well as the accuracy and completeness of the higher-level abstractions that developers can construct with the language.

That sounds like a mouthful. Let’s do an example. A language that provides arrays and an interface to read and write is an abstraction of a contiguous chunk of memory. Users of the language believe that there is no other way to change the array than through these interfaces. For another example, if a language supports lexical scope, then the speakers of the language assume that variables can and can only be used in their lexical scope.

In an insecure language, developers must remember all the low-level details, such as the distribution and order of data in memory, in order to understand the code. The results of code execution are also affected by the environment in which it is run.

Language “security” and “static type safety” are not the same thing. Language security can be achieved either through static type checking or through run-time checking (reporting an error or throwing an exception whenever an illegal operation is encountered). Scheme, for example, is a secure language, but it doesn’t have a static type system.

On the other hand, insecure languages often try to provide static type checkers, but by our definition, such languages don’t count as type-safe. Because such languages do not guarantee that well-typed programs will be well poured. Static checkers for these languages can prove that one piece of code “has” a runtime type error, but not that another piece of code “does not” have a runtime type error.

(This section will not be translated, interested in their own)

The efficiency of

The first type systems in the history of computer science began in 1950 and 1960 (Fortran, for example), and were introduced to improve mathematical efficiency by distinguishing integer and decimal operations. By distinguishing the two types of data, the compiler can use different representations to generate different machine instructions and primitive operations. Today’s high-performance compilers also rely heavily on information gathered by type checkers during the optimization and code-gen phases, and even compilers for languages without type systems will try to mine type information to improve execution efficiency.

Type systems and language design

Ideally, language design should be accompanied by type system design. Below is a little.

Type a brief history of

The original type system was designed to distinguish integers from floating-point numbers, and this taxonomy has since been extended to structural data (like Arrays of Records) and higher-order functions. In the 1970s, a richer set of concepts was proposed, including parametric polymorphism, abstract data types, Module systems, and subtyping. Computer scientists began to realize the connection between type systems and mathematical logic, and the two fields have influenced each other until now.

Related reading materials

  • Handbook articles by Cardelli (1996) and Mitchell (1990b)
  • Barendregt ‘s article (1992).
  • Foundations for Programming Languages (1996)
  • Reynolds’ Theories of Programming Languages (1998b),
  • The Structure of Typed Programming Languages, by Schmidt (1994),
  • Hindley’s monograph Basic Simple Type Theory (1997)
  • Abadi and Cardelli’s A Theory of Objects (1996)
  • Kim Bruce’s Foundations of ObjectOriented Languages: Types and Semantics (2002)
  • Palsberg and Schwartzbach (1994) and Castagna (1997).
  • Basic Category Theory for Computer Scientists (Pierce, 1991a).
  • Proofs and Types of the Girard, Lafont, and Taylor’s Proofs and Proofs (1989)
  • Pfenning’s Computation and Deduction (2001).
  • Thompson’s Type Theory and Functional Programming (1991)
  • And Turner’s Foundations for Functional Languages (1991)
  • Proof Theory and Automated Deduction (1997).

There are so many books that I won’t translate.