[Prev][Next][Index][Thread]
Paper on constraint-based polymorphic type system in Cecil
The following paper is now available:
Constraint-Based Polymorphism in Cecil
Vassily Litvinov and Craig Chambers
University of Washington
Technical Report UW-CSE-98-01-01
PoscScript: ftp://ftp.cs.washington.edu/pub/chambers/sbp-tr.ps.gz
We are developing a static type system for object-oriented languages
that strives to guarantee statically and completely the absence of
certain large classes of run-time errors, to enable polymorphic
abstractions to be written and typechecked once separately from any
current or future instantiations, and to avoid forcing code to be
written unnaturally due to static type system limitations. The type
system supports bounded parametric polymorphism, where the bounds on
type variables can be expressed using a mixture of recursive subtype
and signature constraints; this kind of bounding supports F-bounded
polymorphism, Theta-style where clauses, and covariant and
contravariant type parameters as special cases. The type system
coexists with many advanced language features, including
multi-methods, independent inheritance and subtyping, mutable and
immutable state, first-class lexically-scoped functions, and mixed
statically and dynamically typed code. We have implemented this type
system in the Cecil language, and we have used it to successfully
typecheck a 100,000-line Cecil program, the Vortex optimizing compiler.
This is work in progress. The TR presents nondeterministic
typechecking rules; we have implemented a prototype typechecker as
part of the Vortex compiler. We are working on the proof of soundness
and a formal deterministic typechecking algorithm.
Vassily Litvinov http://www.cs.washington.edu/homes/vass/
Cecil/Vortex Project http://www.cs.washington.edu/research/projects/cecil/