## Stream: new members

### Topic: TPIL question, lambda defs

#### Daniel Donnelly (Aug 26 2019 at 04:08):

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 (Aug 26 2019 at 04:36):

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 (Aug 26 2019 at 04:38):

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

#### Daniel Donnelly (Aug 26 2019 at 04:41):

@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 (Aug 26 2019 at 04:41):

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

#### Daniel Donnelly (Aug 26 2019 at 04:42):

oh, I think I get it now

#### Daniel Donnelly (Aug 26 2019 at 04:43):

#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 (Aug 26 2019 at 04:44):

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

#### Daniel Donnelly (Aug 26 2019 at 04:45):

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

#### Daniel Donnelly (Aug 26 2019 at 04:46):

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

#### Keeley Hoek (Aug 26 2019 at 04:46):

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

#### Daniel Donnelly (Aug 26 2019 at 04:46):

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

#### Daniel Donnelly (Aug 26 2019 at 04:48):

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 (Aug 26 2019 at 04:55):

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

#### Marc Huisinga (Aug 26 2019 at 11:55):

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 (Aug 26 2019 at 12:10):

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 (Aug 27 2019 at 10:43):

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.

Last updated: May 16 2021 at 20:13 UTC