4 ms·

> what Common Lisp offers, especially SBCL: optional static typing Common Lisp offers optionally unsound static typing. (SBCL doesn't change that, that's why

> what Common Lisp offers, especially SBCL: optional static typing Common Lisp offers optionally unsound static typing. (SBCL doesn't change that, that's why it inserts runtime checks.)

_ph_ 8y ago
I am not sure what you mean by "unsound static typing", care to explain? SBCL does offer optional static typing as it goes beyond Common Lisp and can perform static type checking across compilation units. If you have a lisp file like: (defun foo (x) (declare (fixnum x)) (* x 2)) (defun bar () (foo 3.5)) Where bar has a static type error by calling foo with a float value, compiling the file with SBCL will give you the expected static type warning: ; file: foo.lisp ; in: DEFUN BAR ; (FOO 3.5) ; ; note: deleting unreachable code ; ; caught WARNING: ; Asserted type FIXNUM conflicts with derived type ; (VALUES (SINGLE-FLOAT 3.5 3.5) &OPTIONAL). ; See also: ; The SBCL Manual, Node "Handling of Types"
- YouAreGreat 8y ago
  A sound type system would have guaranteed that no program execution ever calls your function foo with the wrong type of argument. SBCL doesn't offer any such guarantee. If some part of your program extracts values from a heterogeneous list and calls foo on one of them, SBCL will not be able to statically guarantee that it is a FIXNUM at runtime. It can't reject the program either, that would require seriously subsetting the language.
  - _ph_ 8y ago
    SBCL will issue a compile warning, that it cannot guarantee that you call the functions only with FIXNUMS.
    - deleted 8y ago
      [deleted]
    - YouAreGreat 8y ago
      Whoa. Will SBCL emit false-positive warnings all the time when you dare to use lists in a Lisp, or does it at least try hard to infer specialized list types, going above what's expressible using the standard LIST type?
      - _ph_ 8y ago
        No it doesn't emit false positive warnings when using lists. That is FUD. But if a function explicitly requires fixnums, and you pass something of type t, it might warn (depending on the optimize settings).
        YouAreGreat 8y ago
        You didn't answer the question if SBCL infers specialized list types. I'll assume the answer is "no". In that case, everything extracted from a list is T and you'd have to get that warning you mentioned above. Such warnings would very likely be false-positive, unless Common Lisp programs are buggy as hell most of the time—assuming that would be the real FUD, no? Therefore, the non-FUD conclusion is to expect a high rate of false-positive warnings in typical list-using programs. TBH, I suspect those false-positive warnings you mentioned aren't bona fide warnings, but some kind optimizer stream-of-consciousness log stream.
        _ph_ 8y ago
        List elements are of type t, and of course acceptable to pass to all functions which take t as an argument, so no false-positive warnings.
        YouAreGreat 8y ago
        Are you saying that the happy path of SBCL static typing—given you also want to use lists, and also not be inundated with spurious warnings—is to declare everything to be of type T?
        8y ago
- ernst_klim 8y ago
  (defun sum (lst) (let ((acc 0)) (dolist (x lst) (setq acc (+ x acc))) acc)) (sum '("a" "b" "c")) gives me a runtime error. Does sbcl support parametric polymorphism?
  - YouAreGreat 8y ago
    The problem as I see it is the type for lst. Common Lisp has a (CONS α β) type for cons cells with member types α and β, but its LIST type is defined as (OR (CONS T T) NULL), basically more of a binary tree type, where T is the Common Lisp "any" union of all types. A useable (LIST α) type would be something like μβ.(OR (CONS α β) NULL), but that's not expressible within standard Common Lisp. I expect it to very hard to infer too, especially with CONS cells being mutable.

> what Common Lisp offers, especially SBCL: optional static typing Common Lisp offers optionally unsound static typing. (SBCL doesn't change that, that's why it inserts runtime checks.)

_ph_ 8y ago

I am not sure what you mean by "unsound static typing", care to explain? SBCL does offer optional static typing as it goes beyond Common Lisp and can perform static type checking across compilation units. If you have a lisp file like: (defun foo (x) (declare (fixnum x)) (* x 2)) (defun bar () (foo 3.5)) Where bar has a static type error by calling foo with a float value, compiling the file with SBCL will give you the expected static type warning: ; file: foo.lisp ; in: DEFUN BAR ; (FOO 3.5) ; ; note: deleting unreachable code ; ; caught WARNING: ; Asserted type FIXNUM conflicts with derived type ; (VALUES (SINGLE-FLOAT 3.5 3.5) &OPTIONAL). ; See also: ; The SBCL Manual, Node "Handling of Types"

YouAreGreat 8y ago
A sound type system would have guaranteed that no program execution ever calls your function foo with the wrong type of argument. SBCL doesn't offer any such guarantee. If some part of your program extracts values from a heterogeneous list and calls foo on one of them, SBCL will not be able to statically guarantee that it is a FIXNUM at runtime. It can't reject the program either, that would require seriously subsetting the language.
- _ph_ 8y ago
  SBCL will issue a compile warning, that it cannot guarantee that you call the functions only with FIXNUMS.
  - deleted 8y ago
    [deleted]
  - YouAreGreat 8y ago
    Whoa. Will SBCL emit false-positive warnings all the time when you dare to use lists in a Lisp, or does it at least try hard to infer specialized list types, going above what's expressible using the standard LIST type?
    - _ph_ 8y ago
      No it doesn't emit false positive warnings when using lists. That is FUD. But if a function explicitly requires fixnums, and you pass something of type t, it might warn (depending on the optimize settings).
      - YouAreGreat 8y ago
        You didn't answer the question if SBCL infers specialized list types. I'll assume the answer is "no". In that case, everything extracted from a list is T and you'd have to get that warning you mentioned above. Such warnings would very likely be false-positive, unless Common Lisp programs are buggy as hell most of the time—assuming that would be the real FUD, no? Therefore, the non-FUD conclusion is to expect a high rate of false-positive warnings in typical list-using programs. TBH, I suspect those false-positive warnings you mentioned aren't bona fide warnings, but some kind optimizer stream-of-consciousness log stream.
        _ph_ 8y ago
        List elements are of type t, and of course acceptable to pass to all functions which take t as an argument, so no false-positive warnings.
        YouAreGreat 8y ago
        Are you saying that the happy path of SBCL static typing—given you also want to use lists, and also not be inundated with spurious warnings—is to declare everything to be of type T?
        8y ago
ernst_klim 8y ago
(defun sum (lst) (let ((acc 0)) (dolist (x lst) (setq acc (+ x acc))) acc)) (sum '("a" "b" "c")) gives me a runtime error. Does sbcl support parametric polymorphism?
- YouAreGreat 8y ago
  The problem as I see it is the type for lst. Common Lisp has a (CONS α β) type for cons cells with member types α and β, but its LIST type is defined as (OR (CONS T T) NULL), basically more of a binary tree type, where T is the Common Lisp "any" union of all types. A useable (LIST α) type would be something like μβ.(OR (CONS α β) NULL), but that's not expressible within standard Common Lisp. I expect it to very hard to infer too, especially with CONS cells being mutable.