• entries
    111
  • comments
    278
  • views
    155513

I Believe in Static Checking I: Constraints

Sign in to follow this  
Promit

190 views

Developing a Graphics Driver III is delayed for a while until I decide exactly what I want in that entry. It won't come until at least Wednesday. Monday should be a SlimDX status update.

I Believe in Static Checking I: Constraints

This entry is actually related to the last one. I mentioned that I have some issues recommending a dynamically typed language to newbies. The truth is that it runs much deeper than that; I have issues with dynamic typing, period. I'm pretty much going to outline my way of thinking here, and explain why I take the views I do. (The title has already spoiled the ending, of course.) I am not trying to change any minds or start a language war here. What I do want is to clarify some of the basic arguments at a theoretical level about static and dynamic typing and my thoughts on them. And lastly, I should mention that this post is by no means grounded in formal computer science theory, so I apologize if I offend any of you heavy CS theory types.

First, forget types. They're not particularly important to the discussion at hand. Hopefully some of you are squirming a little already, because I started off talking about static and dynamic typing, and type systems are frequently the defining aspect of a language. As it turns out, they're not nearly as important as most people think. Second, realize that this discussion is largely independent of specific languages or even paradigms. As such, I'm going to avoid using the term "variable" in favor of the more paradigm neutral "value".

That's the preliminaries out of the way. Let's dig in.

Every program performs various operations on values. In most cases, there are constraints on these values. Constraints limit the flexibility of values and allow us to make concrete assertions about the inputs and outputs of our algorithms. Some constraints are permanent, and some are temporary. Some can be broken for short periods of time, and some are always present. For example, consider a value which represents a month. There are three permanent constraints:
  1. This value must be an integer.
  2. This value must be greater or equal to 0.
  3. This value must be less than 12.
The first in this list is what we previously referred to as the "type"; I will call it the primary constraint. It's the primary because the other constraints are meaningless without it. However, all three constraints are still of equal importance. Violating the integer constraint is no less significant than violating the less than 12 constraint. Here's an alternate method of representing a month:
  1. This value must be a member of the set {Jan, Feb, Mar, Apr, May, Jun, Jul, Aug, Sep, Oct, Nov, Dec}
Most of you will recognize this as an enum. (Be careful though -- there is no integer conversion here.) In this definition, the primary constraint is the only constraint, and attempting to apply #2 and #3 from the other representation would be nonsensical.

Temporary constraints, on the other hand, are constraints that are applied at some point and then removed later. For example, a function might take a reference with a not-null constraint as a parameter. The calling code may well have a reference which does not have this constraint. When the function is entered, the constraint is applied to the value. That constraint is valid for the life of the function, which is also the life of that value (which is of course a copy). You'll notice that temporary constraints will always reduce the valid domain (I use the term roughly based on its mathematical meaning) for a value; if it doesn't, the constraint was redundant and can be ignored.

Constraints are a simple and intuitive concept, so I won't waste any more time on them. (Although there is plenty more to talk about if you want to flesh out the system.) Here is the key to it all, though:
All* constraints can be dynamically checked. Some constraints cannot be statically checked. In particular, temporary constraints can never** be statically checked.
All this talk of static and dynamic typing is just blind dancing around this simple statement of a rather obvious fact.
* Within some limitations. Constraints are themselves code that runs, and we're subject to restrictions about what we can do there.
** I'm lying. Temporary constraints can be statically checked in certain situations, but we're not going to go there. Yet.


The real advantage of a dynamic type system is that all of the constraints on a value can be unified into a single place, both in space (where in the code they are) and time (when you're told about constraint violation). You can simply write a function which can be invoked at any point to check if a value satisfies certain constraints. (And one could imagine that a language could provide all sorts of syntactic support for this.) And having all of the constraints listed in one place is certainly useful, since the conditions for a value to be valid are immediately visible. Additionally, the distinction between temporary and permanent constraints becomes irrelevant at the entry point to a function; the parameters must satisfy certain constraints, and whether or not those were permanently applied is irrelevant. Again, all constraints are equally important; if a reference's not-null constraint is broken, it doesn't matter that the constraint was temporary.

Take note of the connection between duck typing and constraints. Whether an value supports a specific operation or message simply becomes a temporary constraint that is applied. It is checked at the same time as all other constraints, too. The key to verifying the code is test driven development; as long as your tests are fairly comprehensive, you can catch obvious bugs.

A static system, on the other hand, splits the primary constraint away from the rest, because a primary constraint can usually be checked statically. (For an example of when a primary constraint can't be checked statically, consider the last time you used RTTI of any sort, especially when dealing with base and child classes in an inheritance hierarchy.) Classical static type systems attempt to enforce just the primary constraint at compile/parse time, and leave the remaining constraints to the programmer. You can see this behavior often enough, in the form of various checks at the top of a function (whether that function is logic or merely some kind of setter). Most static systems are clumsy and crude, and we're forced to hack around them fairly often. And because we can't check temporary constraints statically anyway, unit testing is still necessary to verify that constraints are being met.

So far, static constraint checking doesn't sound that great. Dynamic checking has apparently everything going for it (except some performance concerns, but that's not something I intend to look at in this series). Static checking doesn't save you the trouble of writing unit tests, and it makes code more complex. But you saw the title. Stay tuned.
Sign in to follow this  


1 Comment


Recommended Comments

Quote:
All* constraints can be dynamically checked. Some constraints cannot be statically checked. In particular, temporary constraints can never** be statically checked.
All this talk of static and dynamic typing is just blind dancing around this simple statement of a rather obvious fact.

It's not that simple. You need a static type system or some other form of syntactic analysis if you want to verify your code is free of deadlock, for example. Dynamic typing can't do that.

Most debates are based upon the false assumption that static and dynamic typing are equivalents. A "dynamic type system", whatever that is, is not the dynamic equivalent of what a type-theorist would call a type system. It effectively amounts to not having a static type system - this is why they would call Python untyped. I'm writing something that would explain all this and explain why I think type systems are a good idea, but for now this does a decent job.

Share this comment


Link to comment

Create an account or sign in to comment

You need to be a member in order to leave a comment

Create an account

Sign up for a new account in our community. It's easy!

Register a new account

Sign in

Already have an account? Sign in here.

Sign In Now