3 ms·

The type of FOO in SBCL is: (FUNCTION (T) (VALUES (OR (INTEGER 42 42) (SIMPLE-ARRAY CHARACTER (9))) &OPTIONAL)) SBCL is b

• groovy2shoes 10y ago
  > The type of FOO in SBCL is: Is that the type of FOO or the return type of FOO? How are the types or number of arguments specified for function types? > SBCL is based on Kaplan & Ullman flow-graph analysis (inherited from CMUCL), not Hindley-Milner. See also http://home.pipeline.com/~hbaker1/TInference.html http://home.pipeline.com/~hbaker1/TInference.html (Nimble Type Inference, H. Baker). Apparently, Typed Racket's papers have other references about related work, albeit not explicitly those. I've read some of Henry Baker's other work, and the man is brilliant. I wish he were more well-known. This is no exception, however it seems that this inferencer is useful primarily for enabling compiler optimizations rather than for performing type checking. Is that correct? What I mean is, say you want to pass the result from FOO above into another function BAR which expects a numeric argument. It seems to me that BAR would need to have an argument of type (OR (INTEGER 42 42) (SIMPLE-ARRAY CHARACTER (9))) in order to guarantee type safety. Otherwise, the type checker couldn't reject a program that passes a string result of FOO as a numeric argument of BAR. Am I understanding this correctly? > In OCaml, a function which throws an exception has not a different type than one which doesn't. So you can get runtime errors even when you typecheck. Right, but I'm talking specifically about run-time type errors, i.e., errors that occur because some value was passed to an operation that does not handle values of such type. What I meant by my statement is that even with type checking, the programmer must handle all cases of a sum type when dealing with it in order for the program to be type safe (in the sense that not only does it not "go wrong" in the Milner sense, but also that it does not suffer a type error at run-time).
  • junke 10y ago
    > Is that the type of FOO or the return type of FOO? It is the type of FOO, it reads as: a function which takes one argument of any type (T) and returns exactly one value, which is either 42 or a string of length 9. Another example: (defun xyz (x y z) (declare (type fixnum x) (type float y) (type (vector (unsigned-byte 8) 1024) z)) (aref z (+ x (round y)))) (FUNCTION (FIXNUM FLOAT (VECTOR (UNSIGNED-BYTE 8) 1024)) (VALUES (UNSIGNED-BYTE 8) &OPTIONAL)) Here there are three arguments, the third one being a vector of bytes of length 1024. Note that the return values was inferred from the inputs. > This is no exception, however it seems that this inferencer is useful primarily for enabling compiler optimizations rather than for performing type checking. Is that correct? It is a mix of both, really. CL is primarily designed to be dynamic. Static analyses are used to optimize code and prevent classes of errors if they can be detected in advance. If you define detecting a type error as a positive test, then SBCL allows to have false negatives. That happens in cases where the expected and actual types overlap: there might be an error, or not, so the actual check is delegated at runtime. Another thing is that with global functions (defun), it seems that there is some widening happening, for the return type in particular, so that (OR INTEGER STRING) is treated as T. This does not happen with inline or local functions. Note also that global functions can be called from anywhere, be redefined (except standard ones) and they are generally responsible for checking their arguments, except when you explicitely turn the safety knob down and add type declarations. So let's say that XYZ above is declared to be inlined, and we use it as follows: (defun use-xyz-1 (x y z) (declare (type positive-float y) (type (integer 0 3000) x)) (xyz x y z)) The above is compiled without problems, even though you could give values which would make an out-of-bounds access. However, you will surely agree that there are theoretical limits to static type checking, so it is expected that not all expressions can be typed in CL as precisely as you could wish (of course, going up the lattice, functions accept type T arguments). However, when you change type declarations so that the intersection of expected/actual types is empty: (defun use-xyz-2 (x y z) (declare (type positive-float y) (type (integer 2000 3000) x)) (xyz x y z)) ... the compiler warns you that: ;; Derived type (INTEGER 2000 4611686018427387900) is not a suitable ;; index for (VECTOR (UNSIGNED-BYTE 8) 1024) The way SBCL treats declaration is that they are used as assertions (except for return types in global declarations, see manual). So what does it mean to treat declaration as assertions? Here is FOO: (defun foo (float) (make-string (abs (ceiling float)) :initial-element #\#)) It makes a new string made of N times character "#", where N is computed from the float input. Then, we call FOO from BAR: (defun bar (x) (foo x) (typecase x (float 0) (integer 1) (t 2))) The unique value returned by BAR is of type `(integer 0 0)`, because knowing that `(foo x)` succeeds allows us to conclude that X was indeed a FLOAT, and thus the TYPECASE expression necessarily returns zero. Declarations, assertions, etc. can be used by the compiler. Note that the equivalent (w.r.t. return value) function below has a different type: (defun bar (x) (prog1 (typecase x (float 0) (integer 1) (t 2)) (foo x))) This time, the return type is (MOD 3), i.e. the set {0,1,2}, even though propagation could be applied backward. However, backward propagation seems to pose problem w.r.t. the CL standard, at least that's what is said here (a good reference, by the way): https://www.pvk.ca/Blog/2013/04/13/starting-to-hack-on-sbcl/ https://www.pvk.ca/Blog/2013/04/13/starting-to-hack-on-sbcl/ Static typing in SBCL gives something I did not yet witness in other languages. I defined a state machine with local functions, roughly as follows: (defun sm () (let ((state)) (labels ((a () (setf state #'b)) (b () (setf state #'c)) (c () (if (plusp (random 2)) (setf state #'d) (setf state #'b))) (d () (setf state #'a)) (e () (return-from sm))) (loop (funcall state))))) So the local variable "state" holds current function. And so, this compiles (and the actual, longer code did so as well) with a note saying "deleting unused function (LABELS E :IN SM)", because "state" is known to never reach E. By the way, function SM never returns normally, as explained by the NIL return type. That was a useful and unexpected thing to notice.