Man, this is ugly. Multiplication is implemented recursively as repeated addition, then exponentiation on top of that as repeated multiplication. But it works! And type-checks! Give it two integers and it gives you n^m.
Sadly, recursive functions mean that it's no longer guaranteed to terminate.
(fn n:int. (rec pwr:int->int m. (if m > 0 then (rec mul:int->int y. (if y > 0 then n+(mul (y + (-1))) else 0) ) (pwr (m + (-1))) else 1 ) ) )I was about to rewrite in in Python just for fun, but then I realized you can't (?) make recursive functions with Python lambdas.