matheusmoreira on Coalton Playground: Type-Safe Lisp in the Browser

Comment on Coalton Playground: Type-Safe Lisp in the Browser parent

Can SBCL actually check at compile time that the arguments to fn-t are bytes? I wonder how that works with Lisp's extreme dynamism. Also wondering about the calling convention it uses.

reikonomushaOP1y

It can detect simple-ish instances, like calling

    (fn-t "hello" "world")

But a good rule-of-thumb is that these compile-time type errors are more of a courtesy, rather than a guarantee. As soon as you abstract over fn-t with another function, like so:

    (defun g (x y)
      (fn-t x y))

and proceed to use g in your code, all the static checking won't happen anymore, because as far as g is concerned, it can take any input argument types.

    CL-USER> (defun will-it-type-error? ()
               (g "x" "y"))
    ;; compilation WILL-IT-TYPE-ERROR? successful

No compile-time warning is issued. Contrast with Coalton:

    COALTON-USER> (coalton-toplevel
                    (declare fn-t (U8 -> U8 -> U8))
                    (define (fn-t x y)
                      (* x y))
                    
                    (define (g x y)
                      (fn-t x y))
                    
                    (define (will-it-type-error?)
                      (g "hello" "world")))

    error: Type mismatch
      --> <macroexpansion>:8:7
       |
     8 |      (G "hello" "world")))
       |         ^^^^^^^ Expected type 'U8' but got 'STRING'
       [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]

Comments