3 ms·

Julia is always dynamically typed and type annotations do not make it static, in contrast to how some "traditional" gradually typed research languages have work

Julia is always dynamically typed and type annotations do not make it static, in contrast to how some "traditional" gradually typed research languages have worked. You can find a more detailed explanation here: https://stackoverflow.com/a/28096079/659248 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.

staticassertion 9y ago
I don't get where this whole "expressions vs values" thing is coming from. Why are you making this distinction? I don't get it. The expression '2 + 2' has a type in mypy - so why are we drawing this distinction here of all places? > 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.
- StefanKarpinski 9y ago
  > I don't get where this whole "expressions vs values" thing is coming from. Why are you making this distinction? I don't get it. 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.
  - staticassertion 9y ago
    > What's your definition of what makes a language static verus dynamic? 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.

staticassertion 9y ago

I don't get where this whole "expressions vs values" thing is coming from. Why are you making this distinction? I don't get it. The expression '2 + 2' has a type in mypy - so why are we drawing this distinction here of all places? > 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.

StefanKarpinski 9y ago
> I don't get where this whole "expressions vs values" thing is coming from. Why are you making this distinction? I don't get it. 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.
- staticassertion 9y ago
  > What's your definition of what makes a language static verus dynamic? 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.