[HN Gopher] Baking the Y Combinator from Scratch
       ___________________________________________________________________
        
       Baking the Y Combinator from Scratch
        
       Author : mprast
       Score  : 54 points
       Date   : 2025-04-09 19:04 UTC (3 hours ago)
        
 (HTM) web link (the-nerve-blog.ghost.io)
 (TXT) w3m dump (the-nerve-blog.ghost.io)
        
       | sva_ wrote:
       | If anyone wants this in a humorous 1 hour format, watch the
       | legendary Jim Weirich (rip) explain it here:
       | https://www.youtube.com/watch?v=FITJMJjASUs
       | 
       | Don't be discouraged that it is in Ruby as the concepts are
       | completely general. Great watch even though I never coded a line
       | of Ruby.
        
       | tromp wrote:
       | > you technically can't do name = term
       | 
       | But you can do                   let name = term in term2
       | 
       | by de-sugaring it to                   ((lname. term2) term)
        
       | mkagenius wrote:
       | Is there a technique to remember this? I will understand it today
       | and forget after a few weeks.
        
         | pvg wrote:
         | There's a way to remember smaller and smaller bits of it until
         | you terminate at a piece small enough to remember permanently.
        
         | bloppe wrote:
         | It's easier to remember if you use a more common notation:
         | (Y(f))(x) = f(f(f(...(x)...)))
         | 
         | Or express it in python, which is still a bit weird but
         | probably still more readable than pure LC to pretty much
         | everybody:                   def Y(f):             return
         | lambda x: f(Y(f)(x))
        
           | tromp wrote:
           | > (Y(f))(x) = f(f(f(...(x)...)))
           | 
           | I think that should be (Y(f))(x) = f(f(f(...)))(x)
        
       | fritzo wrote:
       | From scratch it's also easy dress up a quoted Y combinator as in
       | Lob's theorem. Start with the usual Y combinator
       | Y = \f. (\x.f(x x)) (\x.f(x x))         : (p -> p) -> p
       | 
       | which can produce a thing of type p from a function f : p -> p.
       | 
       | Now Lob's theorem states that []([]p -> p) -> []p, which can be
       | read, "if you have the source code to transform (the source code
       | of a thing of type p) to a thing of type p, then you can produce
       | the source code for a thing of type p". Let's embellish Y using
       | {} to denote the quoting comonad.                 Y' = \{f}.
       | (\{x}.{f{x{x}}}) {\{x}.{f{x{x}}}}          : []([]p -> p) -> []p
       | 
       | To get there, just add quotes as needed: f must be quoted, f's
       | result must be quoted, and f takes a quoted input.
        
       ___________________________________________________________________
       (page generated 2025-04-09 23:00 UTC)