Summary
Why don't we treat it like a set of tests?
Advertisement
I've had a lot of feedback since my last blog. A few people pointed out that Common Lisp and Erlang do something similar. Several people pointed toward Guido's desire to add static typing to Python (I had read about that.. it would be cool to see if this separate compiled type annotation thing could work in Python), and several pointed toward Gilad Bracha's paper on pluggable type systems [PDF] and it looks like the same idea. I knew someone had to have thought of this before. I wish I'd seen those references earlier :-(
One thing I'm wondering, though. In that paper, Gilad talks about type systems being pluggable. What would it be like if they were end user extendable? I know AspectJ allows you to produce errors and warnings based upon static aspects that you specify. For instance, you can have AspectJ produce an error if a someone creates an object of a particular class using new in another particular class. Essentially, that extends the type system.. but from another point of view, couldn't it be seen as a test for a design constraint?
Let's try this point of view on for a second.. The type system of a language is really a set of tests, run by the compiler or the generated runtime. Perhaps we should treat the static end of a type system as a set of tests. Make it them programmable. A project could start out with a set of constraints, as tests, and elaborate them as the project progresses.
I don't know that I see it as a set of test, or at least, I don't find that to be the greatest value of static typing. Here's an off-the-cuff analogy: I see it as more of a registration system. When I declare an variable to be of a type, I'm saying this this the API I am using. If you are going to change it, you need to either make sure you don't break me or you're going to hae to fix me.
Whether that fits with the rest of your post or not, I'm not sure.
> I don't know that I see it as a set of test, or at least, > I don't find that to be the greatest value of static > typing. Here's an off-the-cuff analogy: I see it as more > of a registration system. When I declare an variable to > be of a type, I'm saying this this the API I am using. If > you are going to change it, you need to either make sure > you don't break me or you're going to hae to fix me. > > Whether that fits with the rest of your post or not, I'm > not sure.
I think it does. It's just a different perspective on the same thing. For what you were describing I'd say that the test is something like:
Verify: "all things declared as X have these operations and no part of the program attempts to invoke any other operations on Xs."
I agree that there are many other ways to see a type system and people like them for many reasons, but I think it's interesting that we could articulate a type system as a set of tests. Right now, these tests are usually hidden in a compiler or a runtime system.
> Let's try this point of view on for a second.. The type system of a language is really a set of tests, run by the compiler or the generated runtime.
Interesting. For a language that is not fully statically typed, would you consider a runtime exception a "test"? A thrown CastClassExceptions is certainly the type system in action (or is that "type system inaction"?) but I wouldn't classify it is a "test". My distinction here is that things like that are not something executed, either by compiler or runtime, before deployment.
By that razor, runtime checks are not tests, since they're not part of a repeatable process. Triggering certain runtime behaviors, including verifying type checks at runtime, can be encoded in artifacts (e.g. unit tests) I'd consider tests.
Static typing could be classified as a test, as the validation is checked during compilation, a repeatable process.
> > Let's try this point of view on for a second.. The type > system of a language is really a set of tests, run by the > compiler or the generated runtime. > > Interesting. For a language that is not fully statically > typed, would you consider a runtime exception a "test"? A > thrown CastClassExceptions is certainly the type system in > action (or is that "type system inaction"?) but I wouldn't > classify it is a "test". My distinction here is that > things like that are not something executed, either by > compiler or runtime, before deployment.
I could argue that either way. The neat thing is that some IDEs drop their UT errors in the same pane as the compiler errors. One could consider UT execution part of a compilation's semantic check or the semantic checks of compilation as part of test execution. They are more alike than different to me.
> By that razor, runtime checks are not tests, since they're > not part of a repeatable process. Triggering certain > runtime behaviors, including verifying type checks at > runtime, can be encoded in artifacts (e.g. unit tests) I'd > consider tests.
I agree.
> Static typing could be classified as a test, as the > validation is checked during compilation, a repeatable > process.
For me, types are more a form of reliable documentation than a set of tests. When using a 3rd party library, it is nice to know the expected parameter and return types without having to rely on out-of-date or missing documentation, or having to inspect the code.
Also, the extremely useful auto-completion that IDE's can do with a static language is in a sense due to the formal/reliable documentation that the static typing provides.
> For me, types are more a form of reliable documentation > than a set of tests. When using a 3rd party library, it > is nice to know the expected parameter and return types > without having to rely on out-of-date or missing > documentation, or having to inspect the code. > > Also, the extremely useful auto-completion that IDE's can > do with a static language is in a sense due to the > formal/reliable documentation that the static typing > provides.
That's fine. Notice that it's not incompatible with anything I'm saying. I'm not saying get rid of static types; I'm saying put the type system under the control of the programmer.
We're in an odd state right now. The static vs. dynamic debate is so far in the forefront that we can't seem to talk about typing at all without the conversation moving in that direction. It's a shame. There are so many more things to talk about.
> A few people pointed out that Common > Lisp and Erlang do something similar. Several people > pointed toward Guido's desire to add static typing to > Python (I had read about that.. it would be cool to see if > this separate compiled type annotation thing could work in > Python), and several pointed toward Gilad Bracha's paper > on <a > href=http://pico.vub.ac.be/~wdmeuter/RDL04/papers/Bracha.pd > f>pluggable type systems [PDF]</a> and it looks like the > same idea. I knew someone had to have thought of this > before. I wish I'd seen those references earlier :-(</p>
I'm glad you didn't, because as usual you bring your own unique and intelligent approach to the table, enriching the discussion.
> <p>Let's try this point of view on for a second.. The > type system of a language is really a set of tests, run by > the compiler or the generated runtime. Perhaps we we > should treat the static end of a type system as a set of > tests. Make it them programmable. A project could start > out with a set of constraints, as tests, and elaborate > them as the project progresses.</p>
I like this idea. So how about this: place these tests in a java-style interface, to distinguish them from implementation code? Then allow them to be conditionally compiled.
To be precise, the statically verifiable parts of a type system could usefully be construed as tests, but the dynamic part (runtime checks, etc) are not. This pedant would be much happier if this thread were titled "The statically veriable parts of a type system comprise a set of tests".
>We're in an odd state right now. The static vs. dynamic >debate is so far in the forefront that we can't seem to talk >about typing at all without the conversation moving in that >direction. It's a shame. There are so many more things to >talk about.
Isn't that the truth.
I definately think static typing (and other forms of static code checking) and automated testing are very similar in purpose and should be grouped together. Both serve to give the programmer rapid feedback as to the correctness of his program.
The purpose of a programming language is for the programmer to communicate with the computer. Specifying type information (and potentially additional DBC information) allows the computer to better validate that that what the programmer is saying makes sense.
The problem is, often times at the early stages of writing a program, the programmer doesn't understand the program adequately for type information to be overly meaningful. Think of specifying type information as trying to explain the details of a concept that you don't understand to another person. All it produces is confusion.
Conversely, failing to specify type information for an understood program opens the door to unnecessary confusion. It's like being vague when there's not reason to be vague. It's like hiding something from the computer.
So specifying static type information in early code is similar to premature optimization, but failing to do so in more mature code invites errors.
The program should be no more and no less precisely defined than it is precisely understood.
What we need is not only pluggable type systems, but a programming language that is programmable at compile-time. In other words, we need a compiler that has no default parts other than the one specifying the mechanism that allows it to perform compile-time processing. All these concepts (pluggable type systems, AspectJ etc) fall under the same question: "how can I program the compiler to interpret my code the way I like?"...
Most programming languages offer a fixed way of interpreting code. Some offer clever macro systems (Lisp/Scheme, Dylan etc) or archaic ones (C/C++), but no language so far has been invented that the compiler can be fully defined in itself. There are extensions of mainstream programming languages like MetaC++ or MetaJava, but they are not mainstream yet. I think that meta-programming is the key to pluggable type systems, aspects etc.
> > I knew someone had to have thought of this > > before. I wish I'd seen those references earlier > :-(</p> > > I'm glad you didn't, because as usual you bring your own > unique and intelligent approach to the table, enriching > the discussion. > > > <p>Let's try this point of view on for a second.. The > > type system of a language is really a set of tests, run > by > > the compiler or the generated runtime. Perhaps we we > > should treat the static end of a type system as a set > of > > tests. Make it them programmable. A project could > start > > out with a set of constraints, as tests, and elaborate > > them as the project progresses.</p> > > I like this idea. So how about this: place these tests in > a java-style interface, to distinguish them from > implementation code? Then allow them to be conditionally > compiled. > > What do you think?
It seems okay except that I can imagine these tests (which stand in for type rules) spanning across several types. I'm rather excited by Stroustrup's idea of use-patterns for expressing 'concepts' in C++. One of the neat things is that they, like tests, are example-based. Have you looked into that work at all?
Flat View: This topic has 73 replies
on 5 pages
[
12345
|
»
]
Previous Topic
