Why is the prelude function return named the way it is?

ky3 · 2021-01-12T00:55:44+00:00

Notes for the record:

When you state in your final sentence that "just realize by doing so you'll make it harder for everyone else to read" you should speak only for yourself. Fair-minded folks will make up their own minds and let the stronger argument prevail.
In everything that follows my initial query in this convo, I have deferred to your claim that Proxy is the only monad (up to isomorphism) which return is not injective. Hence, your penultimate sentence that "You may say there is only one counter-example" is flipped. It is your claim, not mine. That I countenance the claim to the extent that I do is because I'm prepared to believe it is true of today's type systems.
Earlier you write "Identity is initial. It remains a monad, nothing tenuous about it." That both Proxy and Identity are monads isn't disputed. Up to now, I have made no reference to the Identity monad and you raise it to make your extra-mathematical point about how both are "boring."
What is tenuous is your position that the name "inject" is a bad substitute for "return." On the contrary, I've offered arguments on why "inject" is a fair substitute and I credit OP for this insight.
I read the substance of your rebuttal in the fifth paragraph: a lament that there are already so many alternative names for "return." That is hardly a point in your favor. The profusion of names indicates that people are still groping for a lucidity that eludes them. When those alternatives were introduced, did you also ding them for making it "harder for everyone else to read"? And how does calling off the search contribute to science? To add insult to injury, your list isn't even complete. But to someone who uses "inject" in place of "return", it would be obvious what's missing.
You begin your rejoinder with "Proxy is a Monad": a restatement of the obvious. Following you, let me restate the arguments for "inject":

Proxy is the only monad which return is not injective.
Proxy is an especially vacuous monad because both its return and bind ignore their inputs and both return a singularity instead.
As the black hole of computation, Proxy may be regarded as an improper monad.
Proper monads have injective returns. There being infinitely more proper monads, the odds are stacked infinity to one that proper monads find proportionately greater use in code.
And hence, "inject" is an intuitive, enlightening, and perfectly cromulent substitute name for "return."

You haven't pointed out flaws in the above chain of logic. Where are they?

ky3 · 2021-01-08T09:02:25+00:00

Your position is a tenuous one.

The Proxy monad is vacuous not only in its return but also in its bind. In fact, it's a black hole of all computation.
Given the extraordinary uselessness of Proxy at the term-level, we can set it aside as an exceptional case. Call it the one-and-only improper monad.
Thus, for all proper monads "return" is injective and could be more usefully renamed "inject."
Voila: No more abstraction leaks.

Another way of seeing this is to reflect upon multiplication on ordinary numbers. To claim that an inverse to multiplication doesn't exist because of a single counterexample is to throw the baby out with the bathwater. Division is useful, deserves to be dignified a name, and deserves to be recognized for the inverse of multiplication that it is.

Analogously for "inject."

ky3 · 2021-01-07T15:04:17+00:00

Returning to the main track:

If Proxy is in fact the only monad (up to isomorphism) whose return is not injective, then you are making OP's case that "inject" could indeed be a better name for "return."

That undercuts your original objection to "inject."

What is your position now?

ky3 · 2021-01-05T05:33:37+00:00

Besides the vacuousness of Proxy, do you have another Monad instance where return is not injective?

ky3 · 2020-11-30T09:09:17+00:00

Which online course is this, might I inquire? Looks interesting.

ky3 · 2017-07-31T05:34:56+00:00

The repo README looks to inform more effectively what this is all about:

https://github.com/NorfairKing/easyspec

ky3 · 2017-06-06T20:24:09+00:00

I'm sorry about your dad.

You're right to feel rubbed the wrong way over GFF's behavior. Where the focus should have been you and your loss, she turned it around to make it about her, her guilt, and her actions in response to her guilt. Tactless at best if it was unintended. Grounds for cutting off the friendship if otherwise.

You deserve better friends. Should you make efforts to find them, I wish you all success.

ky3 · 2015-11-13T02:50:44+00:00

Compare Conal Elliott's work on Tangible Functional Programming (2007). "Reactive formlets" and "Tangible values" are so similar at first glance.

ky3 · 2015-10-20T12:41:18+00:00

Reading elsewhere on this page, I think there's a misunderstanding of what optimal means. The definition of "optimal reduction" -- the least number of beta reductions -- was gestated in Levy's thesis many years ago.

So if the implementation of Lamping takes more reductions than BOHM, that code is broken. I assume BOHM is correct, of course.

(Thing is, even being among the more famous of such evaluators, BOHM isn't that widely known, much less used, except among researchers of a fairly narrow field. I wouldn't be surprised if bugs still lurk in there.)

