Hacker News new | ask | show | jobs
by cvoss 1034 days ago
Of course there are other useful things. But a comment argued that the presence of Y is what makes untyped lambda calculus useful. My rebuttal is that certain subsets which (intentionally) lack Y are more useful. Applications of typed calculi abound, but one rarely sees applications of the untyped calculus. Universality is not so important, it would seem. For example, infinite computations can still be modeled in typed calculi, but one has more control over them in that setting than running on "bare metal" untyped lambda calculus.
1 comments

Ok, "useless" is a slight exaggeration; non-universal calculi can be useful. But the thing that makes the lambda calculus so important and famous - the thing that makes it "the lambda calculus - is universality, and that's the ur-application that makes all of the subsequent application of calculi to mechanical computation possible.