Zulip Chat Archive

Stream: general

Topic: monad refactoring


view this post on Zulip Patrick Massot (Mar 01 2018 at 07:45):

@Sebastian Ullrich woke up with a lot of homework... Does anyone knows whether basic users like me will see any difference after merging this?

view this post on Zulip Simon Hudon (Mar 01 2018 at 07:51):

Are you referring to the commits in his own fork?

view this post on Zulip Sean Leather (Mar 01 2018 at 07:53):

To avoid ambiguity and for posterity: https://github.com/leanprover/lean/pull/1881

view this post on Zulip Simon Hudon (Mar 01 2018 at 07:58):

Thanks @Sean Leather

view this post on Zulip Sean Leather (Mar 01 2018 at 08:01):

woke up with a lot of homework... Does anyone knows whether basic users like me will see any difference after merging this?

@Patrick Massot: I'm guessing you're referring to Leo's comments, of which there were a lot.

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:01):

Yes.

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:06):

There are a lot of comments but there is a lot of code in this PR.

view this post on Zulip Mario Carneiro (Mar 01 2018 at 08:07):

I'm also curious about this. @Sebastian Ullrich , could you maybe discuss or point to a place where you discuss the purpose of the monad refactoring project? From what little I can garner from Leo's comments, it looks like you are maybe adding more advanced monad features from Haskell like monad transformers, the continuation monad and call/cc?

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:08):

I think you'll see a difference (hopefully for the best) if you use Lean to write programs. Otherwise, I don't think you'll see a difference

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:08):

It's very hard to resist going to Leo's most cryptic comment and add: "Yeah, I wondered about that too".

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:08):

What do you mean "write program"? Write a tactic?

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:09):

I think not much if you write tactics. More if you use Lean as a functional programming language (with or without much verification)

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:10):

Are there people doing that?

view this post on Zulip Sean Leather (Mar 01 2018 at 08:10):

As in I/O?! :scream:

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:11):

On top of my head, there's me

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:12):

I/O or other kind of code. There's a lot you can do with monads

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:12):

Why do you seem so scared of I/O?

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:12):

Doesn't sound functional to me

view this post on Zulip Sean Leather (Mar 01 2018 at 08:12):

I meant, as in writing a “real” program that does I/O, not as in using the io monad... :wink:

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:13):

Doesn't sound functional to me

Why not?

view this post on Zulip Sean Leather (Mar 01 2018 at 08:14):

Why do you seem so scared of I/O?

Because of the meme that theorem-proving languages are generally only used for proofs and type-checking.

view this post on Zulip Kevin Buzzard (Mar 01 2018 at 08:14):

Doesn't sound functional to me

Why not?

Every article I read about functional programming makes a huge fuss about i/o. That's probably what he means. In contrast to procedural languages, where the first program you ever see is "print hello world"

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:14):

I thought functional programming swears to be isolated from real world

view this post on Zulip Sean Leather (Mar 01 2018 at 08:15):

I thought functional programming swears to be isolated from real world

That's a myth and a well-disproven one at that.

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:15):

That was true of Haskell before they invented monads but the io monad makes I/O into a perfectly ok part of pure functional programming.

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:16):

Some people write OSs and web servers using purely functional programming. It looks pretty real to me and their users :)

view this post on Zulip Sean Leather (Mar 01 2018 at 08:17):

It's funny how, as you climb up the ladder of high-level programming languages, each level above seems to be less useful than the level you're on, at least until you understand it.

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:17):

What's funny is right now I'm staring at my NodeJS I/O code which doesn't work. I don't know why it insisted trying to read all 29668 files in this directory before starting to work on the first one (and then FATAL ERROR: CALL_AND_RETRY_LAST Allocation failed - JavaScript heap out of memory)

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:18):

Yeah! And as I climb up, I get nervous about climbing down. Everything makes sense up here!

view this post on Zulip Sean Leather (Mar 01 2018 at 08:18):

Yes, you can get complacent with all of the protection you have.

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:19):

I love functional programming languages guys. They are brothers to mathematicians. We also think what we do is more powerful and more beautiful than what other do. And normal people think what we do is un-understandable and useless

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:20):

