Type systems are designed to prevent the improper use of program operations. They can be classified as either static or dynamic. Static type systems detect "ill-typed" programs at compile-time and prevent their execution. Dynamic type systems detect "ill-typed" programs at run-time.

Static type systems hace two important advantages over dynamic type systems. First, they provide important feedback to the programmer by detecting a large class of program errors before execution. Second, they extract information that a compiler can exploit to produce more efficient code. The price paid for these advantages, however, is a loss of expressiveness, modularity, and semantic simplicity.

This paper presents soft type systems that retain the expressiveness of dynamic typing, but offers the early error detection and improved optimization capabilities of static typing. The key idea underlying soft typing is that a type checker need not reject programs containing "ill-typed" phrases. Instead, the type checker can insert explicit run-time checks, transforming "ill-typed" programs into type-correct ones.

Paper: https://www.cs.rice.edu/~javaplt/papers/sigplan39-4.pdf
Zoom: https://umd.zoom.us/j/98723227318?pwd=K0RJZVZZM1Jhd2laMlg1ajgvUjltQT09