Omg. My assessment was correct, after all.

> Hence, they're not objectively superior to anything else

Of course they are.

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.

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.

Again. Only Americans are conditioned to value and cherish their self esteem. That was my statement.

Other cultures do not put any emphasis on self esteem (and many consider it as something shameful to even talk about it).

No, I'm saying that only Americans are so conditioned to value their "self esteem". There is no emphasis on this stupidity in the other cultures.

It's all about the emphasis: http://faculty.washington.edu/jdb/articles/Cai%20et%20al.%20...

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.

> 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.

> 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 dynamic type system, no such constraints exist (besides for the constant literals, of course) and there are no rules for combining the constraints.

These definitions should cover all the spectrum.

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.

Is it so hard to follow?!?

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.

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.

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.

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.

Static typing bears important semantics far beyond a mere "validity checking" and compile time optimisations. And this fact is overlooked far too often.

Anecdotes are the best we have. Far better than a pseudoscience with agenda.