"The Power of Pi" has survived as the most accessible but information and lesson-dense paper i recommend to people interested in dependently typed programming cs.ru.nl/~wouters/Publi
Conversation
Replying to
Read this one recently and implemented a bit of it in Idris. Well worth the time!
Sadly I got an obscure totality checker problem with my DDL implementation. I was trying to allow for more general binary types: github.com/brendanzab/idr - also would be interesting to try to get it closer to looking like PADS 🤔
1
I'm guessing it has to do with the `FVect` constructor that I moved into the top-level universe. The paper mentioned a similar problem that occurred with a 'many' binary format, but it was hard to figure out a way around it on my own...