Type Systems

Most programming languages are split between either typed or untyped languages (untyped approximately means dynamically typed). In order to discuss this distinction, what is meant by type?

The consensus is that a type is a set of values. For example, int is the set of all integers. bool is the set of {true, false}. List[int] is the set of all lists containing integers. int->int is the set of functions mapping from integers to integers.

Type Inference

One reason people are interested in type systems is to be able to definitively show that, under the assumption that certain expressions have certain types, a new expression has a known type. Specifically, in type systems, we prove that a given expression has a particular type. Type inference has a particular syntax that is precise and well-established, but takes a little time to get used to.

Symbols & Syntax for Type Inference

\(\land\) means “and”. \(X \Rightarrow Y\) means “if X-then Y”. \(X:T\) means “expression x has type T”. Thus, \(e_1: Int \land e_2: Int \Rightarrow e_1+e_2: Int\) means “If e_1 and e_2 are both integers, then their sum is also an integer.” The turnstile symbol \(\vdash\) is used to indicate “It is provable that…”.

The common syntax is to place hypotheses above a broad horizontal line and its conclusions below the line, typically after the turnstile symbol. For instance:

\[\infer{\vdash A}{ B}\]

Means

Rules of Inference