Check out the new USENIX Web site. next up previous
Next: Values Up: Names, Lifetimes, Types and Previous: Lifetimes

Types

Nickle has two sets of type consistency rules. First, any object in the program may be statically typed. The static type system strongly resembles that of C or Java. Syntactically, Nickle types are required to be like Java's optional ``left-hand'' syntax: type declarations appear to the left of program objects, and are modified type-by-example. Semantically, there are subtle but significant differences between the type systems of these languages. Nickle allows objects to be explicitly typed poly, indicating that the type need not be statically checked. Unlike C, arrays with different sizes are not of different type. Nickle has more types than C, including a disjoint union type and multi-dimensional array types. Structure types obey a subtype relationship over their members. The void type is handled slightly differently than in C: in Nickle, there is a single value of type void, written as <>, allowing the void type to interact more smoothly with the rest of the language without significant loss in security. All of this adds up to a type system which provides full security while retaining reasonable expressiveness.

Secondly, all operations are currently checked for type consistency (as well as performing array bounds checking and the like) at runtime. While in principle many of these runtime checks could be removed by static type checking, and others could be hoisted in order to improve performance, runtime type checking is not currently believed to be a performance bottleneck, and the implementation is greatly simplified by this choice. The combination of strong static checking and complete runtime checking does normally mean that program defects will be caught ``as early as possible'', providing confidence in execution correctness and aiding debugging.


next up previous
Next: Values Up: Names, Lifetimes, Types and Previous: Lifetimes
Bart Massey 2001-04-19