5 ms·
Knowledge of the Y-combinator helps avoid making your language divergent (sometimes desirable), disallowing explicit recursion is not enough! The typed lambda c
by grumpyprole 4y ago
Knowledge of the Y-combinator helps avoid making your language divergent (sometimes desirable), disallowing explicit recursion is not enough! The typed lambda calculus uses static types to prevent the Y-combinator and give a sound logic for proofs.
- dataangel 4y agoStatic types doesn't seem sufficient? Typed languages have no problem expressing passing functions as parameters. Where does it break when you apply static types?
- saghm 4y agoI think it's because the y-combinator needs to be passed to itself as an argument, and it's hard to come up with a static type for a function where one of the parameters is the type itself.
- octachron 4y agoThe Y-combinator require (equi)recursive types for the intermediary step `x x` where `x` has type `('a -> 'b as 'a) -> 'b` using OCaml notation.