Okay but they are formal systems and don't have anything to do with AI either, do they?
13 karma · joined July 18, 2019
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.
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!
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.
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?
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.
>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? ;)
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 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.
Excuse me but tuples. You still have to observe them to evaluate them but that's all you need to simulate n-arity in the way you want.
>more dynamic
Well, Hindley—Milner is how you do type-safe stuff with inference that annotates for you. For any generic purposes you just put a typevar with constraints, so I don't see a problem here and can't really get what you gain. MLs are more about proper composition.
Why keep reinventing the wheel when there's an ML language family already? Why do people keep giving up these juicy Hindley—Milner-ish type systems and these brief and concise equations for anything? It just doesn't make sense for me.
I guess that the complexity people are concerned about is that once you implement a parametric polymorphism, HKTs are inevitable and that probably requires some brain flexing in order to get the meaning of a structure, which defeats the main purpose that is being explicit and simple. Pretty much a deadlock. I now understand why the community is so in odds with the parametric polymorphism as the concept but I'm also sure that simplicity of use and convenience of writing a robust solution is the two things that require it. You can't keep your head near the sand and avoid HKTs when you want flexibility and you can't allow that type of polymorphism whilst striving for what's Go trying to do.
While understanding the both standpoints, though, I still hope that Go will get parametric polymorphism as it's just so much more pleasant and convenient than carrying around a mess of structures to be explicit no matter the costs.
The second assumption made here is that the (as pointed out) fuzzing is a thing.
The third one is that you can't be sure of the input device. Joystick like the one seen on ThinkPad is uncommon but still used as the input device. Touchscreens are common but human-ish, though you will have to cover them too. The extreme case is that some X-savvy person may just move the pointer sometimes using the X's built-in capabilities, by dmenu and stuff, and even if that's highly unlikely, it still will fail.
There's no point in doing all the possible checks you may come up with: egde cases, no matter how impossible they look, still exist and break the consistency of the slider solution easily. Google captcha and Funcaptcha are nearly the best options you can readily get, freeing your hands and head of a huge deal of hassle you will face when dealing with this task.
As of your described way of desugaring the contract, looks way too cluttered. It's exactly the reason why Reader and ReaderT exist in Haskell. Even though the proposal's contract syntax doesn't look very beautiful, it's still drastically better than keeping track of drilled structs of functions, the latter will become a mess really really fast, so having a way to conveniently constraint the accepted types while having a full-blown parametric polymorphism is essential for a modern language. Not sure exactly why anyone would be against that.