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 more than one type.

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. This resolution happens entirely at compile time.

$$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}$$