Type System

Lambda Calculus

Lambda Calculus just has variables, functions, and function applications. It is a "dynamic" language without static types.

λx. x y z

Simply Typed Lambda Calculus

Types can help distinguish terms and their intended purpose. The : colon is traditionally used to separate terms from types. LM uses prefix notation for everything, so the colon precedes both the term and the type.

Traditional Notation

1 : Integer

LM Notation

(: 1 Integer)

System F

System F adds the ability for objects to be parameterized with quantified type variables. In LM type variables are represented with lowercase identifiers.

some : a -> Option<a>

System F<:

System F<: adds the ability for objects to become subtypes (<:) of a hierarchical type system.

In standard notation this might look something like this:

type X implies Y;

(x : X) <: Y    # yes

In plural notation the subtyping relations can often be expanded to clarify a bit more of what is going on.

(x : X+Y) <: Y  # yes

System F<: with Specialization

Specialization adds the ability to pun (overload) functions onto the same identifier. Then, when applied, punned functions are "narrowed as necessary" to decide which function to apply.

$$abstraction \quad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B \quad \Gamma \vdash x:X \quad \Gamma \vdash y:Y \quad λ⟨a.b⟩⟨x.y⟩}{\Gamma \vdash λ⟨a.b⟩⟨x.y⟩:(A \to B) + (X \to Y)}$$

$$application \quad \frac{\Gamma \vdash f:(A \to B) + (C \to D) + (X \to Y) \quad \Gamma \vdash x:A + X \quad f(x)}{\Gamma \vdash f(x):B + Y}$$

Guarantees

Type Inference is Strongly Normalizing and Decidable as long as all overloaded functions are given explicit type annotations.