Constraint-Based Polymorphism in Cecil

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