In Ceylon 1.2 we've factored out the type system of Ceylon as an independent module, with minimal dependencies and a clean API. The ceylon-model project incorporates:

• an extensible object-oriented model of the type system in Ceylon,
• algorithms for reasoning about types at compile time—or even at runtime in a system with reified generics—and
• a framework for model loading, that is, for loading a model representing the types in a program or module from binary artifacts, source artifacts, or anything else—this is a necessary feature for incremental compilation and modularity.

Why might this be interesting to someone outside the Ceylon team? Well, if you're thinking of creating a programming language with nominal typing, you could consider reusing ceylon-model in your own language, saving yourself the problem of implementing all the hairy typing algorithms that we've already spent years getting right. That way, you can concentrate on the stuff that's really different about your language, that is, the syntax, the compiler backend, the runtime semantics, and the basic language types.

ceylon-model implements an extremely complete type system, including all the following features:

• nominal typing with single-inheritance of classes and multiple-inheritance of interfaces,
• bounded parametric polymorphism (generics with constraints),
• sum types,
• union and intersection types, with sophisticated reasoning about principal types and canonicalization,
• reasoning about subtyping,
• reasoning about coverage and disjoint types,
• principal instantiation inheritance (more powerful than the single-instantiation inheritance found in other languages with subtyping and generics),
• declaration-site and use-site variance,
• type constructor polymorphism (higher-kinded types),
• higher-rank / impredicative polymorphism,
• type aliases including generic type aliases,
• self types, and
• some support for overloading.

It doesn't include any functionality for type inference, flow-sensitive typing, or pattern matching, since in Ceylon that stuff is implemented within the typechecker, and anyway your language probably has different rules to ours.

It seems to me that unless your type system is based on structural typing or dependent types, ceylon-model is an awesome starting point. It might already have everything you need, and, even if it doesn't, it provides a framework that would let you incorporate other features into the type system. For example, I imagine that primitively-defined function, array, tuple, or record types would be easy to incorporate.

We're already reusing this model between the typechecker, two compiler backends, two IDE projects, and the runtime, so we know its API is reasonable.

The only stumbling block is that the project is implemented in Java, so if you want to use it in a compiler written in a different language, you'll probably want to translate it to that language first. The code is pretty clean and straightforward, so that's probably not a massive hurdle to overcome.

The license for ceylon-model is Apache 2.0, so you can basically do what you like with it. But if you decide to use it in a project, please drop us a note, because it makes us happy to see people reuse our work.