Comment

Comment by librexpr

I'm pretty sure it's impossible to write a function that tests for zero for these numerals. Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...) with some number of args. This call must be toplevel, not as an argument to another function, because otherwise it is lazy and not executed. The number of args also cannot be infinite, since that would require an infinitely large program.

The expansion into |n|(args...) must happen before we know what n is, because in the lambda calculus we can't know anything about a function without calling it. Since it happens before we know what n is, then the number of args will necessarily be the same for all n. When n > numargs, |n|(args...) ignores all its arguments and halts, and therefore f cannot be a useful test for zero.

parent librexpr 3 years ago

Discussion

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton