Comment by Icy0 | Hacker News Reader

Comment by Icy0 | Hacker News Reader

You can solve this by working backwards from the outside in, replacing a (b x) with c a b x wherever you can (not inside out, or else you get into an infinite loop!)

A cute alternative expression to solve the curried composition puzzle is c c c c c, just 5 c's in a row :)

Finally, Lean is a great language to do these puzzles in. See the following code:

  /-- Compose! -/
  def c (g : β → γ) (f : α → β) := g ∘ f
  /-
  ?f (?g (?h ?x))
  -/
  #reduce c (c c) c ?f ?g ?h ?x
  /-
  ?f (?g (?h ?x))
  -/
  #reduce c c c c c ?f ?g ?h ?x

I used Lean too earlier today :-)

I saw what each #reduce c c ... c did to explore the "palette" I had to work with, and then accidentally stumbled upon the answer that way. I also stumbled on the c (c c) c solution.

May as well include a formalized proof while we're at it:

  def c (g : β → γ) (f : α → β) (x : α) : γ := g (f x)

  example (h : γ → δ) (g : β → γ) (f : α → β) (x : α) :
      h (g (f x)) = (c (c c) c) h g f x :=
    rfl

  -- Or
  example  :
      (fun (h : γ → δ) (g : β → γ) (f : α → β) (x : α) => h (g (f x)))
        = (c (c c) c) :=
    rfl

Reply on news.ycombinator.com