Some years ago I worked through this in Haskell: https://github.com/evertedsphere/how-to-implement-dependent-type-theory https://github.com/evertedsphere/how-to

Some years ago I worked through this in Haskell: https://github.com/evertedsphere/how-to-implement-dependent-type-theory https://github.com/evertedsphere/how-to-implement-dependent-... If you find this stuff interesting, the recent Little Typer book is also worth a look.