Zulip Chat Archive

Stream: new members

Topic: Function that takes a pair


view this post on Zulip Iocta (Dec 13 2019 at 20:54):

I'm getting started. The tutorial wants me to write a function def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := sorry but I'm not sure the syntax for writing a function that it would take as an argument.

I tried

def g : ℕ  ×  ℕ ->  ℕ := λ x y, x + y
#eval g (5, 3)

but it doesn't seem to like that: "failed to synthesize type class instance".

view this post on Zulip YH (Dec 13 2019 at 20:58):

def g : ℕ  ×  ℕ ->  ℕ := λ ⟨x, y⟩, x + y
#eval g (5, 3)

view this post on Zulip Iocta (Dec 13 2019 at 21:00):

Thanks.

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 21:09):

YH's trick used to confuse me when I was beginning. It's a clever and important trick, but you can also do this:

def g :   ×   ->   := λ xy, xy.1 + xy.2

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 21:11):

Either way, the point is that ℕ × ℕ is one type, so λ x y, can't be the way to start. That's why you got the error.

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 21:12):

As a professional mathematician who knew essentially nothing about functional programming when I started, I took a while to get the hang of all this basic stuff; on the other hand computer science undergraduates with a Haskell background find the whole thing trivial.

view this post on Zulip Iocta (Dec 13 2019 at 21:21):

I see. I am checking out Lean after watching your recent talk on youtube. :-)

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 22:03):

Great! When you're finished with Theorem Proving In Lean you could try the natural number game

view this post on Zulip Bryan Gin-ge Chen (Dec 13 2019 at 22:06):

A while back as a demo for some other stuff, I made a little interactive walkthrough about currying and uncurrying in Lean. Not sure if it's pitched at the right level (it assumes that you're OK with Lean's basic syntax), but you might find it helpful nonetheless.

view this post on Zulip Johan Commelin (Dec 14 2019 at 05:36):

Whoow! @Bryan Gin-ge Chen That's really fantastic! The way you walk through interactively writing the code, see the tactic state (and expected types), and have your explanation right below. Really really great!

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 07:43):

What does

To use it yourself, add footer: stepEditor(steps, index) to the options object of leanEditor, where steps is an array of objects (see below) and index (optional, set to 0 by default) is the starting index.

mean? I am reading it as meaning "before you go any further, change an option in a place which you don't understand (the "options object of leanEditor").

view this post on Zulip Bryan Gin-ge Chen (Dec 14 2019 at 07:49):

Sorry, those are instructions for people who would want to use this function in another Observable notebook. I ought to to make that more clear.

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 08:25):

Bryan I would happily promote these little notebooks on Twitter. I have followers who are in to little "gimmicky" stuff like this. Maybe you should send me a random list of cool little things you've done and I can shout them out. I still have under 1000 followers but it slowly goes up and I'm trying to figure out what works well in the ecosystem there; I suspect that this stuff might.

view this post on Zulip Bryan Gin-ge Chen (Dec 14 2019 at 08:38):

Thanks Kevin, feel free to share any or all of the notebooks in this "collection". @Kevin Kappelmann also has several neat tools / templates for Lean notebooks here.

I haven't had much time for Twitter recently, but my account is here. To be honest, at the moment I'd prefer to fix up my notebooks a bit more before making any kind of publicity push, as there are still lots of things I could do to make the editor more user friendly.

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 15:58):

In the walkthrough linked to above, why not (a) delete all the stuff about how you made it and just make it a stand-alone thing with a link to a "how I did it" page, and (b) add a 15th page with the formalised sorried examples such as uncurry add' = add and curry uncurry = idso the user doesn't have to figure out how to formalise the statements? If they're interested they will figure out some more questions on their own after they've done the easier job of filling in the sorrys

view this post on Zulip Bryan Gin-ge Chen (Dec 14 2019 at 16:49):

Great suggestions! I'll try to implement them soon.


Last updated: May 09 2021 at 18:17 UTC