Dominic Duggan

*Finite subtype inference* occupies a middle ground between
Hindley-Milner type inference (as in ML) and subtype inference
with recursively constrained types. It refers to subtype
inference where only finite types are allowed as
solutions. This approach avoids some open problems with
general subtype inference, and has practical motivation where
recursively constrained types are not appropriate. This paper
presents algorithms for finite subtype inference, including
checking for entailment of inferred types against explicitly
declared polymorphic types. This resolves for finite types a
problem that is still open for recursively constrained types.
Some motivation for this work, particularly for finite types
and explicit polymorphism, is in providing subtype inference
for first-class container objects with polymorphic methods.

Michael Hicks

We examine the design space for copying garbage collectors (GCs) in which ``large objects'' are managed in a separate, non-copy-collected space. We focus on two main issues:

We explore these issues experimentally using Oscar, our GC testbed. In particular, we vary the threshold size of large objects and also whether the objects may contain pointers. Furthermore, we compare the performance of treadmill collection to that of mark-and-sweep collection for managing the large object space.

We find that there is a minimum cutoff size below which adding objects to the large object space does not result in a performance improvement. In addition, there is no significant reduction in speedup if pointer-containing objects are also included in the large object space. Finally, the exact method used to collect the large object space does not overly influence overall performance.

Fermin Reig

C is used by several research compilers as its target language, relying on a C compiler to generate machine code. In this way, you obtain portability for free. However, C was not designed for this purpose and it limits the compiler's writer flexibility and the performance of the resulting code. C-- is a compiler target language that aims to be portable and suitable for efficient code generation. I will describe C--'s motivations and design rationale, and an implementation using the MLRisc back end.

Stephen Weeks

*This is the first talk in what I hope will become a regular series at
NJ-PLS. The aim is to present programming techniques that make the
languages we like to program in more usable, hopefully making
interesting use of type systems, module systems, higher-order
functions, laziness, continuations, etc.*

It is often useful to associate information with parts of a data structure. For example, the graph algorithm depth-first search associates a boolean with each node indicating whether or not the node has been visited. As another example, a simplification pass in a compiler might associate an occurrence count with each variable. There are several ways to implement such associations. The monolithic solution is to define a field in the data structure for each piece of information that may be associated. Other solutions include the use of polymorphic data structures and the use of tables mapping the data structure to the auxiliary data. All of these solutions have drawbacks, either in time, space, typeability, or modularity. In this talk, I show how to use type-safe property lists in Standard ML to implement dynamically extensible data structures and describe their use in graph algorithms and a compiler.

Kim Bruce

Beta's virtual types provide a very handy notation for using inheritance with mutually recursive classes. Unfortunately, the original design requires run-time checks in order to assure type-safety. By going back to some of our early work on the semantics of object-oriented languages, we have been able to see how to generalize type systems to provide a statically type-safe notation with expressiveness comparable to that of virtual types. The solution involves a generalization of the "MyType" notation for the type of "self" or "this", and should be compatible with most statically-typed object-oriented languages.

(This is joint work with Joe Vanderwaart)

Vijay Saraswat

Henry Cejtin

We describe a method of reflecting all the information gathered by a 0-CFA style flow analysis in the simply-typed lambda calculus, and a closure-conversion algorithm that uses this technique. This closure conversion algorithm is used in MLton, a whole-program optimizing compiler for Standard ML. In this setting, the output of the closure conversion algorithm being well-typed constitutes a proof that the flow information is sound. The method of encoding flow information in simple types is to insert coercions when values flow from program points where the flow information is more precise to where it is less precise. Data representations can be chosen so that these coercions have no run-time cost.