Hacker News new | ask | show | jobs
by mrkeen 15 hours ago
It depends on the type system you choose to apply to LC. Simply-typed LC terminates.

You have to include a construct that introduces general recursion to make it Turing complete.

There's a cool practical space within those constraints that needs more exploration.

Non-total functions can call total functions, but not vice-versa.

Imagine a web server whose main loop is non-total, because you want it to stay up. But each route is total, to guarantee termination.