I have a friend whom i'm mentoring with Haskell. He works with JavaScript. He's more courageous than me. I don't think I'd want to go back to object oriented programming ... unless it was generated from afull functional specification

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:20):

And we're also insufferable when coming in contact with other communities

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:21):

In my case the trouble is not object oriented programming, it's asynchronicity

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:21):

"You're getting into trouble because your pointers are aliasing each other? How quaint!"

view this post on Zulip Sean Leather (Mar 01 2018 at 08:22):

Aliased pointers in JavaScript? :confused:

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:22):

Object oriented programming is supposed to be a solution (some might disagree cough cough) but asynchronicity is an actual programming challenge ... at the center of my research as it happens

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:23):

Aliased pointers in JavaScript? :confused:

References to objects, etc. I'm fairly sure they don't have a complete value semantics

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:24):

It's fun here but I need to take a shower, see you

view this post on Zulip Simon Hudon (Mar 01 2018 at 08:25):

Alright! Let's be insufferable later! :grin:

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 09:58):

I'll leave this link as a hint to our motivation... :P https://github.com/Kha/syntax/blob/master/macro.lean#L5

view this post on Zulip Scott Morrison (Mar 01 2018 at 11:40):

Hi @Sebastian Ullrich , is there some explanation I can read of what you did to bind?

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 11:42):

@Scott Morrison Does the test file help? https://github.com/leanprover/lean/blob/master/tests/lean/run/rebind_bind.lean

view this post on Zulip Scott Morrison (Mar 01 2018 at 11:42):

There are lots of places mathlib has broken, e.g.

theorem length_bind (l : list α) (f : α  list β) : length (bind l f) = sum (map (length  f) l)

view this post on Zulip Scott Morrison (Mar 01 2018 at 11:43):

Where is says

type mismatch at application
  l >>= f
term
  f
has type
  α → list β : Type (max u v)
but is expected to have type
  α → list ?m_1 : Type u

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 11:45):

Ah, list.bind is protected now, as it should have been from the beginning

view this post on Zulip Scott Morrison (Mar 01 2018 at 11:46):

So it should use ...?

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 11:47):

You can replace bind with list.bind

view this post on Zulip Scott Morrison (Mar 01 2018 at 11:47):

thanks

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 11:49):

But I would argue that we should usually prefer using the generic operations (i.e. bind/>>= here) even if it means that alpha and beta have to live in the same universe in this case

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 11:49):

@Mario Carneiro thoughts?

view this post on Zulip Scott Morrison (Mar 01 2018 at 12:09):

The other place I'm seeing trouble from the monad refactoring is in mathlib's data/encodable.lean.

view this post on Zulip Scott Morrison (Mar 01 2018 at 12:10):

where it looks like the problem is that there are too many binds available

view this post on Zulip Scott Morrison (Mar 01 2018 at 12:10):

and the do notation is now failing as a result.

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 12:47):

I guess option.bind should be protected as well? Gaah.

view this post on Zulip Mario Carneiro (Mar 01 2018 at 14:35):

The "named" bind is there in part exactly for this universe distinguishing thing. There are times when it matters, and you need the polymorphic version. For most of these operations, there is also a symbol name for them, which is preferred when universes don't matter or you are over a known structure.

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 14:44):

Yah, it's the curse of the monad. I'll mark option.bind as protected then.

view this post on Zulip Simon Hudon (Mar 01 2018 at 22:14):

I took the liberty of commenting on your pull request. Is this the best way to interact on this subject or should I stick to Zulip / Gitter?

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 23:00):

That's fine, I just didn't get to it yet

view this post on Zulip Simon Hudon (Mar 01 2018 at 23:01):

No worries. I just don't want to be intrusive by commenting directly on github

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 23:11):

I'm happy for any feedback by experienced Haskell programmers, since neither Leo nor me is one of them

view this post on Zulip Simon Hudon (Mar 01 2018 at 23:20):

Excellent then :) I'll keep them coming. In passing, I am truly amazed by the language that you guys came up with. Learning Haskell was like a religious conversion for me and it ended a three year programming hiatus. Lean is comparing really well

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 23:30):

Thank you :smile:


Last updated: May 13 2021 at 20:13 UTC