Does Common Lisp need a better type system?

[levy]

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

[TheGZeus]

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

[wchogg]

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.

[findinglisp]

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?

[levy]

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

[wchogg]

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

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.

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.

[pTymN]

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.

[wchogg]

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.

[findinglisp]

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.

[dlweinreb]

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.