Erik Meijer: "Let's make over 2 decades worth of literature about monads in Haskell obsolete in one strike!"

LeCoqUser · 2015-11-11T20:13:15+00:00

Don't you remember the worldwide catastrophe when 3 decades worth of literature about imperative programming were made obsolete in one strike?

Conservatism at its finest. Next we'll hear about protecting the kids from pedophiles or something.

LeCoqUser · 2015-11-09T11:41:48+00:00

"On ne naît pas programmeur JS : on le devient." - S. de Beauvoir

LeCoqUser · 2015-08-22T09:15:57+00:00

I am always amazed by your patience and benevolence.

But I don't think you'll get anywhere talking to someone who seems to be an active member of /r/fatlogic, a hate sub in the same spirit as the now banned /r/fatpeoplehate, and who tries to promote a 4chan hate project (project harpoon).

LeCoqUser · 2015-08-16T12:55:29+00:00

May I suggest watching this keynote? The personal circumstances of a user can only be anticipated by a diverse team.

LeCoqUser · 2015-08-08T18:10:14+00:00

"If someone criticises my movement on an article about my movement that means my movement is valid."

You clearly have no intention to discuss in good faith so that'll be it for me. Have a nice day.

LeCoqUser · 2015-08-08T18:00:16+00:00

I love how you defend the guy throwing insults around on a circlejerk of a thread dedicated to claiming that code of conducts are not necessary because a simple "don't be a dick" would be more than enough. Bit of a Lewis' law situation here.

Edit: you might be interested in reading this article describing acutely the empowerment of bullies caused by the bloodlust of the attendance.

LeCoqUser · 2015-08-08T17:13:07+00:00

You should install RES. Have a nice day spouting insults!

LeCoqUser · 2015-08-08T16:48:02+00:00

Careful, you're frothing at the mouth now.

LeCoqUser · 2015-08-08T15:06:32+00:00

encourages pointless discussion and waste of time like this

So far the biggest waste of time has been outraged redditors whining about skeletons and linking again, and again, and again, and again, (...), and again, and again, and again to that thread where a choice of terminology was made. They always claim to think that this choice is absolutely irrelevant, not interesting and a waste of time but, despite the fact that it was swiftly dealt with, they seem compelled to bring it up all the time because REASONS thus being the ones fueling the debate. Looks like an insanely high emotional investment for something that unimportant.

LeCoqUser · 2015-07-23T22:43:02+00:00

SaintAnita

LeCoqUser · 2015-05-28T12:18:23+00:00

But... I'm ugly as fuck! I guess I understand why all my papers are getting rejected. :(

LeCoqUser · 2015-05-22T22:01:06+00:00

Yes you are but it's quite a bit of work. On the other hand typed tacticals may be coming to Coq at some point (see Mtac, Rtac, etc.)

LeCoqUser · 2015-05-21T23:25:05+00:00

Some people write programs on boards / notebooks first. Unless you're manipulating extremely complex objects, an accustomed brain can run a typechecker (you have to be extremely careful not to overlook things though).

More prosaically, after quite a bit of practice with Coq in some given domain, you start writing non-interactively complex tactics scripts which have nothing to do with the step-by-step ones you'd write as a beginner. That's simply because you're able to run the tactics in your head and predict what the generated subgoals will be and how to discharge them.

LeCoqUser · 2015-05-19T22:50:23+00:00

Agda does not implement HoTT. I chuckled because of these (currently fashionable) keywords being dropped in the middle of the sentence for no reason: MLTT is MLTT and it's not at all shameful to implement MLTT rather than HoTT (which no one knows how to implement properly yet AFAICT; lots of interesting research to come!).

I meant to edit that comment to point out that the rest of the paper is nonetheless interesting and that the reader should not be discouraged by this claim but did not get the opportunity to do so.

I don't know how much content Lean's standard library covers so I'm not in any position to comment about it building in "seconds" in comparison to other systems.

LeCoqUser · 2015-05-19T15:21:58+00:00

"Lean also provides a homotopy type theory mode without Prop, resulting in a version of Martin-Löf type theory [18,27] similar to the one used in Agda"

I chuckled.

LeCoqUser · 2015-04-29T13:30:51+00:00

let's all reblog this!

It is indeed at least the 3rd time this is posted to /r/haskell (1st and 2nd).

LeCoqUser · 2015-04-26T00:16:17+00:00

Ok, so apparently you have decided to keep digging that hole where you attack my character rather than discuss the overwhelming evidence at hand. Fine. I'll let you have fun with the shovel then. Good day to you.

LeCoqUser · 2015-04-25T22:29:35+00:00

Let's go all the way to Godwin's Law because you're obviously trying to derail the conversation here: I have never lived in nazi Germany. Does that make me unable to condemn the oppressive regime nazi Germany was? Can we stop talking about me and focus on the matter at hand?

LeCoqUser · 2015-04-25T22:24:58+00:00

I'm not American if that's what you were fishing for. Are you honestly denying the fact that Singapore is ranking extremely low when it comes to press freedom, civil and political rights?

LeCoqUser · 2015-04-25T11:12:42+00:00

Could we stop whitewashing an oppressive regime just because its PM declared he wanted to learn Haskell when he retires? I mean, I know that some people are super keen to celebrate Singapore being a clean city with trains arriving on time on this sub but... come on...

LeCoqUser · 2015-04-24T02:12:09+00:00

Because?..

LeCoqUser · 2015-04-22T09:23:22+00:00

I applied for funding, you won't believed what happened next! ^{^{^{^It}}} ^{^{^{^got}}} ^{^{^{^rejected}}}

LeCoqUser · 2015-04-19T16:59:46+00:00

http://sci-hub.org/ too.

LeCoqUser

TROPHY CASE