Contains the untyped lambda calculus example, where all the terms are untyped. Only term and evaluated value in the language.
- Omega Combinator which is a builtin that allows a lambda argument to itself, which allows recursions.
Contains the STLC example, which add type annotation and type checking to the language. Now out language has two scopes (one is to store types, and one is for values).
- A monad for type checking so that the type checking between expressions/files is possible.
Terms depend on types, it has a lot of names (generic, parametric polymorphism, system F...). It is named lambda 2 because of the name "second order typed lambda calculus).
A generic term is a term that works for any data type, if there is an instance for it. So we only write one definition and it will copied the same way, and generally acts the same way for different type.
We allocating definitions on the heap and pointers for data structures, and we cast the data to and from, depends on its type.
Copy the code in compile time statically for the different types of data we want to store.
Types depend on types, it is extended from lambda 2. Where it allows type constructor that accept another type. Like Rust's Result<T, E> and Haskell's Either Left Right.
Types depend on Terms, also dependent type
It is a lambda that include the feature of λ2 and λω and λΠ.
Higher inductive types.