Currently my programs parse text. I have a JSON formatter, a lisp formatter. I'm also writing an Agda preprocessor in Agda i.e. parse Agda-like code, process it, print valid Agda code. I use them in my other projects as tooling.
Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.
Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.