> Click on the time (for example "2 minutes ago") to open the post and reply there.
Shit. Is it a new feature? I do not remember this working before.
> And my point is that you haven't answered why using a static type system over a dynamic one is a net win for people
I am not interested in diverting the discussion from the topic. The topic was that static typing is superior to dynamic typing - i.e., more powerful and more flexible.
How does it translate to a "net win"? I do not care, honestly. There are fare to many factors other than the language features.
> Please stop editing your posts 40 minutes after you initially post them in order to muddle the post history.
HN does not allow to continue a thread below a certain threshold.
> I think strong static type systems are useful in many ways and I've already told you repeatedly that I prefer them.
This is not what I was talking about. Learn to read.
My point is that you do not understand what does it mean that a bigger type system is providing new semantics for the language. You still fail to understand it, obviously, because this is a central point of my proof, which you failed to comprehend.
> No one, in their next project, is going to build a dynamic type system in their static one, and then jerk off over that fact, when they could just start working on their ACTUAL project.
Take a look at pretty much any code in static languages - it is almost always doing exactly this: various degrees of dynamic typing on top of static. Sometimes it is ugly, sometimes it is done the right way (LLVM is a good example of this approach).
> Would you recommend to someone choosing between static and dynamic typing to start with a static one and then build their dynamic one on top of that?
Even you somehow heard something about the gradual typing - which is exactly an example of this.
> Your posts are full of bullshit, stupid assumptions and personal attacks.
Omg. I'm only responding to your attacks. You're an uninformed and incompetent side in this argument, not me.
> What culture doesn't acknowledge self respect, and one's place in society relative to others?
What culture (besides the Northern Americans) would so blindly equate self respect to self esteem? The others understand better that you can respect yourself even without the overblown, unrealistic views on your own abilities and virtues.
It is very childish and stupid to respond to a proof with a shit like "no, this is not a proof".
> The idea that static type systems are better to use (in general) because you can make dynamic type systems on top of them is simply not something you can just say and then have taken as fact.
Oh, did not realise you're so incompetent (although I should have guessed after your epic fail with the gradual typing). Do I have to prove that 2+2=4 too?
Once again: dynamic typing is a subset of static typing and therefore it is less powerful. Period. You cannot do anything with this fact.
Also, funny that you did not respond to my accusation that you believe that type systems are only for "validity checking". Which suggests that I was right.
Sorry, cannot reply down the thread, so I'll put my answer here:
> This is not necessarily true: Static typing quite often requires you to satisfy the type system
We're talking about static typing in general, not some particular implementation of it.
Any static type system with an "anything" type (think of the System.Object in .NET, for example) allows a transparent fallback to dynamic at any time.
So, claiming that "there is a cost" is an outright lie.
> I haven't stated that dynamic typing is better, but I have stated that people claiming one or the other need to have proof.
You know, there is a little funny thingy called "logic". And one of the most common tricks in logic is a proof by contradiction. When you're asking for a proof that static typing is superior, the simplest way is to start with "let's assume dynamic typing is superior". This is exactly what I did. Unfortunately, you could not follow.
> If your programs are as airtight as the "proof" you've given here, I'm not sure I ever want to use them.
It's understandable that a person who do not know much about type systems in particular and PL theory in general also apparently does not know much about proofs and logic in general. After all, type theory and proof theory are indistinguishable.
In a static type system, all of the expressions and expression-like constructs of your language may have a constraint attached to them, which guarantees that a value this expression yields have certain properties; In a static type system there is a well defined set of rules, describing how such constraints are transformed when expressions are combined in a certain way.
In a dynamic type system, no such constraints exist (besides for the constant literals, of course) and there are no rules for combining the constraints.
I provided you with a proof. Cannot you follow such a trivial logic?
Let me repeat it again, slowly:
1) Dynamic typing is a subset of static typing. With static typing you can do everything that is possible with a dynamic typing, at no additional cost, while the opposite is not true.
2) Static typing is far more than a mere "validity checking", as you apparently seem to believe. These advanced semantic properties cannot be added on top of a dynamic type system, so, even suggesting that a dynamic type system may be somehow superior is automatically declaring that under no circumstances you will ever need any of these properties.
> We are talking about the value of different kinds of type systems and using them.
Exactly. And you're apparently suggesting that there may not be a single case where you may want static constraints. Kinda very strong position, needs very strong proofs indeed.
> gradual typing
Gradual typing IS a static typing, period.
> you cannot take a language that is not statically typed and add a type system seems misguided.
What?!?
You cannot build a gradual typing system on top of a dynamic one.
> this is not at all what reality looks like.
I can only conclude that you do not know much about the reality if you think so.
> No, cutting away from something can make it better
What?!?
You can build a dynamic type system on top of a static one. The opposite is impossible. What else is there to even talk about?
> "More diverse things" is ill defined.
It is very well defined. Static (i.e., compile time) metadata allows to infer constraints in compile time. Dynamic metadata is useless for deriving constraints. A very obvious consequence of this observation is that there will always be far more boilerplate with dynamic typing than with static.
> Please, do present the solid theory that is not simply derived from speculation and opinion.
What theory shows is enough to claim superiority:
1) Dynamic typing is a subset of a static typing. This thing alone is enough.
2) Static typing provides more semantic options in both compile and run time, meaning that you can do more diverse things. Also quite a strong claim for superiority.
Anecdotes are case studies. In social sciences, for example, it's often the only thing you have. Do not dismiss this kind of evidence when you do not have any other options.
Empirical evidence is nearly impossible in this area.
On the other hand, we have a solid theory, not some "beliefs". If you want to dismiss the entire PL theory, you have to try really hard to justify such a stupid move first. The problem is, most of the dynamic proponents know next to nothing about the PL theory anyway.