3 ms·
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 e
by 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 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.