Does Common Lisp need a better type system?

I have been reading the TAPL books by Pierce lately. I was really suprised how far they can get with type systems starting from the untyped lambda calculus. There are quite a few examples for various things, such as polymorphism, recursive types, subtyping, handling references and mutable state, forgetting garbage collection by region based memory management, etc...

I started this topic to talk about the type system of Common Lisp, its current state, and its future.

Let me start with a few questions:

- what does Common Lisp's type system misses from the developments available in other programming languages such as ML or Haskell?
- what is more important in writing more reliable programs, using more and better abstractions, or having more complicated types and better type checkers?

levy

-- there's no perfectoin

He knows better than I:
http://steve-yegge.blogspot.com/2008/05 ... -back.html

I'm a little bit of a type theory nerd, but I have a bit of a two tiered answer:
Does Common Lisp need a better type system? No, I really don't think it does. I don't think you could really add any kind of static typing without essentially redesigning the whole language a la Qi.
Do languages in general need better type systems? Oh hell yes. Check out the work on Agda or anything touched by Conor McBride. There are really cool things out there in the intersection betweeen math & cs and if I were writing software where high assurance was a primary goal, I would be tapping into that.

wchogg wrote:I'm a little bit of a type theory nerd, but I have a bit of a two tiered answer:
Does Common Lisp need a better type system? No, I really don't think it does. I don't think you could really add any kind of static typing without essentially redesigning the whole language a la Qi.
Do languages in general need better type systems? Oh hell yes. Check out the work on Agda or anything touched by Conor McBride. There are really cool things out there in the intersection betweeen math & cs and if I were writing software where high assurance was a primary goal, I would be tapping into that.

So help me out here. I'll admit to being an engineer by training, not a mathematician or theorist. And I'm probably not even a very good engineer. I have been programming since I was 12, though, which means 29 years. I have used a variety of languages during that time.

Whenever I read anything about type systems on Lambda the Ultimate or other more theoretically-oriented sites, my eyes just glaze over and and I start drooling. I try to read some of these papers every now and then and I have decided that either type theory is something I'll never understand, or it's basically gibberish written by those seeking tenure that are forced to publish something and would rather have it be incomprehensible, lest somebody discover that they weren't really working on anything anyway.

So, wchogg, you seem pretty pragmatic. Help me out and tell me why I, a practical engineer of sub-average intellect, should care about better type systems. What will they do for me?

wchogg wrote:I'm a little bit of a type theory nerd, but I have a bit of a two tiered answer:
Does Common Lisp need a better type system? No, I really don't think it does. I don't think you could really add any kind of static typing without essentially redesigning the whole language a la Qi.

I think that it is perfectly valid, if a type system is not able to deal with all parts of a program. I'm not a big fan of the idea that you have to fit everything into "one something"... I actually would like to have several type systems at hand, and use them (even mix them) when they are appropriate for the problem. Certainly, I would have to provide annotations (or rely on runtime checks), so that they can work together, but that seems to be ok to me.

Qi is really interesting and might be one of them. AFAICT it builds on top of CL, so it does not redesign the language, but I don't know how much you can mix Qi and CL code.

In Haskell, for example, you can tell for every function whether it is purely functional or not, just by looking at its type that was inferred by the compiler.

In CL, in contrast, you can't define a type which specifies a list of integers. Well, actually you can do it using 'satisfies', but that is completly opaque for the compiler and will never be inferred for you. Another example: you can't really specifiy a string* type, which has an argument for the upper limit of the string's length.

The current CL implementations do some type inference, and check code based on that, but the result is not available in a standard way. And even if you query the result in an implementation specific way, you will get very little. Also, there is no standard way for type reflection, so you can't expand type aliases.

Even though I'm not expert, I think there are many ways to improve the current CL type system.

levy

-- there's no perfectoin

I hope my initial terse reply didn't sound dismissive. It was mostly due to time constraints.

levy wrote:
I think that it is perfectly valid, if a type system is not able to deal with all parts of a program. I'm not a big fan of the idea that you have to fit everything into "one something"... I actually would like to have several type systems at hand, and use them (even mix them) when they are appropriate for the problem. Certainly, I would have to provide annotations (or rely on runtime checks), so that they can work together, but that seems to be ok to me.

I guess I'm showing some bias here in that I wasn't really thinking of pluggable type systems in the vein of Gilad Bracha's old paper. I have a gut feeling though that when it comes to CL, a language that practically revels in type puns (it's as if Haskell had made Nothing, [], & False all the same thing), you'd be facing a really hard time implementing them.

