Stream: new members
Topic: Function that takes a pair
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.
def g : ℕ × ℕ -> ℕ := λ x y, x + y #eval g (5, 3)
but it doesn't seem to like that: "failed to synthesize type class instance".
def g : ℕ × ℕ -> ℕ := λ ⟨x, y⟩, x + y #eval g (5, 3)
Iocta (Dec 13 2019 at 21:00):
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
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.
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.
Iocta (Dec 13 2019 at 21:21):
I see. I am checking out Lean after watching your recent talk on youtube. :-)
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
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.
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!
Kevin Buzzard (Dec 14 2019 at 07:43):
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").
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.
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.
Bryan Gin-ge Chen (Dec 14 2019 at 08:38):
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.
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
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