3 ms·

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 typ

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.
  - deleted 9y ago
    [deleted]
  - StefanKarpinski 9y ago
    > Types are checked before program execution. I think this definition is very, very standard, and in keeping with the type theory view. 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 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 https://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime [2] http://mypy.readthedocs.io/en/latest/basics.html http://mypy.readthedocs.io/en/latest/basics.html

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.
- deleted 9y ago
  [deleted]
- StefanKarpinski 9y ago
  > Types are checked before program execution. I think this definition is very, very standard, and in keeping with the type theory view. 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 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 https://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime [2] http://mypy.readthedocs.io/en/latest/basics.html http://mypy.readthedocs.io/en/latest/basics.html