|
From: Kenton V. <tem...@ga...> - 2003-02-14 18:50:55
|
Yeah, so things have been taking some time, as you probably noticed. The
thing is, as I have been implementing, I started coming up with new
ideas. One big one is a complete revision of how types work... which I
will now attempt to explain.
First, forget everything you know about types and objects. As a matter of
fact, start thinking about objects in a first-order predicate calculus
fashion. An object is some abstract thing which has a set of
properties. We define these properties using predicates.
Now, what is a type? A type is simply a set of predicates... or, rather,
it's an implication:
isa(object, Array) =>
hasField(object, elementType) &
hasField(object, size) &
isa(object.elementType, type) &
isa(object.size, Integer)
Here we have said that if "object" is of type "Array", then it has fields
"elementType" and "size", where "elementType" is some type, and "size" is
an Integer.
Now, if we have some particular object "MyArray" which is an array of
integers, we could specify this like so:
isa(MyArray, Array) & equals(myArray.elementType, Integer)
Now, where this gets interesting is, say we have a function which gets an
element of the array:
getElement = array => index => #...
To specify the types of "array" and "index", we say the following:
isa(array, Array)
isa(index, Integer)
But, predicates are not just limited to discussing types and fields. We
could also say:
isLess(index, array.size)
isGreaterOrEqual(index, 0)
And, thus, we have specified that the index taken by getElement must be
within the array's range. This fact becomes a precondition to the
function, just as the types of the inputs are preconditions.
Now, the compiler would only allow a function to be called if all of its
preconditions were met. So, the preconditions would have to be provable
within the calling function. The easiest way to satisfy the range
precondition would be to do this:
if (myIndex < array.size) & (myIndex > 0)
then getElement array myIndex
else #handle error...
The compiler would see, in this case, that the precondition must be
valid. This forces people to check these things, which eliminates
potential bugs. Of course, in many (perhaps most) cases, the fact that the
index is within the array's range will already be implied naturally from
the code. (Imagine a for loop which iterates through an array. If the
initial condition is "i = 0" and the loop test is "i < array.size", which
is the usual case, then you automatically know that i is within the range
of the array. Of course, functional languages don't have for loops, but
you get the idea.)
Of course, I have mentioned this idea before. Dusty earlier pointed out
the example of matrix multiplication, where we might want to add the
precondition that the left matrix's width should be equal to the left
matrix's height.
Adding this form of types to the language would do wonders for compile-time
bug catching. Many errors which are currently signaled using exceptions
could be eliminated by using proper preconditions. Catching errors at
compile time is certainly much better than runtime, especially since it's
often the end user who gets stuck with the runtime errors.
This method would also lend itself quite nicely to optimization. The
optimizer would probably keep track of facts using the same logic the
compiler uses, and thus would have all kinds of extra info about the types
and objects in use.
The down side is that the compiler will often have to use resolution (a la
AI) to check if preconditions are met. This is a rather complicated thing
to do. For the prototype, we can just assume that preconditions are met,
or use runtime checks... but eventually we will have to implement the real
thing. Previously, I did not think this was worth it, but I think I have
changed my mind.
What do you think? Dusty, have you come across this sort of scheme in your
research?
-Kenton Varda
|