LambdaPiPlus: a small language for learning and hacking Dependent Types

Author here.

LPP is a small language with dependent types. The idea is that it's a small set of features for people who are just starting with DTs to learn, and it's also a small enough code base that if you're doing research with DTs, it can serve as a platform for testing new features.

It's been compiled to JavaScript, so you can try it in your browser, though right now there's no way to run programs, only to typecheck them. The error messages right now are pretty terrible, but this is partially intentional, since I'm working on new message generation techniques.

As you find issues (as I'm sure there are many), feel free to report them on Github .

I created LambdaPiPlus as the starting language for the research of my Masters Thesis, on the subject of improving error messages in dependently-typed languages. I found in my research that it's hard to artificially create poorly-typed programs that resemble what a programmer (especially a novice DT programmer) would write.

Part of my motivation for releasing LPP is to allow others to try it and, if they consent, collecting the source of small programs that fail to type-check. Source-code collection can be turned off by checking the box at the bottom of the "Try" page.