TPIL question, lambda defs

Stream: new members

[Daniel Donnelly]

def double (x : ℕ) : ℕ := x + x
#reduce double 3    -- 6

def do_twice (f : ℕ → ℕ) (x : ℕ) : ℕ := f (f x)

#reduce do_twice double 2    -- 8
-- These definitions are equivalent to the following:

def double : ℕ → ℕ := λ x, x + x
def do_twice : (ℕ → ℕ) → ℕ → ℕ := λ f x, f (f x)

I'm not getting how the second do_twice definition is equvalent to the first since the second is of type (\nat \to \nat) \to (\nat \to \nat) via right associativity. In other words it should "return" function from nat to nat, however when you do reduce it, it equals a natural number which is not of the same type as nat to nat. Where is my reasoning stuck?

P.S. how do I do inline lean?

[Keeley Hoek]

It should evaluate to a function form nat to nat if you only pass it one argument. But you pass it two, further evaluating the function from nat to nat at a fixed nat.

[Daniel Donnelly]

@Keeley Hoek I get it now! Thank you, friend.

[Daniel Donnelly]

@Keeley Hoek okay, now I don't get it (again). Because of the type of do_twice is a map from maps to maps. So... I'm lost again

[Daniel Donnelly]

@Keeley Hoek I edited my post, not sure if you get a ping for that hence this.

[Daniel Donnelly]

oh, I think I get it now

[Daniel Donnelly]

#reduce do_twice double 2 is returning nat -> nat when called on double, but evaluated is 8. Now I get it, finallly! Thank you!

[Daniel Donnelly]

#reduce do_twice double would show the nat -> nat result

[Daniel Donnelly]

@Keeley Hoek you look like Collin Hanks (an actor, Tom Hanks' son)

[Daniel Donnelly]

:) in your avatar, but I didn't click on it

[Keeley Hoek]

You probably know this already, but this is a simple instance of https://en.wikipedia.org/wiki/Currying

[Daniel Donnelly]

@Keeley Hoek I'll read that article anyway to absorb some more of the formal thought about it

[Daniel Donnelly]

Yes, currying seems very valuable in this setting, as functions are first-class data objects in Lean. Not to mention they're verifiable, they're beyond first-class!

[Daniel Donnelly]

This is exciting. We're doing math and coding at the same time. :)

[Marc Huisinga]

kevin wrote something about this as well https://xenaproject.wordpress.com/2018/05/19/function-composition/
eta-conversion/-equivalence is a related idea that you might encounter occasionally

[Marc Huisinga]

as for doing math and coding at the same time; if you've read a bit of TPIL you'll have noticed that proving theorems in term mode is often very similar to programming in a functional language. although less common, you can often also use tactic mode to write code:

def first {α β : Type*} (tuple : α × β) : α :=
begin
  cases tuple,
  exact tuple_fst
end

#eval first (1, 2) -- 1

[Kevin Buzzard]

This is exciting. We're doing math and coding at the same time. :)

I noticed this two years ago and the excitement has still not worn off.