3 ms·

Exactly. Almost any error can be a type error with a sufficiently expressive type system, because a type system is just a way to mechanically prove things about

Exactly. Almost any error can be a type error with a sufficiently expressive type system, because a type system is just a way to mechanically prove things about your code. A more expressive type system lets you prove more useful things. Of course, you can easily do things in a dynamic language that are observably correct, but which are very difficult to prove correct without advanced logic (i.e., an expressive type system). And more advanced type systems typically lose some nice ergonomic properties of simpler type systems, such as clear error messages, type inference, principal types, or decidability. So I can definitely see how someone moving for example from Java to Python would find the latter very liberating at first. On the other hand, you can argue that people shouldn’t be writing code that’s so difficult to prove things about in the first place. :) To my mind, the benefit of static types is that they allow proving properties of your code, but the cost is that they may force you to do so; the benefit of dynamic types is that they don’t force you, but the cost is that they don’t allow it. On balance I think static types are therefore preferable, because you can always fall back to dynamic types (strings/hashes/variants/sums) in a static language, but you can’t “fall forward” to static types in a dynamic language.

kronos29296 9y ago
With things like typescript or mypy in python you fall the other way around with types in dynamic languages. You can do it if you really want (optional but recommended for large projects). So Python and typescript have a nice sweet spot between static and dynamic if you want.
junke 9y ago
> ...the cost is that they don’t allow it. Saying they don't allow it is too strong (they allow it, but it might be harder).
- evincarofautumn 9y ago
  You can’t prove even very simple universal properties of dynamically typed code, such as “when given an integer, this function always returns an integer”, because its result type can depend on the value of the integer passed in at runtime. You can only prove existential properties (“there are integers for which this function returns an integer”) through testing. That testing can be done before runtime in some languages, e.g., with Perl’s BEGIN/UNITCHECK/CHECK/INIT blocks. But it’s not really the same. In a referentially transparent, statically typed language, if you give me a function of type ∀a. a → a, then I know for a fact that if this function halts, it must be the identity function. The only thing it can do is return its input. The same function in a dynamically typed language could return any value of any type, because its result’s type can depend on both the type and the runtime value of its input, or not depend on its input at all, even if it’s referentially transparent. Even if you supply that type annotation and check it at runtime (“this function returns a value of the same type as its input”), it would only be checking a single code path, and it could still give me any value. That is, a valid implementation would be “return 3”—I wouldn’t get a type error if I only ever called it on integers, but it would still be non-parametric.
  - junke 9y ago
    "when given an integer, this function always returns an integer" (defun foo (x) (declare (integer x)) (round (/ x))) (describe #'foo) Derived type: (function (integer) (values integer rational &optional)) When given an integer, the function returns an integer, as well as an additional rational value. ROUND's specification says the type of the remainder is a REAL, but since I call it with integer, it is more precisely a RATIONAL (a subtype of REAL). (foo 0) => arithmetic error DIVISION-BY-ZERO signalled Note, the meaning of the derived type is: if the code returns a value, then its type is .... The same applies in OCaml, where you can raise exceptions. Let's restrict the input domain to non-zero integers: (defun foo (x) (declare (type (or (integer 1 *) (integer * -1)) x)) (round (/ x))) (describe #'foo) Derived type: (function ((or (integer 1) (integer * -1))) (values (integer -1 1) (rational -2 2) &optional)) The primary return value is an integer between -1 and 1; the remainder is a rational between -2 and 2 (ranges are inclusive).
    - evincarofautumn 9y ago
      Cool—Common Lisp? Isn’t that a promise to the compiler that you will obey the type, not a request to the compiler to enforce that you do? And can it correctly enforce something like the (∀a. a → a) that I described? I consider gradual typing (e.g. Typed Racket, Hack) an interesting case of static typing where you’re trying to provide good interop with your dynamically typed surroundings, typically while migrating from dynamic to static types. Not all dynamically typed systems that allow type annotations have “gradual typing” in that sense, because many of them don’t give you enough power to get to “fully annotated” code (where the compiler is finally free to erase types completely).
      - junke 9y ago
        Yes, SBCL, where declarations are treated as assertions (before you reach it, you must prove it or test it, after the declaration you can assume it). No, (∀a. a → a) is not easily expressible (unless you write your own DSL).
      - 9y ago

kronos29296 9y ago

With things like typescript or mypy in python you fall the other way around with types in dynamic languages. You can do it if you really want (optional but recommended for large projects). So Python and typescript have a nice sweet spot between static and dynamic if you want.

junke 9y ago

> ...the cost is that they don’t allow it. Saying they don't allow it is too strong (they allow it, but it might be harder).

evincarofautumn 9y ago
You can’t prove even very simple universal properties of dynamically typed code, such as “when given an integer, this function always returns an integer”, because its result type can depend on the value of the integer passed in at runtime. You can only prove existential properties (“there are integers for which this function returns an integer”) through testing. That testing can be done before runtime in some languages, e.g., with Perl’s BEGIN/UNITCHECK/CHECK/INIT blocks. But it’s not really the same. In a referentially transparent, statically typed language, if you give me a function of type ∀a. a → a, then I know for a fact that if this function halts, it must be the identity function. The only thing it can do is return its input. The same function in a dynamically typed language could return any value of any type, because its result’s type can depend on both the type and the runtime value of its input, or not depend on its input at all, even if it’s referentially transparent. Even if you supply that type annotation and check it at runtime (“this function returns a value of the same type as its input”), it would only be checking a single code path, and it could still give me any value. That is, a valid implementation would be “return 3”—I wouldn’t get a type error if I only ever called it on integers, but it would still be non-parametric.
- junke 9y ago
  "when given an integer, this function always returns an integer" (defun foo (x) (declare (integer x)) (round (/ x))) (describe #'foo) Derived type: (function (integer) (values integer rational &optional)) When given an integer, the function returns an integer, as well as an additional rational value. ROUND's specification says the type of the remainder is a REAL, but since I call it with integer, it is more precisely a RATIONAL (a subtype of REAL). (foo 0) => arithmetic error DIVISION-BY-ZERO signalled Note, the meaning of the derived type is: if the code returns a value, then its type is .... The same applies in OCaml, where you can raise exceptions. Let's restrict the input domain to non-zero integers: (defun foo (x) (declare (type (or (integer 1 *) (integer * -1)) x)) (round (/ x))) (describe #'foo) Derived type: (function ((or (integer 1) (integer * -1))) (values (integer -1 1) (rational -2 2) &optional)) The primary return value is an integer between -1 and 1; the remainder is a rational between -2 and 2 (ranges are inclusive).
  - evincarofautumn 9y ago
    Cool—Common Lisp? Isn’t that a promise to the compiler that you will obey the type, not a request to the compiler to enforce that you do? And can it correctly enforce something like the (∀a. a → a) that I described? I consider gradual typing (e.g. Typed Racket, Hack) an interesting case of static typing where you’re trying to provide good interop with your dynamically typed surroundings, typically while migrating from dynamic to static types. Not all dynamically typed systems that allow type annotations have “gradual typing” in that sense, because many of them don’t give you enough power to get to “fully annotated” code (where the compiler is finally free to erase types completely).
    - junke 9y ago
      Yes, SBCL, where declarations are treated as assertions (before you reach it, you must prove it or test it, after the declaration you can assume it). No, (∀a. a → a) is not easily expressible (unless you write your own DSL).
    - 9y ago