Is Python becoming more statically typed then?
I've tried to elaborate here why annotating variables with type doesn't make a dynamic language static:
https://medium.com/@Jernfrost/dynamically-typed-languages-ar...
You can't look at the presence of type information to determine if a language is static or dynamic. What matters is when and how that type information is used. In static languages expression have type. In dynamic languages values have type.
The implication is that you can't know the type of something in a dynamic language until the expression has been evaluated at run time. With a static language we can determine the type of every expression at compile time, which requires full knowledge of the whole program. It is why dependencies becomes much more problematic in static languages and why they are so poor as glue languages.
But you have to have this information anyway, or at least most of it. Even in a dynamically typed language, you have to know what sort of arguments a function expects; otherwise, how can you write any code at all to operate on those values if you don't even know what they are? Static typing just forces you to be more explicit about encoding those constraints. Whether that's worth the tradeoff depends on a lot of factors, but its use as a "glue" language is certainly not one of them.
Edit: Moreover, the line between statically typed and dynamically typed languages isn't as well-defined as you claim. For instance, TypeScript is a statically typed language, but it successfully compiles regular JavaScript code because, by default, every expression is given the type `any`. This means you can start out with dynamic typing and add static types progressively. And at that point, how is that any different than Python with mypy[0]?
True, but the Smalltalk idea was that you send a message to an object, and that object decides how (or whether) to handle it. So in Ruby, if you send the + method to some kind of number object along with the objects you want added, and the receiving object decides how to perform that addition, assuming the objects you sent can be summed.
Not necessarily...
If the value passed to function implements whatever functionality called then its type doesn't really matter. Really the whole theory behind duck typing.
>>> i = 1 + "1"
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for +: 'int' and 'str'
There is actually an entire category of static type systems called "structural type systems"[0], which is basically duck typing checked at compile-time rather than runtime.
> With a static language we can determine the type of every expression at compile time, which requires full knowledge of the whole program.
> Dynamic and static languages are fundamentally different. There is no more or less.
For many Python programs, every expression can be determined statically. While this may not be true for all expressions in all programs, surely this means the OP's claim that "Python is becoming more statically typed" is true and your claim that "There is no more or less" is false, no?
Besides, there are languages like Go which have dynamic types (interface{}) and which are considered statically typed languages. You might say that the static type is interface{}, but then you could say that every type in an un-annotated Python program is also interface{} (or whatever the equivalent Python type would be).
It seems like your arguments hinge on semantic games.
And C# has a var type (dynamic) and Dart has gradual typing.
C# Dynamic Type: C# 4.0 (.NET 4.5) introduced a new type that avoids compile time type checking. You have learned about the implicitly typed variable- var in the previous section where the compiler assigns a specific type based on the value of the expression. ... A dynamic type can be defined using the dynamic keyword.Jan 1, 2014
I don't think this is true. In a dynamic language all values, including expressions, share a single type - a union of all possible types. In a static language you can limit which possible types a value may hold. A dynamic language is like if you cast every single type to Any in a static language.
In Python this is entirely possible with mypy - a static type system for the Python language, which works through annotations.
> in static languages they are used to prevent the compilation of programs containing expressions where types don’t match up.
This is already the case with mypy in Python. It seems very much static. It's like everything is statically determined to be Any, then you specify in certain areas a more limited type.
In your case with Julia, the type annotations are static. Even if by default Julia is dynamic, it allows for static annotations.
I disagree that there is no in-between. I think Julia is actually a great example of an in-between. And, in fact, it has a name - gradual typing.
No, you're thinking of a weakly- versus strongly-typed language. Python is dynamically and strongly typed - values have a definite type, but a variable can be assigned a value of any type.
Using annotations you can then specify the type.
Nothing to do with weak/ strong, which merely imply some level of implicit casting.
https://stackoverflow.com/a/28096079/659248
The notion that dynamic languages are "unityped" comes from looking at them through the lens of static typing, leading to a disconnect about what "type" means and a correspondingly meaningless answer. Since the static notion of type applies to expressions and the dynamic notion of type applies to values, when you ask what the type of an expression in a dynamic language is, you get an useless answer since dynamic languages don't—by their very nature—assign types to expressions. Yes, you can sometimes figure out what the type of an expression must be, but the ability to do so is incidental and not guaranteed by the language, nor an inherent part of its semantics.
The dynamic notion of type belonging to a value distinct from an expressions is present to a limited extent in object-oriented static languages with subtyping: when the static type of an expression and its actual runtime type can be different. The static type corresponds to the static notion of what a type is while the runtime type corresponds to the dynamic notion of what a type is.
> Yes, you can sometimes figure out what the type of an expression must be, but the ability to do so is incidental and not guaranteed by the language, nor an inherent part of its semantics.
It's not guaranteed with most languages - they build up from primitives, and almost all of them have some sort of soundness holes.
If I have every primitive type in Python correspond to a type in mypy, I don't get how that isn't a basis of a static type system.
It seems like you're talking about the difference between evaluation and a value itself. But mypy types are evaluated...
> The notion that dynamic languages are "unityped" comes from looking at them through the lens of static typing, leading to a disconnect about what "type" means and a correspondingly meaningless answer.
Pretty sure it's just the simple, type-theory way of defining it, and I don't see why we would define types in a way that isn't consistent with type theory.
What's your definition of what makes a language static verus dynamic?
> If I have every primitive type in Python correspond to a type in mypy, I don't get how that isn't a basis of a static type system.
Being able to describe and annotate types doesn't make a static type system. A static type system is a way of associating with each valid program a proof that there will be no runtime type errors (or at least that certain entire classes of runtime errors will not occur). That's the entire premise of type theory.
The fact that you can assert types and determine the types of some expressions in mypy doesn't make it static (just like it doesn't make Julia static). You can prove that `2 + 2` is an integer in any language. Being able to do that does not make a language static or the term "static" is vacuous.
> Pretty sure it's just the simple, type-theory way of defining it, and I don't see why we would define types in a way that isn't consistent with type theory.
When a definition isn't useful, you don't just throw up your hands and say "oh well, guess we can't do anything about this"—you use a definition that is useful for the problem at hand. The fact that type theory's entire conclusion about dynamic languages is "they only have one type" is about as clear evidence as possible that, despite the name, "type theory" is not a useful tool for understanding types in dynamic languages. Yet systems like Julia and mypy are clear evidence that interesting things can be said about "types" even in systems that traditional type theory would call unityped.
Types are checked before program execution.
I think this definition is very, very standard, and in keeping with a type theory view.
> Being able to describe and annotate types doesn't make a static type system. A static type system is a way of associating with each valid program a proof that there will be no runtime type errors (or at least that certain entire classes of runtime errors will not occur).
These two statements seem to contradict each other. Adding the type annotations is exactly what allows mypy to associate a proof with code.
I don't think the definition is useless... it seems entirely consistent with gradual typing.
This is a common informal understanding of the distinction, but when types are checked is not a property of a language and does not agree with the type theoretic definition of what a type system is. For example, you can defer type checking of Haskell programs until runtime [1]. Does Haskell suddenly become a dynamic language just because you decided to check types later even though your code is the same and the program behaves the same? No. What makes Haskell static is the fact that it comes with a set of rules that assign a proof of type-correctness to every valid Haskell program. When or even if you choose to check whether those rules are followed is not the deciding factor.
Similarly, the same Python 3 program can be run with or without running mypy on it first. The Python language is the same either way and a correct program will behave exactly the same since running mypy has no effect on program execution. Does whether Python is a dynamic language or not depend on whether I happen to have run mypy on it first? In this view, the adjectives "dynamic" and "static" do not describe the language and its semantics, they describe how one happens to use it.
> > Being able to describe and annotate types doesn't make a static type system. A static type system is a way of associating with each valid program a proof that there will be no runtime type errors (or at least that certain entire classes of runtime errors will not occur).
> These two statements seem to contradict each other. Adding the type annotations is exactly what allows mypy to associate a proof with code.
Type annotations are neither necessary nor sufficient to be able to type check a program. Type annotations are almost entirely unnecessary in Hindley-Milner languages (ML, Haskell), yet these are very much static languages—these are the languages of type theorists. Conversely, the mypy developers describe mypy as a "type linter" [1] for a reason: mypy is not what type theorists would consider to be a "type checker" precisely because you cannot associate a proof of the lack of type errors with every valid Python program. You can give a proof of the correctness of some programs, but that’s true in any language, so if that’s the criterion for being “static” then every language is static, so the term is meaningless.
> I don't think the definition is useless... it seems entirely consistent with gradual typing.
This HN post about gradual typing is relevant and worth reading: https://news.ycombinator.com/item?id=8595116. Mypy has optional typing, not gradual typing because the Python type system is not complete, even with type annotations. Perhaps you disagree with this perspective and consider Python 3's types to be "real types" and believe that mypy is a "real type checker". In that case, you are in direct disagreement with type theorists because they consider Python to be a unityped language and would take umbrage at calling mypy a "type checker" insisting instead that it is merely a "type linter". This is exactly why I feel that the type theoretic perspective should be broadened to consider systems like mypy to be "real" type systems, albeit dynamic ones, and that they should be studied and formalized rather than dismissed with unhelpful terms like "unityped".
[1] https://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime
And given how mypy works, you can enforce types over only parts of a program.
That, to me, sounds like the python ecosystem is becoming more statically typed.
Because (1) you need to declare the fields, and (2) it's good to do that in a way that will work with typecheckers even though they are external, and (3) there are actually two particular type declarations that are used by the implementation, even aside from external typecheckers.
For example you could set the type to object, typing.Any, ... (Ellipsis), or None, etc.