1
$\begingroup$

I want to implement Martin Löf's intuitionistic type theory in a functional language such as Haskell, preferably also implementing a lexer/parser for the language. How should I start approaching it? Are there any good papers/blog posts/github repo examples that might be useful? Thanks!

$\endgroup$
3
$\begingroup$

This paper is my go-to for implementing dependent types. It starts from the basics, uses bidirectional types, and has accompanying code in Haskell.

If you're at all interested in type inference, this paper is great, and also has accompanying Haskell code.

David Christiansen has a tutorial on dependent type checking with bidirectional types, with a Haskell and Racket. More generally, I've heard great things about his book The Little Typer, though I haven't had a chance to read it myself.

I've heard great things about smaltt by András Kovács, particularly for it being an efficient implementation.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.