Zulip Chat Archive

Stream: general

Topic: function.blah


view this post on Zulip Reid Barton (May 14 2020 at 15:56):

Did something happen where f.foo means function.foo f when f is a function?

view this post on Zulip Reid Barton (May 14 2020 at 15:56):

or was that just a suggestion?

view this post on Zulip Gabriel Ebner (May 14 2020 at 15:56):

No, I'm still waiting on a PR.

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 15:57):

AFAIR, last thing happening was Gabriel pointing at the C++ source file that should be changed to achieve this.

view this post on Zulip Reid Barton (May 14 2020 at 15:58):

I was hoping we could rename the dreadful set.range to function.image--though I suppose we could do this anyways

view this post on Zulip Patrick Massot (May 14 2020 at 16:03):

Even better would be a trick to write f.map F where f is a function and F is a filter. Johannes sometimes wrote F.map f, I always try to write map f F

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 16:04):

What should the parser to to understand that f.map F is actually filter.map?

view this post on Zulip Patrick Massot (May 14 2020 at 16:30):

That's tricky, it must use that F is a filter. Maybe :four_leaf_clover:

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 16:30):

For filters you can probably use <$>

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 16:31):

But this wouldn't work for bundled homomorphisms.

view this post on Zulip Mario Carneiro (May 14 2020 at 16:31):

there are universe issues with this alternative

view this post on Zulip Patrick Massot (May 14 2020 at 16:31):

I thought this never works because of universe issues

view this post on Zulip Patrick Massot (May 14 2020 at 16:32):

Oops, Mario was faster

view this post on Zulip Mario Carneiro (May 14 2020 at 16:32):

It works as long as you are on a known type, which is probably in Type, but anything generic wants to have two universes

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 16:39):

I forgot about universes. Again.

view this post on Zulip Patrick Massot (May 14 2020 at 16:39):

Yes, that's one effect of the virus lock-down. It becomes even easier to forget about the outside universe.

view this post on Zulip Johan Commelin (May 14 2020 at 16:42):

Can the universe issues with <$> be fixed? Or are they inherent?


Last updated: May 16 2021 at 21:11 UTC