levy wrote: Qi is really interesting and might be one of them. AFAICT it builds on top of CL, so it does not redesign the language, but I don't know how much you can mix Qi and CL code.

In Haskell, for example, you can tell for every function whether it is purely functional or not, just by looking at its type that was inferred by the compiler.

In CL, in contrast, you can't define a type which specifies a list of integers. Well, actually you can do it using 'satisfies', but that is completly opaque for the compiler and will never be inferred for you. Another example: you can't really specifiy a string* type, which has an argument for the upper limit of the string's length.

The current CL implementations do some type inference, and check code based on that, but the result is not available in a standard way. And even if you query the result in an implementation specific way, you will get very little. Also, there is no standard way for type reflection, so you can't expand type aliases.

So if I remember correctly, in Qi you can drop down to CL but you are no longer under the protection of the type checker. For all intents & purposes, the part of Qi that is statically typed is a completely separate language with a convenient FFI down to Lisp.

Also, I'm not arguing against the usefulness of static typing in the slightest or that the CL way of doing things is the greatest; however, in practice I've been finding that generic functions have provided most of the type granularity I've needed. The caveat is that most of my CL code has been small experiments with games, not 100k LOC business apps.

The choice is a good type system or unit testing + constant asserts to confirm assumptions about the data passed in. I'll take the asserts any day, since that doesn't require me to think ahead about relationships between types.

findinglisp wrote:

wchogg wrote:I'm a little bit of a type theory nerd, but I have a bit of a two tiered answer:
Does Common Lisp need a better type system? No, I really don't think it does. I don't think you could really add any kind of static typing without essentially redesigning the whole language a la Qi.
Do languages in general need better type systems? Oh hell yes. Check out the work on Agda or anything touched by Conor McBride. There are really cool things out there in the intersection betweeen math & cs and if I were writing software where high assurance was a primary goal, I would be tapping into that.

So help me out here. I'll admit to being an engineer by training, not a mathematician or theorist. And I'm probably not even a very good engineer. I have been programming since I was 12, though, which means 29 years. I have used a variety of languages during that time.

Whenever I read anything about type systems on Lambda the Ultimate or other more theoretically-oriented sites, my eyes just glaze over and and I start drooling. I try to read some of these papers every now and then and I have decided that either type theory is something I'll never understand, or it's basically gibberish written by those seeking tenure that are forced to publish something and would rather have it be incomprehensible, lest somebody discover that they weren't really working on anything anyway.

So, wchogg, you seem pretty pragmatic. Help me out and tell me why I, a practical engineer of sub-average intellect, should care about better type systems. What will they do for me?

Aww crap...I hate it when people call me on my bold assertions.
Okay, so I'm probably not the best person to try & argue this point but I'll give it a shot. For me there are three reasons static type systems are cool.

• Proving properties about your code.
• Giving the compiler as much information as possible about your code.
• A source of new abstractions.

Now, what do I mean by these things?

In terms of proving properties, once you get to the level of dependent type systems you can start doing things like statically track semaphore operations in the type signature of your functions, check whether an array index is valid, or validate capability-like security all at the type level. The idea is that you can move entire classes of possible misbehaviors from only being detectable at runtime to being detectable at compile time. To me, that's very cool. Even at the level of something like Haskell, the separation between effectful code & pure code allows for libraries like STM to provide the semantics they can.

I'd recommend looking at GHC & the work by Don Stewart & Manuel Chakravarty for examples of type level information being able to inform compiler optimizations. The automatic parallelization in GHC looks pretty slick.

In terms of abstractions, this is probably something that is mostly interesting to me, but I like it when investigations into the math behind type theory allow you to pull out honest-to-God useful abstractions such as applicative functors, zippers, or monads. You get a rather different kind of abstraction from this than you do from object-oriented approaches. I'd describe it as being much more focused on structure & algebraic laws than on data or punning-functions.

Now, does that mean that static type systems are The Holy Path? Well, not really. These are all tools & a lot of it is personal preference. I think there's a whole different class of abstractions you get from things like CL macros & symbols. For example, I love the syntactic abstractions you get from slick CL libraries like Postmodern or lispbuilder-sdl.

So, that's my general feeling. I have been writing software a lot less long than you have, though, so feel free to take it with a few grains of salt.

