日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

Outlook on Composite Type Labels inUser-Defined Type Systems
Antoine Tu

Shigeru Chiba

This paper describes an envisioned implementation of user-defined type systems that relies on a feature wecall composite type labels for type-checking. Desiging a type system is a complex task, and while someuser-defined type systems exist to address the need for use-case specific types, those systems usually havea high level of verbosity and compromise on expressiveness to ensure safety. Our preliminary approachaddresses these problems through automating the instantiation of additional type labels, the derivation ofimplicit conversion rules and the resolution of ambiguities during type-cheking as necessary. To achieve that
we rely on composite type labels, that are defined by composition rules. We first begin by identifying somekey problems with current approaches, after which we demonstrate how our planned system solves them.

1 Introduction
In this paper, we present a system for typechecking user-defined type labels that relies on composition rules to reduce the cognitive load on programmers while ensuring a high level of expressiveness in declaring new type labels. Our approach
uses those rules to automatically instantiate additional type labels when appropriate. Similarly, oursystem automatically derives implicit conversions
between instantiated type labels and performs typenormalization where necessary.
A programming language’s built-in type system
only provides a small set of primitive types thatare suitable for general use-cases. In some applications however, use-case specific types are useful toprevent type-related errors that are not handled by
the general-purpose built-in type system. The ideaof allowing programmers to bring in their own typesystem to enhance the existing one has already been
proposed by Bracha [1] and is called user-defined orpluggable type systems. Current implementationsof this idea only implement it partially and in a restricted fashion, as it is challenging to open up the
コンポジットタイプレーベルによるユーザ定義型システム
ツ アントアン 千葉滋, 東京大学情報理工学系研究科,
Graduate School of Information Science and Technology, The University of Tokyo.

type system while maintaining the safety promisesof the overall system.
We believe that for a type system to be useful,it must provide users with a high level of expressiveness while minimally increasing the cognitive
load required to define and use such type system.
To achieve this, we extend the idea of user-defined
type systems by proposing composite type labels.
A composite type label is a type label that is defined by the composition of traditional type labelsor other composite type labels through user-definedcomposition rules. Our contribution is the automatic instantiation of additional type labels using
type label composition rules, implicit conversion
support for pluggable type systems using path finding, and the automatic resolution of flow merging
ambiguities through the automatic application oftype normalization. We believe these contributions
enhance existing pluggable type systems by reducing the cognitive load on programmers while maintaining an equal or higher level of expressivenesscompared to existing systems.

2 Motivation
User-defined or pluggable type systems [1], asdefined by Bracha, have been introduced to address the need to support use-case specific typesystems in addition to a host language’s built-

in type system. Their implementations do so byproviding a framework that allows users to define additional attributes, which we will refer toas type labels, that can be attached to primitive
types to provide additional information to the typechecker. Type-checking is then performed against
those user-defined type labels on top of the regular type-checking that occurs in the host language.
This allows users to bring their own type system
to the host language. For instance, the Checker
Framework [4] described by Papi et al. accomplishes this by providing a compiler extension tothe Java programming language that parses userdefined type labels implemented through Java type
annotations.
2. 1 Reducing definition burden
Those systems however are subject to several
constraints to ensure that users do not introduce
unexpected behavior to the host language. Indeed,
they often demand a high level of verbosity on
the part of the programmer, and provide low expressiveness. The previously introduced Checker
Framework, for instance, requires every type label
to be explicitly defined and doesn’t provide support
for combining type labels.
As an example, if we wanted to implement a typesystem to express units of measurement, current
systems would require us to explicitly define allunits of length (m, km, cm, etc.) and time (sec,min, hour, etc.) as well as all possible combinationsof length and time (m/sec, m/hour, km/hour, etc.).
Furthermore, current systems do not provide a way
to relate composite types such as km/hour with thetypes labels they are composed of (km and hour ).
For all intents and purposes, current systems treat
them as completely unrelated types.
The problem with this approach is that due to its
high verbosity it increases the cognitive load on theprogrammers who want to define type labels. To
support more complex user-defined type systems,
we therefore need to provide a way of reducing definition burden.
2. 2 Implicit conversions
Implicit conversions are useful in a type system as
they reduce the need for programmers to explicitly
annotate conversions, but they are usually avoided
by current user-defined type system approaches due

1
2
3

double@m foo = 5;
double@mm bar = 59;
double@Length baz = foo + bar ;Fig. 1

