Hacker News Reader

Comment by _ph_ | Hacker News Reader

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"

View on HN

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.

SBCL will issue a compile warning, that it cannot guarantee that you call the functions only with FIXNUMS.

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?

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

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.

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.

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?

No, I am not. Perhaps you read up a bit about Common Lisp and SBCL before we continue the discussion.

  (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?

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.

Reply on news.ycombinator.com