shlok (श्लोक): dependently typed functional language

The project is in its nascent stage and is purely for educational purposes. I do not have a defined roadmap as such but I am looking to explore PL design space and incorporating eclectic ideas into shlok. I might end up building something entirely different, you never know. Currently, I am learning to write type checker for simply-typed λ-calculus (STLC) 🚧

Here are a few things I am looking to build although it might seem ambitious for a curious PLT beginner (who cares?):

Highlights of this project

• Smallest imaginable statically typed functional language
• Dependent type sytem serves as the core of the language
• Evolved from a small STLC core to dependent-typed λ-calculus
• Support for data types and writing simple programs in its initial version

Reading material

Simply typed lambda calculus

• Paper on "An Implementation of a Dependently Typed Lambda Calculus" by Andres Löh, Conor McBride and Wouter Swierstra
• OPLSS 2018 lectures "Foundations of Programming Languagues" by Paul Downen and Jan Hoffman
• Chapter 7 on Types, "Essentials of Programming Languages" 3rd edition by Daniel P. Friedman and Mitchell Wand
• Part II on Simple Types, "Types and Programming Languages" by Benjamin C. Pierce

Road to Shlok

1. Implementing Simply typed λ-calculus 📍