|
|
|
|
|
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. |
|