rohlang3: a point-free, homoiconic, and dependently typed SK calculus

A small, experimental SK-like language with a dependent-type flair—and a pinch of reflection, partial evaluation, and environment reordering—implemented in Rust. What's cool about it is that typing context is a first-class construct that can be manipulated by the program itself.

Also even though I (and o1-pro) wrote it, I can't really even think of a good example to write. Also, I am 100% sure there are many, many, logical inconsistencies and paradoxes (for one, Girard's paradox). If you want a more complete look at the (obvious) issues check issues.md.

---

Table of Contents

1. Introduction
2. Overview
3. Key Concepts
   • Expressions (AST)
   • Combinators
   • Dependent Types
   • Reflection & Partial Evaluation
4. Language Features
   • Type System
   • Runtime Evaluation
   • Context Stacks & Reordering
   • Pairs & Dependent Pairs
   • Reflection & Quotation
   • Partial Evaluation (z)
5. Installation & Usage
6. REPL Usage
7. Example Snippets
8. Project Structure
9. Contributing

---

Introduction

rohlang3 is a self-contained functional programming language and experimental type system built in Rust. It’s inspired by SK combinator calculus, extended with a small dependent type system, reflection constructs, and novel context reordering combinators. The language is an exploration of minimalist combinator-based programming with new possibilities for typed, partially-evaluated, and reflective expressions.

It’s still a small prototype, suitable for language enthusiasts, researchers in typed functional calculi, or anyone curious about how to build a language from scratch in Rust. Our main goals are to:

• Explore how SK-like combinators can be enriched with a type system.
• Provide reflection capabilities—allowing the language to “see” and “quote” its own expressions.
• Support partial evaluation, ensuring that known combinator patterns can be simplified at compile- or run-time.
• Manage a lightweight dependent type system, giving new ways to specify and check program correctness.

See Plan.md for future steps.

---

Overview

In rohlang3, programs are made of combinator applications and symbolic atoms. Rather than conventional lambda abstractions, we use fundamental building blocks (s, k, i, etc.) that can be combined to encode higher-level constructs. On top of that, we allow expressions like (p A B), which acts like a dependent function type (a Pi type), and (g A B), which acts like a dependent pair (a Sigma type).

Additionally, rohlang3 introduces:

• A single universe u, so that types themselves can reside in u (depending on usage).
• Reflection combinators q and e for quoting and evaluating expressions.
• Partial evaluation combinator z for on-the-fly simplifications.
• Context reordering combinators i, E, and D for referencing, exchanging, and duplicating the top of a "type context" stack.

---

Key Concepts

Expressions (AST)

The language supports the following core constructs:

1. Atoms (e.g., s, k, u, or user-defined symbols).
2. Applications: Written as (f arg1 arg2 ...). Internally represented by Expr::App(Box<Expr>, Vec<Expr>).

Combinators

• s and k: The standard SK combinators.
• i: An identity-like combinator referencing the top of the context.
• E: Exchanges the top two elements in the context.
• D: Duplicates the top element in the context.
• q and e: Reflection: quote and evaluate.
• z: Partial evaluation.
• r, f, d: Construct and destruct pairs.

Dependent Types

• u: The universe or type-of-types.
• p: Pi type constructor, (p domain body).
  • E.g., (p u (k u)) is “a function that, for any type A in u, returns u again.”
• g: Sigma type constructor, (g domain body).
  • E.g., (g u (i)) means “a dependent pair over u, with the second component also referencing the binder.”

Reflection & Partial Evaluation

• q: Quote an expression, e.g. (q foo). This produces a quoted AST at runtime.
• e: Evaluate a quoted AST if it’s well-typed: (e (q foo)) => foo if foo type-checks.
• z: Trigger partial evaluation. If the expression matches known rewrite patterns (like (s (k k)) => i), z attempts to simplify it eagerly.

---

Language Features

Type System

• Single universe u: all well-formed types reside in u.
• Dependent function types (p) and dependent pair types (g).
• Context-based type inference: references (i, etc.) rely on an internal stack in the type checker.
• Built-in checks for well-formedness: e.g., (p u (i)) has type u.
• Reflection type-check: (e (q expr)) only proceeds if expr is well-typed.

