Verified Functional Programming in Agda (dl.acm.org)

I was delighted to see that both idris and agda have JavaScript backends. Is there actually any productive use for that? Particularly looking at all the excitement around Reason .

I'm surprised Andrej didn't give a longer answer. He usually does. In a type theory the type system and calculus are the same thing, not really two things glued together (although there are some of those.) Those used for theorem proving and programming (CIC, MLTT, etc) aren't Turing complete by themselves. Different type theories do differ in computational strength. How is this possible? Well think about it, if you couldn't express the type of the Y combinator then you couldn't use it. Schemes like recursion, induction-recursion and induction-induction allow more power to be added to the language.

To answer you more directly, one starts with the most powerful system, the lambda calculus and then one restricts its power using types. Finding the goldilocks zone of the right amount of power is one of the primary things type theory research has been about. Type theories vary in decidability, those that aren't decidable aren't usually used for theorem provers or as substrata for programming languages.

You need something which decreases on each step. You could try to recurse on the number of unvisited nodes in the graph. You can try well-founded recursion if this does not work for some reason.