The Y combinator is in a sense the heart of the λ calculus; it's a key discovery for understanding that the λ calculus is universal, which is what makes it a useful concept rather than an arbitrary bundle of rules.
The simply typed, and, especialy, the dependently typed lambda calculi are extremely versatile and powerful subsets of untyped lambda calculus which do not admit the Y combinator. Their usefulness does not at all require universality, and are, perhaps, more useful for being typed.
The Y combinator is a specific fixed-point combinator in lambda calculus. It is used to express recursion in lambda calculus where direct recursion is not initially available due to the lack of named functions. The Y combinator demonstrates the power of lambda calculus.
> which is what makes it a useful concept rather than an arbitrary bundle of rules.
I cannot recall a single practical FP language based on the Y combinator for recursion. The typical approach is to extend lambda calculus with a separate recursion primitive.
lmm|2 years ago
cvoss|2 years ago
andsoitis|2 years ago
The Y combinator is a specific fixed-point combinator in lambda calculus. It is used to express recursion in lambda calculus where direct recursion is not initially available due to the lack of named functions. The Y combinator demonstrates the power of lambda calculus.
Hirrolot|2 years ago
I cannot recall a single practical FP language based on the Y combinator for recursion. The typical approach is to extend lambda calculus with a separate recursion primitive.