Brendan Zabarauskas on Twitter: "@GabriellaG439 Oh, I also forgot to mention “A simple type-theoretic language: Mini-TT” which was pretty helpful too: https://t.co/85SVFVi8bY" / Twitter

I'm a self-taught type theorist, so I wrote up a post introducing type theory resources geared towards implementers that were instrumental in my own education:

haskellforall.com

Introductory resources to type theory for language implementers

A post touring resources you can use to learn how to implement a type checker or type inference algorithm

11

64

329

Brendan Zabarauskas

@brendanzab

May 1

Nice list! I found “ A Tutorial Implementation of a Dependently Typed Lambda Calculus” to be pretty helpful early on: andres-loeh.de/LambdaPi/, and also this series of blog posts: math.andrej.com/2012/11/08/how

1

5

Brendan Zabarauskas

@brendanzab

May 2

Later on I found github.com/jozefg/nbe-for and github.com/AndrasKovacs/e to be extremely useful! But yeah I'm not sure how easy they would be to get into from scratch. I often joke that it would be neat to have some sort of “Crafting Elaborators” book for getting people started.

1

6

Replying to

and

Oh, I also forgot to mention “A simple type-theoretic language: Mini-TT” which was pretty helpful too: cse.chalmers.se/~bengt/papers/

2:27 AM · May 2, 2022Twitter Web App

Conversation