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.
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.
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.
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.
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)
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.