Not in an HN comment, but here's a paper called Power of Pi https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf https://cs.ru.nl/~wouters/Publications/ThePo

Not in an HN comment, but here's a paper called Power of Pi https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf that probably explains it the best. It shows the usage of it for deriving a parser and generator from a single specification, and also crypto protocols and database usage. It uses Agda for its examples, but it can be translated to Idris as well.