How to implement dependent type theory I (2012) | Hacker News Reader

How to implement dependent type theory I (2012)

math.andrej.com

58 pointstodsacerdoti9 comments

I've noticed amongst many peers that when going down the type theory/pl theory journey there is a ton of hidden knowledge and context we all find ourselves collecting which makes all it "click" and help produce more idiomatic implementations.

All of this knowledge and context spread amongst a common set of books, papers, blog posts, and git repos floating around the internet.

At the risk of creating yet another partial silo, I decided earlier this year to create a project similar to the [Elaboration Zoo](https://github.com/AndrasKovacs/elaboration-zoo) but focused on a blessed path to MLTT with a number of the desirable language features via bidirectional typechecking.

https://github.com/solomon-b/lambda-calculus-hs

The project is incomplete and my end goal is a website like the [1 Lab](https://1lab.dev) but focused on Type Theory and PL Theory, but I ran low on steam and could use some collaborators.

This is really cool. I've been doing something in a similar vein at https://github.com/sgodwincs/lamda_calculus_formalizations, though the difference being I'm using Lean and trying to prove certain properties of the languages (type safety, normalization, etc.). Of course, compared to unification and stuff you have, I only have very simple additions like natural numbers and binary product types (though the proofs still are hard for me!). Working on finite product types now and it's an absolute pain to even define it in a way that Lean likes.

Your project is cool too! I haven't tried Lean yet but have done some similar formalization in Agda.

I went with Haskell as my meta-language because I'm specifically trying to focus on language implementation rather then formal analysis and proofs.

I have everything from the README other then linear types, row polymorphism, and case-trees implemented outside the repo (and some in the main/old folder). I haven't gotten them into the repo yet because I want to make sure the implementations are succinct and decently documented.

I want to move onto a 1lab style presentation with substantially more documentation at a later date.

This is really wonderful. I'm an amateur PL theory / type theory enthusiast, always looking to get my hands more dirty.

Not sure how I could contribute, but I'd love to if possible.

Can you recommend any resources on how to avoid paradoxes? From what little I know, very innocent seeming combinations of features/axioms result in proofs of false. That seems to be a very important resource for developing a language, because you can't wait until the end to discover that you shouldn't have had type-in-type or so on.

Excellent work. Thanks for sharing!

Jon Sterling, How to code your own type theory

https://www.youtube.com/watch?v=DEj-_k2Nx6o

There's Pi and Sigma so it is about dependent type theory as well.

type term = | Var of var | Pi of term * term binder (* Pi (x:A). Bx A; x.B ) | Sg of term term binder

https://github.com/martinescardo/HoTTEST-Summer-School/tree/...

We've started to formalise TypeQL (TypeDB's query language) using dependent type theory, which fit together very nicely. Interestingly, the formalisation shows us how to consistently and safely extend the language with new structures for higher levels of expressivity, which is a huge benefit of type theoretic formalisms of production languages IMO.

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

If you find this stuff interesting, the recent Little Typer book is also worth a look.

Reply on news.ycombinator.com