higherkinded's comments

Okay but they are formal systems and don't have anything to do with AI either, do they?

Don't.

Suggestion to rely on AI for proof verification is just laughable. Neuron weights instead of formal definitions. So reliable.

Curious! Instantiation by means of the language is actually slower than parsing stuff and instantiating the objects that way. Didn't ever think of that possibility before. Anyway, I understand that JavaScript is much more complicated to parse than bare JSON, but still, that just feels odd. Good read!

Lasting long against HN-mainpage-level load. That's what's hard.

Wrong Amazon, you again!

Add a <noscript> to your landing mayhaps? Takes a little while to figure out that I need my JS on for a proper representation.

Effectful sizeof, what a delightful feature!

Though the compile-time magic with structs and functional macros are so tempting that I feel like it's high time to do some C.

Not sure if I'm going to express an unpopular opinion on that matter but I'm pretty sure that ot was already said somewhere in the comments in some different form. Not sure if my opinion even counts to people like ones who authored this strange piece of text since I'm from the mischievous and sinister kind of people collectively called "straight white male", and thus I may not have the fitting amount of oppression points to be heard. But I'll try anyway.

I think that the article itself revolves heavily about some prestige or whatever. So here comes the first question: does the person who cares about prestige more than science possess the amount of dedication and discipline to get to the higher ranks? In my opinion, the answer is strong "no" at the very least. To be proficient and productive, to be useful, you have to dedicate all your hard work towards your chosen discipline. Apparently you must be interested very much in it. It doesn't just fall down upon the "privileged cast", it's a competitive field, and outcome of that, if any, depends on dedication and the ability to act smart without relying on anyone or anything else too much.

The second question will be: do you actually know better than the people who make their own life choices? I mean, they do things or don't do them for a reason. Sometimes it's bad, sometimes it's good, but if we talk about education and science, it's nothing close to sexism in the vast majority of cases.

The third part is simpler. What will happen if we enforce/regulate/implement quotas? The amount of useful output will decline. You can't force people into being effective and they will not be effective by "getting there" just by regulations and quotas.

And for the last one, some personal part. Last couple of years I study quite complex math (abstract algebra mostly) on my own out of pure interest in it. I don't have any mentorship, and I don't suffer from it. My dedication compensates for it. It's a bit anecdotal but I believe that you can achieve a lot just by being dedicated and interested. You will not get even close by being placed there and babysat until you're "big enough".

Think about it. Cheers!

"...so again, like I said earlier,.."

For some reason I've thought about the other Amazon. Even São Paulo didn't help the title to ring a bell.

>Youngsters these days

What a marvelous start, good luck looking trustworthy. It's straight up the same as it was generations and generations before. I also love the emphasis on video games imposed in this article, from the very beginning.

I have a different opinion on this. While I can confirm that some team-based games can tilt someone, it's unlikely that it contributes to mentioned suicide rates in any meaningful way. It's just the same kind of "youngsters these days" activity as it was before. The actual reason may lie deeper in the current state of human society. Fearmongering by the crackpot young adults who still didn't grow up themselves is but one manifestation of what's happening in the bigger picture.

I'm ashamed to admit, being the part of this "young adult" generation myself, that we're a laughable bunch of irresponsible wimps, relying on everything but ourselves to relieve the stress posed onto us by the ordinary "adult" problems. As the result, some of us easily fall the cult-like mobs, failing to recognize the stupidity of our derived positions and causing problems to people around us while hypocritically stating that we just want to make the world better. Our generation isn't strong enough. We ruin each other and the majority of us is too immature to take care of our "youngsters", which is the real reason behind them going rabid or just straight out killing themselves.

We are the ruined generation and we ruin our societies, and what's more important, our kids, the ones who are supposed to be the next building blocks for it. And it's most probably our fault. Or wait, do the games cause that? It's always someone else's fault, it's the guns who kill people, not the other people, it definitely must be the case this time, isn't it? What a mess.

Who would've guessed? Getting a kilometer of solar panels installed as a road (sic!) in a region that has a cloudy skies most of the time. It's borderline genius. How did it get any approval at all? Who treated solar panels being used as a road (probably to spend some more tax money on casing?) as a good idea? How is it not just obvious that it will not even get close to the easier and cheaper (rooftop panels) options? This imitation of environment care is so hilarious that I don't have the proper words to describe it.

The fact that someone needs to say that for it to be apparent is somewhat unsettling.

>cross the bridge

No one really wants that in any use cases of type-level numbers. Type-level numbers are generally used to do just opposite: silently (well, loudly, if you ask the compiler to check it) govern the structure in question, limiting, say, its arity or whatever. But if you want to "cross the bridge", I think it's still possible but tricky in case of Java. Don't get me wrong, I don't advocate for Java nor intend to write it, I just use it as a dummy trashcan language to illustrate concepts and their latency in a sense that you don't really need to use fancy X in order to do Y or express Z.

>20-30 static analysis tools

Too bad. I'm usually pretty happy with just plain compiler and a 80-char bar.

>huge value in gradual typing

Doubt that. It's actually a good safety net to stop a project from turning into a big ball of mud but it won't help unless used correctly and with the right intent.

>being able to explore interactively

Hindley-Milner type systems can infer your stuff so well that you usually don't have to worry about supplying type signatures at all. For instance, in Haskell you don't have to "add types" compared to what you do in REPL, you have them all the time and oftentimes you don't have to annotate anything, it's still static and usually done just to give an idea to other people what's doing what.

Oh, not about our little conflict but about Python: does it have some form of traits/typeclasses/whatever? I mean, yes, it has them in form of mixins but can it, in modern days, put a constraint on some type variable, saying that it must have some properties that are described in different traits?

