soundness of combined Coalton/CL codebases

[tgbugs-build]

Is Coalton able to deal with soundness issues like those described by Felleisen around 44mins in https://youtu.be/XTl7Jn_kmio?t=2644? From the statement in the introduction Though note that Coalton will not type-check these function calls for you, since they’re being called as Lisp code. it seems that there is currently nothing like the Racket contract system that can protect against such issues.

[tgbugs]

Looks like this hn comment https://news.ycombinator.com/item?id=28486543 might be the answer. No contracts needed because they are built into CL?

However, if you're really scared, you can do

(declaim (optimize (speed 0) (safety 3)))

and really precise run-time type assertions will be inserted into the code.

[stylewarning]

I would say that contracts would still be welcome, because the Lisp types are not as expressive as the Coalton types, so a Lisp type-check would be more or less limited to some amount of basic data type checking. It's good for most use-cases, but still can let bugs slip through.

I think this general area—how Lisp and Coalton interact—needs more attention, documentation, and policy.

[eliaslfox]

Hey @tgbugs, I wanted to comment on the system as it currently works.

Coalton can't express types that are a subset of values the way that some contract systems can. This means that numerical ranges and other similar constraints need to be checked within Coalton just like in Common Lisp. It is possible to pass the wrong type to a Coalton function from Common Lisp but the types of errors such as passing a string when a list was expected are much more likely to crash than give an incorrect answer.

When Coalton is compiled, Common Lisp type declarations are added to generate more performant code. On high safety settings SBCL will add runtime checks to verify these type declarations.

The following code is the identity function specialized to strings.

(coalton-impl::process-coalton-toplevel '((define (f x) (the String x))))

The codegen for the above function is

  (COMMON-LISP:DEFUN F (X-700)
    (COMMON-LISP:DECLARE (COMMON-LISP:IGNORABLE X-700)
                         (COMMON-LISP:TYPE COMMON-LISP:SIMPLE-STRING X-700)
                         (COMMON-LISP:VALUES COMMON-LISP:SIMPLE-STRING
                                             COMMON-LISP:&OPTIONAL))
    X-700)

If I compile f and then call it with (f 5) I get the following error in SBCL.

The value
  5
is not of type
  SIMPLE-STRING
when binding X-701
   [Condition of type COMMON-LISP:TYPE-ERROR]

These runtime checks are sufficient for simple types. However Common Lisp's type system does not have parametric polymorphism
so checks on generic types degrade to only checking the generic type and not its arguments.

G as defined below only takes tuples of Integers, but it can be called from Common Lisp with tuples of any type because the dynamic checks only verify that t is an instance of Tuple at runtime.

(coalton-toplevel
               (declare g ((Tuple Integer Integer) -> Integer))
               (define (f t)
                 (match t
                   ((Tuple a _) a))))

If G was instead defined as

(coalton-toplevel
               (declare g ((Tuple Integer Integer) -> Integer))
               (define (g t)
                 (match t
                   ((Tuple a _) (+ 1 a)))))

Then the type of a would be checked upon calling the + function. However calling G with Tuple Integer String would still not fail at runtime.