Flow merging in Checker Frameworkpresented using C# syntax

to the additional level of complexity its support introduces. Indeed, the Checker Framework does notsupport rewriting values and therefore has limited
support for implicit conversions. Defining all possible implicit conversions for a type system consisting of n type labels would be an eﬀort of the orderO(n2 ). We therefore want to have a mechanism fordefining implicit conversions with a low definitionburden.
2. 3 Resolving ambiguity
Current systems like the Checker Framework allow the grouping of type labels into something similar to a subtyping or subclassing relationship witha parent or abstract type label. For instance, aprogrammer can define type labels m (meter) andmm (millimiter) as being concrete incarnations of
the Length abstract type label. A variable declared
as Length may take on a label m or mm later onthrough a process the authors call type refinement
which assigns to a variable a more restrictive typelabel if such label is found to exist [4]. However,this process only applies from the abstract type label to a concrete one, and doesn’t allow for interactions between concrete type labels.
Indeed, merging two data flows of diﬀerent typelabels results in a compiler error even if both typelabels are related. For instance, in Figure 2. 3 we
present a simple Checker Framework example, that
we have rewritten in C# syntax for consistency
with the language used in this paper. In this example, if we try to add two units of Length, namely mand mm, the compiler throws an error since it is unclear which type label this operation should resultin. However, it is necessary in our composite typelabel implementation to handle such ambiguities.
Indeed, since we automatically generate additional
type labels, we cannot rely on the users to explicitly
specify how to solve every ambiguous case.

@Length@m@cm@km/hour

@Time

@km
@Speed...

@m/sec

@sec

@min

...

...

1
2
3
4

int@m foo = 5;
int@sec bar = 2;
int@Speed foobar = foo / bar ;int@Length baz = foobar * bar ;Fig. 4

Sample code using composite typelabelsFig. 212345678910111213Composite type labels

Label m {AllowedTypes : uint ulongdouble
Canonical}
Label cm {AllowedTypes : uint ulong double
C on ve rt Fr om Ca no nical : Multiply(100)Conve rtToCanonical : Divide (100)}
CompositeLabel Length {MemberLabels : m | km | cm
CompositionRules : Speed *Time}

Fig. 3

Definition of labels and composite typelabels

3 Composite Type Labels
A composite type label is a type label that is defined by the composition of traditional type labelsor other composite type labels through user-definedcomposition rules. It can be seen as similar to an
abstract type which can take the instance of any
type label in its definition. The concrete instance isselected automatically during type-checking. Figure 3 shows the Length, T ime and Speed composite type labels and their members. New type labels
and composite type labels are defined using a provided external DSL for this purpose, as illustrated
in Figure 3.

3. 1 Composition rules
Composition rules define the legal combinationsof type labels or composite labels, providing hints
to the type-checker. They are defined by using theCompositionRules keyword as shown on line 12 of
Figure 3 where we declare that a Length composite
type label can be composed of the multiplication ofa Speed and T ime. Figure 3. 1 shows sample C#code that uses those type labels. In lines 3 and4, composite type labels are used. During typechecking, line 3 will resolve to m/sec while line 4
will resolve to m, according to the respective composition rules of the declared type labels.
3. 2 Implicit conversion rules
Implicit conversions are implemented by resolving conversion paths. Indeed, a programmer only
needs to select a type label to be a canonical representation, and provide conversion rules to and fromthe canonial type label. In Figure 3, we declare m
to be a canonical type label, and declare conversions for cm in lines 7 and 8. Based on those rules,
we define that there is an implicit conversion between a type label A and B if there exists a conversion path from A to B that goes through theirrespective canonical type labels and can automatically resolve additional implicit conversions fromthe minimal set provided.
This approach is inspired from the Checker
Framework, which provides an interface to relate
sub-units like mm and km to the base unit m.
However, it does not support modifying values during type-checking, and the sample code in Figure
3. 2 will type-check, but the result will be erroneousas the run-time semantics are diﬀerent than thoseduring compile-time. In this example, line 3 will
yield a value of 10.0 instead of the correct value of
5.05.
In more complex cases such as composite type la-123

double@m foo = 5;
double@cm bar = 5;
Console . WriteLine ( foo + bar ) ;Fig. 5

