> the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all
This is only the case for untyped systems. If we try to type the Y combinator, we will eventually need some notion of recursion. For example, in Haskell/OCaml we can type it with iso/equi-recursive types. How many truly untyped systems we use in practice?
The Y combinator as a counterexample of termination is a great insight though!
Dynamically typed programming languages are statically untyped.
You might argue they are unityped, but that’s really a type theoretician’s job security: if a language has the untyped lambda calculus as a subset (like the python example in this discussion) it’s reasonable to call it untyped.
This is only the case for untyped systems. If we try to type the Y combinator, we will eventually need some notion of recursion. For example, in Haskell/OCaml we can type it with iso/equi-recursive types. How many truly untyped systems we use in practice?
The Y combinator as a counterexample of termination is a great insight though!