5
$\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$

1 Answer 1

5
$\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$
2
  • $\begingroup$ Great answer. Do these tutorials cover bottom, top, unit, etc. types? $\endgroup$
    – igravious
    Commented Nov 21, 2022 at 4:18
  • $\begingroup$ The LambdaPi paper doesn't, but it gives the general pattern for how to add types, so it shouldn't be too hard to add bottom and top. $\endgroup$ Commented Nov 21, 2022 at 16:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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