4 ms·

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

by junke 9y ago

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).
    - kazinator 9y ago
      That's right; those are promises to the compiler whose main use case is local "hotspot" optimizations. Those promises can be used as checking assertions in safe code; they become dangerous if code is optimized with safety 0. You'd work around not being able to express (∀a. a → a) by focusing on the specific use scenario in the optimized code where that function is being called, and the concrete types that are involved. The identity function fits this type. If we know that x is fixnum, we can do this: (the fixnum (identity x)). Using the, we an assert types of individual forms. Which is not to say that an implementation cannot do type inference for (identity x) and represent it type as (∀a. a → a) ; it's just that type inference is a separate thing from the ANSI CL declaration system.
  - flavio81 9y ago
    Every time i hear some person complain about dynamic typing as if it was a world filled with pitfalls and dangers, I think in Common Lisp and how great is its dynamic type system. Good example.
- flavio81 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” Really? Straight from my common lisp (SBCL) command line: CL-USER> (defun myfunction (x) (atanh x)) MYFUNCTION CL-USER> (describe #'myfunction) #<FUNCTION MYFUNCTION> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES (OR (SINGLE-FLOAT -1.0 1.0) (DOUBLE-FLOAT -1.0d0 1.0d0) (COMPLEX SINGLE-FLOAT) (COMPLEX DOUBLE-FLOAT)) &OPTIONAL)) Source form: (SB-INT:NAMED-LAMBDA MYFUNCTION (X) (BLOCK MYFUNCTION (ATANH X))) ; No value CL-USER> What happened here? I defined a function, i never declared which type does the function use, but the compiler can infer all the types. If i supply a string to "myfunction", the compiler will complain. Typing is strong, but it's dynamic. What will atanh return? CL-USER> (describe #'atanh) #<FUNCTION ATANH> [compiled function] Lambda-list: (NUMBER) Declared type: (FUNCTION (NUMBER) (VALUES (OR SINGLE-FLOAT DOUBLE-FLOAT (COMPLEX SINGLE-FLOAT) (COMPLEX DOUBLE-FLOAT)) &OPTIONAL)) Derived type: (FUNCTION (T) *) Documentation: Return the hyperbolic arc tangent of NUMBER. Known attributes: foldable, flushable, unsafely-flushable, movable, recursive Source file: SYS:SRC;CODE;IRRAT.LISP ; No value CL-USER> The wonders of CL... not only i get all the possible input types, but also the return types. And the documentation, and the source code file(!)

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

by 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).
  - kazinator 9y ago
    That's right; those are promises to the compiler whose main use case is local "hotspot" optimizations. Those promises can be used as checking assertions in safe code; they become dangerous if code is optimized with safety 0. You'd work around not being able to express (∀a. a → a) by focusing on the specific use scenario in the optimized code where that function is being called, and the concrete types that are involved. The identity function fits this type. If we know that x is fixnum, we can do this: (the fixnum (identity x)). Using the, we an assert types of individual forms. Which is not to say that an implementation cannot do type inference for (identity x) and represent it type as (∀a. a → a) ; it's just that type inference is a separate thing from the ANSI CL declaration system.
- flavio81 9y ago
  Every time i hear some person complain about dynamic typing as if it was a world filled with pitfalls and dangers, I think in Common Lisp and how great is its dynamic type system. Good example.
flavio81 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” Really? Straight from my common lisp (SBCL) command line: CL-USER> (defun myfunction (x) (atanh x)) MYFUNCTION CL-USER> (describe #'myfunction) #<FUNCTION MYFUNCTION> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES (OR (SINGLE-FLOAT -1.0 1.0) (DOUBLE-FLOAT -1.0d0 1.0d0) (COMPLEX SINGLE-FLOAT) (COMPLEX DOUBLE-FLOAT)) &OPTIONAL)) Source form: (SB-INT:NAMED-LAMBDA MYFUNCTION (X) (BLOCK MYFUNCTION (ATANH X))) ; No value CL-USER> What happened here? I defined a function, i never declared which type does the function use, but the compiler can infer all the types. If i supply a string to "myfunction", the compiler will complain. Typing is strong, but it's dynamic. What will atanh return? CL-USER> (describe #'atanh) #<FUNCTION ATANH> [compiled function] Lambda-list: (NUMBER) Declared type: (FUNCTION (NUMBER) (VALUES (OR SINGLE-FLOAT DOUBLE-FLOAT (COMPLEX SINGLE-FLOAT) (COMPLEX DOUBLE-FLOAT)) &OPTIONAL)) Derived type: (FUNCTION (T) *) Documentation: Return the hyperbolic arc tangent of NUMBER. Known attributes: foldable, flushable, unsafely-flushable, movable, recursive Source file: SYS:SRC;CODE;IRRAT.LISP ; No value CL-USER> The wonders of CL... not only i get all the possible input types, but also the return types. And the documentation, and the source code file(!)