pluggable type systems

No replies

Mon, 2009-12-28, 18:34

Miguel Garcia

Joined: 2009-06-10,

Hi,

I'm trying to organize a mental map on what has been done and what is to be
done around pluggable-types in Scala. Pointers to issues I might have
overlooked are welcome.

A previous post on scala.debate (Jan 2009) mentions two compiler plugins
that extend type checking (with units of measure [1] and with DTD-aware XML
validation [2]). Later in 2009, another plugin became available, to check
hand-over of references across method calls [3].

What I haven't found so far (pointers are welcome .) is a Scala counterpart
to the JSR 308 Checkers framework [4], offering reusable functionality for
implementers of a certain kind of pluggable type systems (those relying on
compile-time evaluated annotations on types, "type qualifiers" in JSR 308
speak).

From what I've found in the Scala compiler [5], the building block coming
closest is AnnotationCheckers. But the infrastructure provided by the JSR
308 Checkers framework goes beyond that, as summarized in Sec. 3 of [6]. For
example, it includes a flow-sensitive analysis that cuts down on the
boilerplate code one would otherwise have to write. Quoting from [6]:

> The implementation of a [pluggable] type system contains four components:
>
> (1) Type qualifiers and hierarchy. Each qualifier restricts the values
> that a type can represent. The hierarchy indicates subtyping
> relationships among qualified types.
>
> (2) Type introduction rules. For some types and expressions, a qualifier
> should be treated as present even if a programmer did not explicitly write
> it.
> For example, every literal (other than null) has a @NonNull type.
>
> (3) Type rules. Violation of the type system's semantics yields a type
> error.
> For example, every assignment and pseudo-assignment must satisfy
> a subtyping rule. As another example, in the Nullness type system,
> only @NonNull types may be dereferenced.
>
> (4) Interface to the compiler. The compiler interface indicates which
> annotations are part of the type system, the checker-specific
> compiler command-line options, etc.