3 ms·
I read the first post and thought someone should at the very least post the lambda cube. This isn't my area of expertise, since I've done very little with depen
by nixpulvis 11mo ago
I read the first post and thought someone should at the very least post the lambda cube. This isn't my area of expertise, since I've done very little with dependent types (staying firmly on the left side of the cube), but it outlines some useful categories of type systems here.
https://en.wikipedia.org/wiki/Lambda_cube https://en.wikipedia.org/wiki/Lambda_cube
- azdavis 11mo agoI wrote a small post on that: https://azdavis.net/posts/lambda-cube/ https://azdavis.net/posts/lambda-cube/ Hope it’s helpful!
- nixpulvis 11mo agoCool that you worked on an implementation of the CoC. I've been somewhat wanting to go back and revisit ATAPL and read chapter 2 on this subject: https://www.cis.upenn.edu/~bcpierce/attapl/frontmatter.pdf https://www.cis.upenn.edu/~bcpierce/attapl/frontmatter.pdf
- ChadNauseam 11mo agoThat is a good post. I've linked to it from mine!
- azdavis 11mo agoThanks! But I don’t think it quite worked?
- ChadNauseam 11mo agoOught to be fixed now