wchogg wrote: Aww crap...I hate it when people call me on my bold assertions.
Okay, so I'm probably not the best person to try & argue this point but I'll give it a shot. For me there are three reasons static type systems are cool.

• Proving properties about your code.
• Giving the compiler as much information as possible about your code.
• A source of new abstractions.

...
So, that's my general feeling. I have been writing software a lot less long than you have, though, so feel free to take it with a few grains of salt.

Excellent, that's what I was looking for. BTW, this wasn't meant to "call you" on your assertion. I'm honestly trying to learn, because I haven't ever "gotten it" with why people go so ga-ga over type theory and type systems. It all seems to theoretical to me and I struggle with trying to ground it with something practical. For what it's worth, I went to a Grateful Dead concert once and didn't "get it" either. Maybe it was the lack of THC in my system, I have no idea.

So, I understand proving properties about the code and giving the compiler as much information as possible, at least in the simple sense. If you can, though, give me a small example of that. I mean, obviously, I understand type mismatches and eliminating errors when you're passing an integer to a function that wants a string, blah, blah. Give me a simple "blow your mind" sort of example, if that's possible, beyond the pedestrian "eliminate a type error" sort of thing. How would a type system make the compiler be able to auto-parallelize my code or something like that, when it wasn't able to do that before?

Secondly, give me an example of "a new source of abstractions." Again, keep it simple. I'm a below average engineer, not a theorist, remember.

The question is rather broad. Do we "need" a better type system? Better in what way? That is, it would help to phrase the question in terms of "Lisp's type system has the following problem in the following scenario:".

I have heard people criticize the fact that CLOS classes are types, but I am not up on the reasoning behind this.

Is the question whether Lisp ought to have "static" types, i.e. variables that are annotated so that they can only hold certain types of values? That's a huge topic and there are all kinds of factors involved (not to mention the whole question of whether it would be appropriate to call such a language "Lisp"!). A few things off the top of my head:

I spent some years programming in Java, and there certainly are pros to having typed variables, especially typed parameters in functions (Java Interfaces too). I also like seeing types in things like hash tables, e.g. Java's HashTable<Integer, Person> or whatever. They also help catch certain kinds of errors at compile-time, which is helpful during development. But there are also many drawbacks.

