Franklin Pezzuti Dyer
Lately I've been continuing my adventures in dependent type theory and computer-verified proofs by working with the Idris language. I've really enjoyed using Agda, but I think that Idris has started to appeal to me more because it feels like it strikes nice balance between practicality and more "academic" use cases, e.g. as a proof assistant. But I still consider myself a beginner at all of this stuff, so instead of arguing for the merits of Idris I'd like to talk about a specific interesting problem that I've solved recently. (You can find all of the code that I've written for this post in this Github repo.)
Idris has this neat feature called totality checking. A function is called total when it is guaranteed to terminate "eventually" for any possible input value you might pass it. Due to the uncomputability of the Halting Problem, it's not possible to look at an arbitrary function and decide algorithmically whether or not it can enter an infinite loop. But for certain kinds of recursive definitions that adhere to a specific pattern, it's possible to confirm that they define total functions.
where x : a is the base-case value of f, and g : a -> a is some function that is iteratively applied to x. Totality checkers like this sort of definition because the argument decreases by one with each recursive call. If one of your function definitions can be seen to fit this pattern through static analysis, then it will get a big thumbs-up from the totality checker, because this is a known way of defining total functions on Nat.
