Zulip Chat Archive

Stream: new members

Topic: TPIL question, lambda defs


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Daniel Donnelly (Aug 26 2019 at 04:38):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Daniel Donnelly (Aug 26 2019 at 04:42):

oh, I think I get it now

view this post on Zulip 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!

view this post on Zulip Daniel Donnelly (Aug 26 2019 at 04:44):

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

view this post on Zulip Daniel Donnelly (Aug 26 2019 at 04:45):

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

view this post on Zulip Daniel Donnelly (Aug 26 2019 at 04:46):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Daniel Donnelly (Aug 26 2019 at 04:55):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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