Lambda Cube is a personal project aimed at implementing every corner of the lambda cube, exploring different variations of lambda calculus and serving as a foundation for experimenting with functional programming and type theory.
The primary goals of the project are as follows:
- Implement an extendable core calculus that allows for the addition of various extensions.
- Develop three main features: System F, dependent types and type constructors, and combine them into different systems like simply typed lambda calculus and calculus of construction.
The project includes the following key features:
-
Core Calculus: An extendable codebase that serves as the foundation for the project and supports untyped lambda calculus.
-
Simply Typed Calculus: Elaboration of the core calculus to support simply typed lambda calculus.
-
Advanced Features:
- System F: Implementation of System F, a polymorphic lambda calculus that introduces parametric polymorphism.
- Dependent Types: Support for dependent types.
- Type Constructors: Support for type constructors, enabling more expressive type systems.
As the project is currently in development, there are no completed features available for use. However, if you're interested in exploring or contributing to the project, you can follow these steps:
-
Clone the repository to your local machine:
git clone <repository-url> -
Build the project using Cargo, the Rust package manager:
cargo build
While the project is still evolving, potential future developments include:
- Providing a Virtual Machine for the project to enable compilation and optimization, aiming for improved performance.
- Continuously refining and expanding the implementation of different lambda calculus variations.
- Welcoming contributions and feedback from the community to enhance the project.
To help you navigate the project, here are some terms you may encounter:
- Lambda Calculus: A formal system in mathematical logic and computer science used to represent and manipulate functions.
- System F: A polymorphic lambda calculus that introduces parametric polymorphism, allowing functions to be generic over types.
- Dependent Types: Types that depend on values, enabling more precise and expressive type systems.
- Type Constructors: Functions that take types as input and produce new types as output, allowing the construction of complex types.
Although the project is in its early stages, feedback and suggestions are welcome. If you encounter any issues or have any advice, please feel free to open an issue on the repository.
This project is licensed under the MIT License.