[HN Gopher] The Y Combinator
___________________________________________________________________
The Y Combinator
Author : pcaversaccio
Score : 57 points
Date : 2021-06-29 08:09 UTC (14 hours ago)
(HTM) web link (mvanier.livejournal.com)
(TXT) w3m dump (mvanier.livejournal.com)
| teddyh wrote:
| If you prefer video, here is an explanation of the Y combinator
| from Gerald Sussman himself:
| https://www.youtube.com/watch?v=0m6hoOelZH8#t=1h12m30s
| selimthegrim wrote:
| The kabbalah joke at 4:48 is priceless
| ProfHewitt wrote:
| Y Combinator _does not work_ for strongly-typed programs
|
| because the definition is not strongly typed.
|
| Instead recursion must be added as an additional primitive to
|
| the lambda calculus.
|
| See https://papers.ssrn.com/abstract=3418003
| Joker_vD wrote:
| It's perfectly well typed in System F as "forall a. (a -> a) ->
| a".
| ProfHewitt wrote:
| Could you write this in Java?
| Joker_vD wrote:
| Not my code, but: https://gist.github.com/aruld/3965968
| ProfHewitt wrote:
| Does the github Java code make use of recursion?
| Joker_vD wrote:
| As you can clearly see, it does not. It also doesn't use
| any forced typecasts to circumvent type checking.
| ProfHewitt wrote:
| Is FuncToFunc defined recursively in the excerpt below???
| private static interface FuncToTFunc<T> {
| Func<T> apply(FuncToTFunc<T> x); }
|
| BTW, what is "x" in the above?
|
| Also is Func defined mutually recursively with FuncToFunc
| in excerpt below? public static <T>
| Func<T> Y(final Func<Func<T>> r) { return
| ((FuncToTFunc<T>) f -> f.apply(f))
| .apply( f -> r.apply(
| x -> f.apply(f).apply(x))); }
| bidirectional wrote:
| I think it is approximately `public <T> T y(Function <T, T>
| f)`.
| ProfHewitt wrote:
| Thanks!
|
| Could you use your Java code to define Factorial?
| jhallenworld wrote:
| Here is Y-combinator in many languages:
|
| https://rosettacode.org/wiki/Y_combinator
| bidirectional wrote:
| Can you type that in System F? It doesn't seem logically
| valid, a -> a is trivially true, but apparently implies any
| a?
| scapp wrote:
| System F isn't consistent as a logic (pretty much precisely
| because it has general recursion). In languages with
| general recursion, you can do things like
|
| (Haskell) anyType :: a anyType =
| anyType
|
| or
|
| (Rust) fn any_type<T>() -> T {
| any_type() }
| Joker_vD wrote:
| I still think it's a device of rather dubious value, the most
| actual use of it I've seen is from being able to do it at the
| type-level (in one of Kiselyov's articles), because honestly, if
| you are allowed to name things at all, getting the function to
| refer to itself is pretty straightforward:
| factorial' self n = if n == 0 then 1
| else n * self self (n - 1) factorial n = factorial'
| factorial' n
|
| That's it. Unless your evaluation strategy is literally
| implemented as term substitution/rewriting, it's about as
| efficient as having actual letrec primitive.
|
| This technique is straightforwardly extended to the case of
| mutual recursion: even' even odd n =
| if n == 0 then True else odd even odd (n
| - 1) odd' even odd n = if n == 0
| then False else even even odd (n - 1)
| even n = even' even' odd' n odd n = odd' even' odd' n
| arethuza wrote:
| "if you are allowed to name things at all, getting the function
| to refer to itself is pretty straightforward"
|
| The neat thing about the Y-combinator is that it allows
| recursion to be defined in systems, such as the lambda
| calculus, which don't have naming and therefore a function _can
| 't_ refer to itself by name.
| Joker_vD wrote:
| Well, lambda calculus _does_ have names, but yes, I agree, it
| 's a very neat trick in environments where naming is heavily
| restricted, it gives you "anonymous recursion", so to speak.
| Church-encoding is another similarly neat trick, for
| environments with substitutions/applications but without
| built-in natural numbers.
|
| It's just that it seems there are not that many such systems
| used in practice except for "advanced type systems".
| kragen wrote:
| The applicative-order Y-combinator that Mike derives at the
| end, lf.(lx.f ly.x x y)(lx.f ly.x x y), can be
| straightforwardly compiled into SKI-combinators, which
| don't have naming at all.
|
| I agree that it's rarely justifiable to actually _run_ a
| translated version of this code, but sometimes it gives you
| an easy proof of non-termination for some kind of formal
| system, which often gives you an easy proof of
| undecidability, which can save you a lot of time trying to
| figure out how to compute the uncomputable. Or it may
| persuade you that adding some feature to your design is a
| bad idea because it eliminates termination guarantees.
| Joker_vD wrote:
| If all you need is a proof of non-termination, then
| encoding a whole of Y combinator is entirely superfluous:
| "(\f. f f) (\f. f f)" is quite enough already. In case of
| SKI calculus, that translates to "SII(SII)".
| Koshkin wrote:
| As the article points out, the value of the Y combinator is
| largely theoretical/aesthetical, in both of which aspects your
| examples suffer greatly: they are ad hoc, lack abstraction/code
| reuse (which is why, perhaps, you needed more examples), and
| they look ugly (at least to my untrained eye). The point of the
| Y combinator is that it is a beautiful, mathematically precise,
| abstract, purely-functional way of expressing recursion.
| Joker_vD wrote:
| "Ad hoc, lack abstraction/code reuse"? How does this
| fix f = f f almost_factorial f n =
| if n == 0 then 1 else n * f f (n - 1)
| factorial = fix almost_factorial
|
| lack code reuse compared to fix f = (\x. x
| x) (\x. f (\y. x x y)) almost_factorial f n =
| if n == 0 then 1 else n * f (n - 1)
| factorial = fix almost_factorial
|
| ? As for ugliness, well, it is indeed in the eye of the
| beholder: I personally think the fixpoint combinators that
| enable mutual recursion are pretty ugly, even more so than
| "(\x. x x) (\x. f (\y. x x y))".
|
| The only real problem is that in my approach the recursive
| calls look like "f closed_over_functions... new_args..."
| instead of "f new_args..." but that's what the compilers are
| for: this transformation is called "closure conversion" and
| is pretty straightforward. Sure, if you have to encode those
| things manually, then perhaps using Y is clearer and may even
| be the only option if you can't mess with the original
| definitions.
| selimthegrim wrote:
| Vanier was my instructor for CS 1 at Caltech, a couple years
| before it abandoned SICP and Scheme. A more dedicated lecturer is
| impossible to find.
| tromp wrote:
| Curiously, the graphical lambda calculus notation for the Y
| combinator slightly resembles a Y, especially when bent a little
| as shown at the top of
|
| https://tromp.github.io/cl/diagrams.html
| eru wrote:
| I always assumed that's where it got the same from?
| tromp wrote:
| The name Y combinator is many decades old, while this
| graphical notation is not even one decade old. But you do
| raise an interesting question:
|
| How did the fixed point combinator come to be known as the Y
| combinator?
| amw-zero wrote:
| Why was lambda chosen as the abstraction character in the
| lambda calculus? Mathematicians just pick random letters
| and symbols for things.
| amelius wrote:
| Probably just drawing letters from the alphabet.
|
| It's like the question: why do we use "x" to denote the
| unknown value in mathematics, most of the time?
| bidirectional wrote:
| The drawing random letters is true for the lambda in
| lambda-calculus, but _not_ true for (at least some)
| combinators. e.g. the K combinator derives from
| Konstanzfunktion, and I from Identitatsfunktion[1]. So I
| do think it is an interesting question why Y, and we can
| 't just assume it's arbitrary.
|
| [1]
| https://www.johndcook.com/blog/2014/02/06/schonfinkel-
| combin...
| amelius wrote:
| Then perhaps this reply comes closest to the truth:
|
| > Y because the letter Y has one stem which splits in
| two, just like what the function does. That's probably
| the reason, or at least that's how I look at it.
| amelius wrote:
| They should draw these diagrams upside-down.
|
| Then they resemble a l.
| kragen wrote:
| This is gorgeous!
___________________________________________________________________
(page generated 2021-06-29 23:02 UTC)