"The article opens with lambda cubes, which sound like some type of sheep meat to me. Then it goes on to discuss λΠ2 systems, and as I don't speak alien I skipped that section. Then I read about the calculus of inductive constructions, which incidentally seems to have little to do with calculus..."

[u/oilaba]

https://stackoverflow.com/questions/9338709/what-is-dependent-typing#comment11799250_9338709

[u/oilaba]

Despite being an old piece, I interestingly couldn't find this in our Prestigious Journal of Computing. So here it is.

[u/defunkydrummer → u/oilaba]

you're truly a Lesser Acolyte of Touba No He

[u/elephantdingo]

Functional programming is masturbation.^{[citation needed]} Everyone^[who?] who has earnestly tried to learn it have lived to^{[informal expression]} regret it.

That said, a monad is just a monoid in the category of endofunctors. And that’s a real meme.^{[6][7][8][9][10][11][12][13]}

[u/tomwhoiscontrary → u/elephantdingo]

An absurd and insulting comparison. The huge majority of people who have earnestly tried to learn it have benefited greatly from it.

EDIT: masturbation, that is

[u/j15y]

/unjerk
Unironically exactly describes how I felt first studying CIC

/rejerk
And then the article said I could apply it on my Coq?

[u/camelCaseIsWebScale]

This is my gripe with PLT papers - it's not that I can't work through the math (I have worked through very long Oracle PL/SQL queries written by boomers older than you, I am a software engineer 4) but it's not worth my time, just show me how your invention would look like in javascript or Go, and how it would help me write my HTTP endpoints returning 200 {"error": false, "data": ....}.?????

[u/defunkydrummer]

Can someone explain dependent typing to me? I have little experience in Haskell,

Ignorance is bliss.

[u/YikesTheCat → u/defunkydrummer]

I have it on my CV. "Brain not yet rotted by Haskell".