| HN Mirror

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

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

We are talking about the value of different kinds of type systems and using them. Being able to build a dynamic one on top of a static one says very little about whether or not dynamic or static typing is better for actual usage. On top of this lots of languages have added gradual typing, so this idea that you cannot take a language that is not statically typed and add a type system seems misguided.

> A very obvious consequence of this observation is that there will always be far more boilerplate with dynamic typing than with static.

I hope you realize that this is not at all what reality looks like.

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

> Exactly. And you're apparently suggesting that there may not be a single case where you may want static constraints.

No, I have consistently asked for objective proof that static typing is a net win over dynamic typing, something you have yet to even address. I don't know if you're intentionally misrepresenting my argument or if you're simply misunderstanding it, but I think you should re-read this whole thread.

As I've said previously, I prefer static strong typing, but I'm also in touch with reality and to present my opinion and speculation as some kind of fact isn't something I'm interested in.

> I can only conclude that you do not know much about the reality if you think so.

If we're jumping to conclusions I'd like to conclude that you think all PL theory is type theory and that you're ignorant of every other bit of it (and also that you're the type of person to think your every opinion is fact. I think both of these have been on display in this thread, so I actually think that's a stronger conclusion than the one you've drawn).

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.

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

Condescending, but not to be confused with correct. I'll try as well:

Given your obviously limited knowledge and familiarity with English I can understand that you seem to have issues understanding my basic argument, but I'll restate it for you:

If you are trying to claim something as superior, you need to provide actual reasons for it, not just speculation.

I hope you followed that.

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

It's actually not understandable that someone who claims to have a lot of knowledge in type systems and type theory, as well as logic, to provide "proof" that in no way proves what was asked for. It's also surprising that someone who claims to be so well versed in PLT essentially says it's all type theory.

It's understandable if a person with reading comprehension issues would have problems reading this post, so if you have any questions regarding it (or the previous posts), feel free to ask.

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.

Is it so hard to follow?!?

> With static typing you can do everything that is possible with a dynamic typing, at no additional cost [...]

This is not necessarily true: Static typing quite often requires you to satisfy the type system and quite often is an exercise in what essentially amounts to paperwork. There is a cost.

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

I haven't stated that dynamic typing is better, but I have stated that people claiming one or the other need to have proof. Dynamic typing is very rarely stated as better, whereas static typing is quite often cited as better subjectively, even if it's only opinion.

If your programs are as airtight as the "proof" you've given here, I'm not sure I ever want to use them.

Have your opinion and know that I share it (mostly), but also know that it's an opinion and that you'd do well in not confusing it with fact. Strong, static type systems are nice, but to say they're superior to dynamic type systems is an opinion and to present it as anything else is a lie.