Runtime Evaluation

• Normal-order rewriting of combinators.
• Combinators like s, k, f, and d have fixed rewrite rules:
  • f (r x y) => x
  • d (r x y) => y
  • s f g x => (f x) (g x), etc.

Context Stacks & Reordering

• i combinator references the top of the context (i.e., the last type pushed).
• E swaps the top two context elements.
• D duplicates the top context element.

Pairs & Dependent Pairs

• r: Pair constructor (r x y).
• f (first) and d (second) are pair destructors.
• Dependent pairs via (g domain body) are recognized at type-check time as well.

Reflection & Quotation

• q: “quote,” stores an expression as data (an AST).
• e: “evaluate,” type-checks the quoted AST, and if valid, splices it into runtime evaluation.
• Any unknown symbols inside (q ...) can result in a type error at reflection time.

Partial Evaluation (z)

• (z X) tries to partially evaluate X by applying certain known combinator optimizations. For instance:
  • (s (k k)) recognized as an identity combinator, so (s (k k) X) => X.
• Repeated partial evaluation steps until a fixpoint is reached.

---

Installation & Usage

1. Clone the repository or download the source:

   git clone https://github.com/username/rohlang3.git

2. Build with Cargo:

   cd rohlang3
   cargo build --release

3. Run the REPL directly:

   cargo run

   or

   cargo run --release

4. Interpret a file containing rohlang3 expressions:

   cargo run --release my_program.rhl

   Where my_program.rhl has one expression per line, ignoring blank lines and lines starting with #.

---

REPL Usage

When you start rohlang3 with no arguments, you enter an interactive prompt:

$ cargo run
Starting rohlang3 REPL...
Welcome to rohlang3 REPL with environment + shared context.
Type `store <NAME> <expr>` to define a named expression.
Type `type <NAME>` to see the type of a stored expression.
Type `quit` or `exit` to leave.

>

Commands

• store <NAME> <expr>: Defines <NAME> in the environment, storing <expr> (parsed & type-checked) for future reference.
• type <NAME>: Prints the type of the stored expression <NAME>.
• Any other line is parsed as an expression to be immediately evaluated.

Example:

> store myId (p u (i))
Stored `myId`.
> type myId
Type of `myId` is:
  u
> (myId u)
(p u (i))
> quit
Bye!

---

Example Snippets

1. Simple SK

   (s (k k) something)  ;; The "i combinator" usage

   This partly evaluates to something.

2. Dependent Pi

   (p u (k u))

   A function from any type A : u to u. The type of this expression is also u.

3. Reflection

   (e (q (p u (k u))))

   Checks if (p u (k u)) is well-typed, then evaluates it. Since it’s well-typed, it stays the same under normal-order evaluation.

4. Pairs

   (f (r s k))  ;; => s
   (d (r s k))  ;; => k

5. Partial Evaluation

   (z (s (k k) u))  ;; => u

   Because (s (k k)) is recognized as the identity combinator.

---

Project Structure

.
├── Cargo.toml
├── Cargo.lock
├── README.md
├── Plan.md
├── slides.latex
├── src
│   ├── ast.rs          # Core AST definitions
│   ├── builtins.rs     # Metadata/type info for built-in combinators
│   ├── evaluator.rs    # Normal-order & partial evaluation
│   ├── parser.rs       # Simple s-expression parser
│   ├── type_checker.rs # Dependent-type checking logic
│   ├── repl.rs         # REPL implementation
│   ├── lib.rs          # Library entry point
│   └── main.rs         # Main CLI entry
└── tests
    └── integration_tests.rs

• ast.rs: Definition of the Expr enum and helper constructors.
• builtins.rs: Provides recognized built-ins and their "placeholder" types.
• evaluator.rs: Implements normal-order rewriting and partial evaluation.
• parser.rs: Tokenizes and parses input text into our AST.
• type_checker.rs: Contains the core type inference & context-based checks.
• repl.rs: Simple interactive REPL with commands to store and retrieve expressions in an environment.
• tests: Integration tests verifying type checking, evaluation steps, reflection, and partial evaluation.

---

Contributing

Plz contribute. Email me if you're curious about anything: rohanganapa@gmail.com.