A playground for building a statically checked type system based on the simply typed lambda calculus. In the source code, there is merely a definition for an abstract syntax tree and a corresponding type checking function. It would be straightforward to define and implement the operational semantics for the language, but that falls outside the scope of the project. No lexing, parsing, or code generation is performed, however a parse syntax tree is defined to facilitate syntactic sugar.
- System F first-class polymorphism
- Function abstraction and application
- Boolean and integer logic
- N-ary tuples
- Structural labeled records
- Structural labeled variants
- Statements
- Let bindings
- user-defined nominal types
- arrays
- mutability
- type inference/reconstruction