An example where implicit conversion
is neededbels composed of two or more type labels, we needto perform that conversion path finding exercise on
all of the type labels that compose the type. For instance, to convert from a km/hour composite typelabel to a m/sec type label we will need to findconversion paths joining km to m as well as hourto sec. This might lead us into edge cases such aswhere the conversion rules defined by the programmer yield a path from km to m but not hour tosec. In this case, a conversion from km/hour tom/sec will not be possible. As we cannot make a
judgement on whether this is intended behavior or adefinition omission on the part of the programmer,
we will reject this code and generate a compiler
warning.
In allowing programmers to define conversion
rules, we need to prevent them from introducing
unintended behavior. Some general-purpose languages such as C# that allow programmers to define their own implicit conversions and put that responsibility on the them. In our case, since oursystem automatically resolves conversion paths itwould be counter-intuitive to rely on programmers
to predict inconsistent behavior. For this reason,
we chose to restrict the rule definition by only allowing programmers to define conversion rules bycalling built-in conversion methods in our provided
DSL, as illustrated in lines 7-8 of Figure 3. Thesemethods can be chained, allowing more complex
conversion rules to be composed.
3. 3 Type normalization
We perform type normalization automatically tosolve the ambiguity problem presented in Section
2. 3. Such normalization is also needed for our typechecker to validate a variable’s type label against
composition rules. During type checking we examine the AST (Abstract Syntax Tree) for nodes
where type labels are being used. We validate
expressions by traversing their left and right sub-trees and comparing them to type label composition rules, which we store internally as a tree structure. In more complex expressions where the left or
right subtrees are deeply nested, we perform suchcomparisons on the smaller subtrees and normalizethem.
In order to resolve ambiguous cases like the one
presented in Figure 2. 3, we use the canonical typelabel as a default type label, and will fall back to
it if no better candidates exist. In this case thebar variable on line 3 will be implicitly converted
from mm to m and the resulting type label for baz
will be m. In more complex cases where a simple
fallback may not resolve all ambiguities, we rely on
the order of definition of the type labels.

4 Related Works
Papi et al. have introduced the Checker Framework, which is a pluggable or user-defined type system implementation in Java which relies on Javaannotations to provide additional information to
the type-checker [4]. However, it doesn’t support
automatically instantiated type labels and thus
comes with a high level of verbosity. As well, itcannot rewrite or change the value of a type during
type-checking and therefore does not support implicitly converting variables during type-checking
to resolve ambiguities when merging data flows.
The JavaCOP framework introduced by Markstrum et al. behaves similarly to the Checker
Framework in that programmers write additional
checkers whose goal is to enhance the built-in typesystem [3]. One improvement JavaCOP had over
the Checker Framwork is an enhanced capability
for dataflow analysis. It however suﬀers from thesame downside of not supporting type label combinations.
It is also worth mentioning that the F# programming language provides support for user-definedmeasurement units, albeit only for numerical types[2]. Those act like type labels in the sense thatusing them adds some label metadata to the variable, allowing the type-checker to perform some additional consistency checks. The interesting part ofF#’s implementation is that it provides some elementary support for combining labels and instantiating new ones. However, such label combinationis performed liberally, without any regard to user

intent. While we also feature measurement units
in our code examples throughout this paper, oursystem aims to support arbitrary user-defined typelabels and therefore an unbounded combinatory behavior is not appropriate for general use.

5 Conclusion
In this paper we introduced composite type labels, which is a new class of type labels that isdefined recursively by traditional type labels andcomposition rules. We further elaborated how we
use those composition rules to automatically instantiate additional type labels as necessary, infer
implicit conversion rules based on path finding andresolve ambiguities in user code by automatically
performing type normalization. In doing so, we reduce the cognitive load imposed on programmers

by existing user-defined or pluggable type systems
while providing them with a higher level of expressiveness in the definition of type labels.
References[1] Bracha, G.: Pluggable type systems, In OOPSLA 04 Workshop on Revival of Dynamic Languages, 2004.
[2] Kennedy, A.: Types for Units-of-Measure: Theory and Practice, Springer Berlin Heidelberg, 2010,
pp. 268–305.
[3] Markstrum, S., Marino, D., Esquivel, M., andMillstein, T.: T.: Practical enforcement and testing of pluggable type systems, Technical report.
[4] Papi, M. M., Ali, M., Correa, Jr., T. L., Perkins,
J. H., and Ernst, M. D.: Practical Pluggable
Types for Java, Proceedings of the 2008 International Symposium on Software Testing and Analysis, ISSTA ’08, New York, NY, USA, ACM, 2008,
pp. 201–212.