[evlan-devel] Logical types

[Kenton V. <tem...@ga...>]

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