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

Plural Types

Sometimes it is necessary to include more information about a type than just its normal data type. For example, representation is important for an assembler to know whether the type is stored as a LocalVariable or a GlobalVariable. Plural Types allow us to pour all of this information into a type "soup" that spreads that information as necessary.

Logical Propositions

Nominal Types can be associated with logical properties. When a Type carries a proposition, in order to soundly fulfill that proposition two things need to be independently proven:

1. The typed memory region carries the proposition's name (for example List::Sorted)
2. The name is only given to regions that satisfy the propositions semantic conditions (List::Sorted lists are sorted)

Condition 1 is already working in the type system, however condition 2 will require some significant work. This feature is a prerequisite for fully certified builds.

Guarantees

Type Inference is Strongly Normalizing and Decidable as long as all overloaded functions are given explicit type annotations. Practically, this means that all type inference can happen at compile time with no "infinite loops" during the type checking.