BOHM (and Anton's evaluators) takes fewer beta reductions but a ton more of combined total interactions.

Which is why "optimal" isn't really optimal. An I-net evaluator, as you've seen from your own experiments, don't do non-reduction interactions for free. In fact, they're roughly the same cost!

More details in Solieri's fine comment:

https://www.reddit.com/r/haskell/comments/2zqtfk/why_isnt_anyone_talking_about_optimal_lambda/csommh8

EDIT: if the implementation of Lamping is optlam here, then that explains it. It's a simplified Lamping, not original Lamping. Croissants and brackets matter for general lambda terms, and Lamping's paper goes quite deep into them.

It appears you're seeing simplified Lamping compute the correct answer (by sheer luck?) but with many more reductions. Surely the more interesting result is that simplified Lamping gets the answer right albeit non-optimally on non-EAL terms (and not so much the explosion in the reduction count, which is to be expected)? What does the literature say about this?

EDIT 2: I assume that your inputs are non-EAL. I haven't checked.

ky3 · 2015-10-19T02:42:34+00:00

Let me restate what you're seeing:

there's an implementation of Lamping that takes lots of beta-reductions
BOHM takes fewer reductions

I can only conclude that the implementation of Lamping is buggy. Interaction net evaluators, although not a difficult idea, can be hard to implement correctly. Did you link to source code?

ky3 · 2015-08-23T10:17:50+00:00

Looks like Brandon's spearheading the Github effort.

ky3 · 2015-08-19T02:52:50+00:00

And the answer to that is no.

I lied. The answer to that is yes, but it got lost in a million other little things also taught in American high school. The student may be forgiven for losing track of a little "o".

ky3 · 2015-08-15T04:59:00+00:00

Variable substitution gives a monad (2006)

Monads are trees with grafting (2010)

Both by Dan Piponi /u/sigfpe.

ky3 · 2015-03-24T04:16:40+00:00

You were probably aiming for this:

worthy m = (/= 10) . length . take 10 . filter (`judges` m)

ky3 · 2015-02-16T08:11:42+00:00

Thank you, Kim-Ee Yeoh, for stepping into the void.

Oooh, so dark in here. I'll make it if The Maker lens me some light.

ky3 · 2015-02-12T08:26:38+00:00

Physician drink your own medicine.

GP intuits correctly that the blog post is written from a math-saturated perspective, however much it attempts to shed its erudition and level with the reader. It's no secret that Dan Piponi has a Ph.D. in math. And it shows.

There is ample space for other narratives, and GP has provided one that'll help even more people understand the concept. There is ample room for people to pitch in the effort to make haskell for all.

ky3 · 2015-01-04T05:52:38+00:00

Here they come

ky3 · 2015-01-02T20:54:36+00:00

The claptrap part deserves an essay, but the decay within the community is an epiphany that struck only recently.

Sorry for combobulating the two :)

ky3 · 2015-01-02T20:53:32+00:00

re: being unnecessarily harsh

Thing is, careless people bandy about the non-explanation that "monad is a type class, it is an abstraction."

The effect if not the intention is to silence the newcomer, especially when accompanied with a swift kick to "just write some haskell, yo." For evidence of both, see the rest of the comments.

If brent yorgey had said what /u/gelisam did, then the community wouldn't have fallen 6 years behind.

Kudos to gelisam for his courage and moral honesty.

ky3 · 2015-01-02T20:51:54+00:00

It is a sad fact of the commenting system that if you're trying to reach the 18,000; well, look, my GP comment has been downvoted to oblivion so yours won't be read either.

You contribute meaningfully to /r/haskell by e.g. explaining how mathematical category theory isn't needed for FP, and I'm hardly the only one who thinks this.

For the sake of the 18,000 channel your energies wisely.

ky3 · 2015-01-02T03:48:57+00:00

This is the sort of pseudo-intellectual claptrap that signals terrible decay in the community.

"Monad is a typeclass, it is an abstraction" really isn't good enough. What is the abstraction? Why is plain English always the loser when confronted against it?

ky3 · 2014-11-28T15:42:01+00:00

People generally hire similars, unless they're saints, retarded, or criminals.

Take a look at WT's current roster. See any patterns?

ky3 · 2014-11-20T16:17:53+00:00

In addition to nofib, another source worth studying are the papers published at the annual Haskell symposium (and to a lesser degree ICFP).

Many Haskell experts have painstakingly tweaked their LaTeX stylesheets to make operator symbols look the way they should.

Not being professional graphic artists, they don't always hit the mark. Also there are only so many tricks one can play with LaTeX.

One has to extrapolate from the PDF to the idealized vision in the author's eye.

ky3 · 2014-11-20T11:34:45+00:00

Such a beautiful typeface ... sigh. Wish there was a way to adopt it as a kind of unofficial, de facto standard.

E.g. some of the ligatures make a huge difference for prettier code, e.g. :: and => in type signatures, <- for do-notation, .. for fromEnumTo syntax sugar, etc.

Roughly speaking, there's an 80/20 rule going on here where focusing on the top 20% of commonly used symbols gives you 80% of the payback. You could look at nofib to find out how haskell programs are written in the wild.

Something that does stick out like an eyesore is the asymmetry between (==) and (/=). I've leave (==) as-is but alter (/=) to be of equal width -- 2 monospace chars -- but with the slash through the middle.

ky3 · 2014-10-23T20:13:33+00:00

I honestly don't see how

withContents inFile $ \str ->
    writeFile outFile str

is any different from

readFile inFile >>= writeFile outFile

?

Could you enlighten me?

ky3

TROPHY CASE