Comment by _lm_

You might find Idris's totality checking very interesting, if you haven't already seen it!

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html...