Home

Types in CMUCL

CMU Common Lisp's compiler, known as Python, has a sophisticated implementation of Common Lisp's powerful type system. The system primarily enforces type safety at runtime, but it also performs static type inference. The static type information is used to detect type errors, eliminate unnecessary runtime type checks, and select efficient primitive code (e.g. avoid excessively generic arithmetic).

CMUCL's history stretches back around twenty years, though I believe the compiler was rewritten "just" 15 odd years ago. The system is still widely used, notably by ITA software as publicised by Paul Graham.

By Luke Gorrie at 2004-07-02 01:24 | Implementation | other blogs | 9618 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

How does it work?

OK, Luke, before I launch into my obligatory tirade :), perhaps you can explain what guarantees CL gives you w.r.t. typing. From your examples in the other thread, I gather that a CL implementation must complain if it can determine that every execution of a program fragment will raise a type error.

Now, having looked at the type specifier language, it is pretty clear to me that it is too expressive for this property is undecidable. However, I could find no mention (during my admittedly cursory perusal of the documentation) of any guarantees about when it can find a type error. In other words, looking at the type checker as a theorem prover, I could find no characterization of what theorems it can prove.

Does CL's type system actually provide any static guarantees? (Note that I am talking about Common Lisp, the specification, not CMU CL, or any particular implementation.)

By Frank Atanassow at Fri, 2004-07-02 13:28 | login or register to post comments

As you expect

Let's see if I can obviate the need for a tirade :-)

There are no static guarantees in CL, and your overall characterisation is quite correct. This is very different to ML-style typing. Runtime checks are still king, the partial static checking is mostly sugar.

What I find the most useful with CMUCL is being able to attach types to variables and structure members and to have those types checked each time somebody sets a value. This creates a lot of extra runtime type checking that will catch errors earlier, i.e. when an invariant is broken rather than later in some bad state.

I said "type", but a better word might be "contract" or "invariant", since Common Lisp's type system can express anything. For instance, suppose you have a predicate prime? and you want to declare a variable that can only be bound to prime numbers: 

(deftype prime () '(satisfies prime?)
  "A prime number.")
(defvar *my-prime*)
(declaim (type prime *my-prime*))
Now all bindings/assignments of *my-prime* will give a runtime error unless the value is prime. This is a flexible way to define invariants on variables and data structures without needing a lot of boilerplate like special setter functions.

Do any other dynamically typed languages have a similar feature? If not, I think they should consider it. There has been a little talk of adding something similar to Erlang by allowing "guard expressions" on record types.

P.S., I think the CMUCL manual is very worthwhile to read. It's a compiler that will put hair on your chest.

By Luke Gorrie at Fri, 2004-07-02 17:38 | login or register to post comments

Tcl's variable traces can do similar

You can do a similar thing with variable traces in Tcl:

set myprime 2
trace add variable myprime write [list checkprime]
proc checkprime {varname _ op} {
    upvar 1 $varname var
    if {![isprime $var]} { error "not a prime number" }
}

The problem with this is that the trace is called after the variable is set, so you might want to do something more fancy with storing away the old value in the write trace (to check next time). Tk uses something like this for entry widget validation, IIRC.

By Neil Madden at Fri, 2004-07-02 18:58 | login or register to post comments