At ITA, we have a macro called define-strict-function, in which you provide an argument list with Lisp types for each argument, and it expands into check-type forms that check the argument types are runtime. (It also checks returned values and conditions signaled, and there's a -method variant, etc, etc.) We use these for major interfaces into big modules. This is good for the same reason that it's generally good to put "assert"'s in various places in your code.

Check out "Typed Scheme" at http://www.ccs.neu.edu/home/samth/typed-scheme/. The work is being done by grad student Sam Tobin-Hochstadt under the supervision of Matthias Felleisen, who knows as much about type systems in languages as anyone in the world, and who has a very deep understanding of Lisp and Scheme.

I've always wished that CL had at least an option for compile time type checking. Maybe one of the commercial implementations have something.

Chris

secondly, give me an example of "a new source of abstractions." Again, keep it simple. I'm a below average engineer, not a theorist, remember.

Having moved to CL from ML in many ways, one of the things I find myself wanting to do every once in a while is using types as a method of abstraction, in particular what ML terms algebraic data types (or at least that's how I was taught it).

So a good example of this functionality already in lisp is the list, where you have either a cons cell or nil. This is in many ways a conceptual abstraction in order to better reason about lists. Now one of the things you can do in ML is declare new constructors, so that you can define a tree for example, in the same way. It can be a Node, which has 3 fields in it (a left branch, a value, and a right branch), or a Leaf which has just a value. Now there are many other ways to represent this (such as just having a leaf node be one in which both branches are nil, a la the common c++ definition, or a list of lists a la what i assume is common in lisp systems) but once I saw this other method, I always found it more intuitive.

Now that being said, it is possible to some extent to mimic the dynamic behavior of such constructs by writing the predicates by hand and/or using the deftype form (i believe there are asdf-installable packages which also bundle the work into a couple macros). However, there's a few reasons why I always feel put off by this approach. One main one is that I really don't understand deftype... I keep reading the hyperspec definitions and coming away still not knowing how to correctly use the form. The other reason is that type decls, which can be annoying to include in the first place, are also allowed to be ignored by the complier in implementation dependent ways, which makes the whole behavior questionable when migrating systems.

That being said, there's arguments both for and against static type systems, a la ML / Haskell vs a dynamic type system like lisp. The particular win i see for lisp is exploratory programming is almost prohibitive in a static type system for any problem which would incorporate meaningful type abstractions. However, when not performing exploratory programming (which admittedly is my preference) compile time static type inference provides alot of useful information for debugging purposes, without having to engage in the tedium of using type declarations everywhere, which also many times I feel like I don't understand.

So does lisp need a better type system? In my opinion, there are type constructs that can be useful for thinking about problems, and type inference can help in debugging. But much of that is a personal choice, some people view one or both of those as a hurdle to effective software development. A different type system is one option, though in many cases I'd settle for better documentation of the one already existing. I just never did find it clear.

findinglisp wrote:Whenever I read anything about type systems on Lambda the Ultimate or other more theoretically-oriented sites, my eyes just glaze over and and I start drooling.

Well, yeah. That's because LtU people are off in the future, working on type systems that have powerful capabilities, but haven't yet been reduced a form that one can use and understand without learning category theory first. If you want a feel for what a more advanced type system can do for you, go play with some form of ML. It's not as far along as dependent types and the other drooligens you see on LtU, but it's much nicer than the sorts of things you see in more mainstream languages.

metageek wrote:

findinglisp wrote:Whenever I read anything about type systems on Lambda the Ultimate or other more theoretically-oriented sites, my eyes just glaze over and and I start drooling.

Well, yeah. That's because LtU people are off in the future, working on type systems that have powerful capabilities, but haven't yet been reduced a form that one can use and understand without learning category theory first. If you want a feel for what a more advanced type system can do for you, go play with some form of ML. It's not as far along as dependent types and the other drooligens you see on LtU, but it's much nicer than the sorts of things you see in more mainstream languages.

Good suggestion. Thanks, I'll check out ML. That's one language I have never looked at in the slightest.

cperkins wrote:I've always wished that CL had at least an option for compile time type checking. Maybe one of the commercial implementations have something.

Hm, what's this then?

CL-USER> (defun foo (x) (declare (string x)) (setf x (list x)))
; in: LAMBDA NIL
;     (SETF X (LIST X))
; --> SETQ 
; ==>
;   (THE #<SB-KERNEL:UNION-TYPE STRING> (LIST X))
; 
; caught WARNING:
;   Asserted type STRING conflicts with derived type (VALUES CONS &OPTIONAL).
;   See also:
;     The SBCL Manual, Node "Handling of Types"
; 
; compilation unit finished
;   caught 1 WARNING condition
FOO
CL-USER> (defun bar (x) (car (- x)))
; in: LAMBDA NIL
;     (CAR (- X))
; 
; note: deleting unreachable code
; 
; caught WARNING:
;   Asserted type LIST conflicts with derived type (VALUES NUMBER &OPTIONAL).
;   See also:
;     The SBCL Manual, Node "Handling of Types"
; 
; compilation unit finished
;   caught 1 WARNING condition
;   printed 1 note
BAR

Sure, this is not what the static typing crowd calls type checking, but it still looks an awful lot like it to me!

Re. issues with the type system or related parts, in no specific order:

• Can't declare exact type of array (fill-pointer, adjustability, displacement).
• Can't declare functions are pure/foldable/flushable.
• DEFTYPE cannot specify a recursive type, and no SIMPLE-LIST type (where CAR would always be of a specific type).
• Arrays of element type NIL are strings.
• Incompabtible re-declamation of a global type of ftype business as usual. No need to forbid it, but requiring consistency *across* different compilation units and a full warning on redefinition would be good.
• No standard way to extend proper compilation units across files. (WITH-COMPILATION-UNIT deals with warnings, and implementations are not allowed to make it imply other things for multi-file scope without using a non-standard keyword argument.)
• Subclasses are allowed to restrict their slot types.
• Non-monotonic class linearization.
• No sealing.
• No way to define funcallable structures (or structures with other metaclasses.)
• No standard environment access to declared types.
• No CONSTANT-VALUE. (Extract the value of form for which CONSTANTP is true.)
• No standard way to write optimizers for post-source stages of compilation, where type-inference information is available. (Moral equivalents of SBCL's DEFTRANSFORM and DEFINE-OPTIMIZER DERIVE-TYPE.)

Some of these can be deal with in user-space, some with implementation specific extension -- but some things like subclasses restricting their slot types, and non-monotonicity cannot (Well, they can if you reimplement chunks of CLOS, but that's like saying you can do closures in C). ...how serious such omissions are, is another question entirely.

Cheers,

-- Nikodemus