4 ms·
"when given an integer, this function always returns an integer" (defun foo (x) (declare (integer x)) (round (/ x))) (describe #'foo) Der
by 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 agoCool—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 agoYes, 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 agoThat'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 agoEvery 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.
- deleted 9y ago[deleted]