>Much like java and javac are different tools, python and pytype/mypy are different tools

I get where you're heading. The `java` one is for JVM bytecode interpretation and the `javac` is for actual Java. Ok. Cool. I suppose that you do understand it well that leaving the choice on typechecking to external tools is something rather atrocious, do you?

>All of the python _I write_

The factory that produces the hammers for us carpenters provides just hammerheads alone and leaves us to choose and get the grips, so oftentimes fellow woodworkers use them without any grip whatsoever, some make flails and flail the nails, and I just go buy the soft grip from a third-party vendor. What's the problem here?

>[throws a Wikipedia link with the term definition at me, goes on showing me what must be done by a sum type]

You sure do consider me stupid, right? Anyway, what dependent types _usually_ do is they limit a category (think set) to some sub-category. Your example indeed describes dependent types but the problem with it is that it isn't a good place for dependent types. It can be expressed by sum types and I don't see any reason not to do so. By the way, do you have the sum types in Python nowadays?

>has generic types, not dependent types

(1) Look. Have you heard it anywhere that once you get powerful-enough generics, you can at least emulate dependent typing to some extent if not outright get it? Consider this: Java can express Peano numbers at the type level, along with Rust, C# and whatever there is with even remotely working generics. Do you know what that means to us here? Yes. We can express anything number-related at the type level, thus getting one little step closer to dependent typing. The most modest example of what you can do with that is a list with length limited on a type level, which qualifies pretty ok for dependent typing.

>not the _type_

Dependent typing is still about types, and if you work with these on a type level, you will deal with types. The type isn't inferred here but the value is limited by the type in question, so please don't say this, otherwise it will not constitute a sane type system. Imagine the types that just constatate the fact once it happened instead of setting an invariant (ah yes).

>with some massaging

Zero massaging[0] but ok. I hope that, knowing about [0], you've already guessed that there's an implementation of matrix multiplication with actual dependent types[1].

Actually, if you want, I could implement type-level floats for you but I'm not sure if they have any good use case and I'm pretty sure that some operations will compile for a little while: type families operating on numbers are usually defined in terms of recursion. Not sure if we're going to flex type systems at each other at this point, there's a clear winner even if we're not bringing the said to the table: static typing in Python isn't provided out of the box, and while your little example makes me check it out and appeals to me, it's still a third-party tool and that's not how it must be. I will not mention anything about types describing here. If that's not enforced by type system, it's pretty bad but there's no point in discussing that already, enough's been said.

>plainly cannot

Refer to (1).

[0]: http://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-Ty...

[1]: https://hackage.haskell.org/package/linear-code-0.1.0/docs/M...

Edit 1: one more link.

Edit 2: a suggestion and some out-of-place conclusion.

And how's it helping you verify the correctness of your codebase at compile time (it still compiles the source to byte-code before evaluation)? Last time I checked, it didn't care too much about type annotations, and it didn't type-check anything before execution without additional shoehorning.

>No other mainstream whatever

C#, Rust. Notice that I don't even mention my man Haskell or Scala while the latter one is really big.

>literal (dependent) types

Uh, even Java has dependent types, anyway. Read the docs.

>templates

Yes, that's parametric polymorphism. No, it's garbage in C++ to the point where you can't guarantee the soundness of a template. It's done in Java, Kotlin, C#, TypeScript, for the most mainstream ones, not to mention that (and how exactly) it's done in Haskell and Scala.

Edit: How do you feel about type-level programming, anyway? ;)

And that's a sad thing to hear. Before my death by thousand downvotes, I'd like to tell you why do I feel that way.

Back in the day when I was way more inexperienced than I'm now, I was a die-hard Python fanboy. To me, it seemed like a best option available due to it being way more concise and readable than JS/PHP, not to mention that it was way more powerful and dense. I didn't really bother with type safety at the time and I wasn't exposed to any real criticism of it at the time, as it happens often when you're just too new, and I was more than fine with it.

Time mercilessly marched forward since then. I worked with different codebases, changing tech stacks and languages a bit, learning new stuff and so on. With some experience, lots of self-education and a vast amount of different workflows to compare with, I've realized one important thing. While Python may be better than some languages that are considered trash by industry consensus, it's also a trashcan language to ones with sound and flexible type systems, not to mention that, across dynamically typed contenders, it's nowhere near as powerful as literally any solid Lisp.

That said, I feel bad for the industry that "dives into Python" more and more over the last years. While it may seem like a pretty easy and cool-ish language to write in, you will inevitably have large problems at scale, it just doesn't have what it takes to be easily scalable, and most importantly, it's just tedious to refactor when it's big, even though the language itself is mind-numbingly easy and even your grandma can jump right in.

In a conclusion I'd like to say that you'll be better off without using Python as your project's main driver. Yes, it's simple to write it and the developers supply is abundant. It's easy to start. It'll just be a major pain to scale it and support it later on.

Edit: Made a pun.

I'd also like to point out that the majority of software engineers nowadays lacks the mathematical background, so it's probably worth including theoretical books like Abstract Algebra by Dummit and Foote on the 'must read' list.

No it's not, and you still have a burden of a proof on your shoulders. It probably is, indeed, kept up by some degree of anti-competitive practices but it's still not a monopoly but a member of what you call oligopoly, providing a lot of cheap stuff in every of its areas of competition.

I'd like to point out as well that sanctions (not necessarily well-deserved) against Amazon will just destroy some workplaces, mostly lower-qualified ones, which will cause quite a bit of a problem.