Type System

Lambda Calculus

Simply Typed Lambda Calculus

System F

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