Unifying object-oriented programming with typed functional programming.
The wide practice of object-oriented programming in current software construction is evident. Despite extensive studies on typing programming objects, it is still undeniably a challenging research task to design a type system for object-oriented programming that is both effective in capturing program errors and unobtrusive to program construction. In this paper, we present a novel approach to typing objects that makes use of a recently invented notion of guarded dependent datatypes. We show that our approach can address various difficult issues (e.g., handling "self" type, typing binary methods, etc.) in a simple and natural type-theoretical manner, remedying the deficiencies in many existing approaches to typing objects.
INTRODUCTION
The popularity of object-oriented programming in current
software practice is evident. While this popularity may result
in part from the tendency to chase after the latest "fads"
in programming languages, there is undeniably some real
substance in the growing use of object-oriented program-
ming. In particular, objected-oriented programming can significantly
software organization and reuse through
encapsulation, inheritance and polymorphism. Building on
our previous experience with Dependent ML [20, 18], we are
Partially supported by the NSF Grants No. CCR-0081316
and No. CCR-0092703
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, to
republish, to post on servers or to redistribute to lists, requires prior specific
permission and/or a fee.
ASIA-PEPM'02, September 12-14, 2002, Aizu, Japan.
naturally interested in combining object-oriented programming
with dependent types. However, a straightforward
combination of dependent types with object-oriented programming
(e.g., following a Java-like approach) is largely un-
satisfactory, as such an approach often requires a substantial
use of run-time type downcasting. In search for a more satisfactory
approach, we have noticed that a recently invented
notion of guarded recursive datatype constructors [19] can
be combined with dependent types to enable the construction
of a type system for programming objects that needs
no use of type downcasting. This is highly desirable as type
downcasting is probably one of the most common causes of
program errors in object-oriented languages like Java.
We briefly outline the basic idea behind our approach to
typing programming objects. The central idea of objected-oriented
programming is, of course, the programming ob-
jects. But what is really a programming object? Unfortu-
nately, there is currently no simple answer to this question
(and there unlikely will). In this paper, we take a view of
programming objects in the spirit of Smalltalk [12, 14]; we
suggest to conceptualize a programming object as a little
intelligent being that is capable of performing actions according
to the messages it receives; we suggest not to think
of a programming object as a record of fields and methods
in this paper.
We now present an example to illustrate how such a view
of objects can be formulated in a typed setting. We assume
the existence of a type constructor MSG that takes a type
# and forms the message type (#)MSG; after receiving a
message of type (#)MSG, an object is supposed to return a
value of type # ; therefore, we assign the following type OBJ
to objects:
Suppose that we have declared that MSGgetfst , MSGgetsnd ,
MSGsetfst and MSGsetsnd are message constructors of the
following types, where 1 stands for the unit type.
MSGgetfst
MSGsetfst
In

Figure

1, we implement integer pairs in a message-passing
style, where the withtype clause is a type annotation that
assigns the type int # int # OBJ to the defined function
newIntPair . 1 Note that such ML-like syntax is used to
present examples throughout the paper. Given integers x
1 The reason for newIntPair being well-typed is to be explained
in Section 2.

Figure

2: The value constructors associated with the g.r. datatype constructor HOAS
fun newIntPair x
val
val
fun dispatch MSGgetfst = !xref
| dispatch MSGgetsnd = !yref
| dispatch (MSGsetfst
| dispatch (MSGsetsnd
| dispatch
in dispatch end
withtype int -> int -> OBJ

Figure

1: An implementation of integer pairs
and y, we can construct an integer pair anIntPair by calling
newIntPair(x)(y); we can send the message MSGgetfst to
the pair to obtain its first component: anIntPair(MSGgetfst );
we can also reset its first component to x # by sending it the
message MSGsetfst(x # operations
on the second component of the pair can be performed
similarly; an exception is raised at run-time if anIntPair
cannot interpret a message sent to it.
Obviously, there exists a serious problem with the above
approach to implementing objects. Since every object is
currently assigned the type OBJ, we cannot use types to
di#erentiate objects. For instance, suppose that MSGfoo is
another declared message constructor of type (1)MSG; then
anIntPair (MSGfoo) is well-typed, but its execution leads to
an uncaught exception UnknownMessage at run-time. This
is clearly undesirable: anIntPair(MSGfoo) should be rejected
at compile-time as an ill-typed expression. We will
address this issue and many other ones in objected-oriented
programming by making use of a restricted form dependent
types developed in Dependent ML [20, 18].
The type constructor MSG is what we call a guarded
recursive (g.r.) datatype constructor. The notion of g.r.
datatype constructors, which extends the notion of datatypes
in ML, is recently invented in the setting of functional programming
for handling intentional polymorphism and run-time
type passing [19]. We write # for a guarded type,
where # is a type variable context that may contain some
type constraints. For instance, #1 .# is a guarded type,
this type is equivalent to int # int since we must map #1
to int in order to satisfy the type constraint #1 #2 #
int # bool. The type #2 .# is also a guarded type, where
is equivalent to the
type void, i.e., the type in which there is no element, since
the type constraint #1 #2 # int cannot be satisfied. If
#1 , #2 , #1 #2 #), we notice the type # has
the following interesting feature: instantiating # with a type
#0 , we obtain a type that is equivalent to #1 #1 if #0 is of
the form #1 #2 , or void if #0 is of other forms.
A guarded recursive datatype constructor is a recursively
defined type constructor for constructing guarded datatypes,
{'a1,'a2}.
| {'a1,'a2}.
| {'a1,'a2}.
('a2) HOASapp of ('a1 -> 'a2) HOAS * 'a1 HOAS
| {'a1}. ('a1) HOASlift of 'a1

Figure

3: An example of g.r. datatype constructor
which are a special form of sum types in which each component
is a guarded type. We present a short example of
g.r. datatype constructor as follows for illustrating the no-
tion. More details and examples can be found at [19]. The
syntax in Figure 3 essentially declares a type constructor
HOAS, which can take a type # and then form another type
(#)HOAS. Intuitively, a value of type (# )HOAS represents a
higher-order abstract syntax tree [9, 16] for a value of type
# . The value constructors associated with HOAS are given
the types in Figure 2. Note the type constructor HOAS cannot
be defined in ML. Because of the negative occurrence of
HOAS in the argument type of HOASlam, HOAS cannot be
inductively defined, either. The reason for calling HOAS a
guarded recursive datatype constructor is that HOAS can
be defined as follows through a fixed-point operator, where
# is the kind for types:
-T : #.
Then the value constructors associated with HOAS can be
readily defined through the use of fold/unfold (for recursive
types) and injection (for sum types). We can now define
an evaluation function as follows that computes the value
represented by a given higher-order abstract syntax tree.
fun eval(HOAStup (x1,
| eval(HOASlam
| eval(HOASapp (x1,
|
withtype {'a}. 'a HOAS -> 'a
Note the withtype clause is a type annotation provided by
the user, which indicates that eval is a function of type
#)HOAS #. In other words, the evaluation function
eval is type-preserving.
In the rest of the paper, we are to present a type system
to support g.r. datatype constructors. We then outline an
approach to implementing programming objects, explaining
how various issues in object-oriented programming can be
addressed.
types # | 1 | #1 #2 | #1 #2 |
patterns p ::= x | #p1 , p2# | c[#](p)
clauses ms ::= (p1 # e1 | - | pn # en)
expressions e ::= x | f | c[# ](e)
case e of ms |
values v ::= x | c[# ](v) | #v1 , v2# |
exp. var. ctx. #,
typ. var. ctx. #1 #2

Figure

4: Syntax for the internal language #2,G-
2. THE LANGUAGE # 2,G-
We present a language #2,G- based on the explicitly typed
second-order polymorphic #-calculus. We present both static
and dynamic semantics for #2,G- and then show that the
type system of #2,G- , which supports g.r. datatype con-
structors, is sound.
2.1 Syntax
We present the syntax for #2,G- in Figure 4, which is
mostly standard. We use # for type variables, 1 for the
unit type and # for a (possibly empty) sequence of types
#1 , . , #n . We have two kinds of expression variables: x for
lam-variables and f for fix-variables. We use xf for either
a lam-variable or a fix-variable. We can only form a #-
abstraction over a lam-variable and a fixed-point expression
over a fix-variable. Note that a lam-variable is a value but
a fix-variable is not. We use c for constructors and assume
that every constructor is unary. 2 Also, we require that the
body of either # or fix be a value. The syntax for patterns
is to be explained in Section 2.4.
We use # for substitutions mapping type variables to
types and dom(#) for the domain of #. Note that #
# ], where we assume # dom(#), extends # with a mapping
from # to # . Similar notations are also used for substitutions
mapping variables xf to expressions. We write
.[#]) for the result of applying #) to ., where .
can be a type, an expression, a type variable context, an
expression variable context, etc.
We use # for type variable contexts in #2,G- , which require
some explanation. As usual, we can declare a type
variable # in a type variable context #. We use #
to mean that # is a well-formed type in which every type
variable is declared in #. All type formation rules are standard
and thus omitted. We can also declare a type equality
#1 #2 in #. Intuitively, when deciding type equality under
#, we assume that the types #1 and #2 are equal if #1 #2
is declared in #.
Given two types #1 and #2 , we write to mean that
#1 is #-equivalent to #2 . The following rules are for deriving
judgments of form #, which roughly means that #
matches #.
2 For a constructor taking no argument, we can treat it as a
constructor taking the unit # as its argument.
Pattern typing rules p #)
(pat-tup)
(pat-cons)
Clause typing rule # p
Clauses typing rule # ms : #1 #2

Figure

5: Pattern typing rules
We use #1 #2 for a type constraint; this constraint
is satisfied if we have #1[#2[#] for every # such that
# is derivable. As can be expected, we have the
following proposition.
Proposition 2.1.
. If # is derivable, then # holds.
. If #1 #2 holds, then #2 #1 also holds.
. If #1 #2 and #2 #3 hold, then #1 #
#3 also holds.
2.2 Solving Type Constraints
There is a need for solving type constraints of the form
#1 #2 when we form typing rules for #2,G- . For-
tunately, there is a decision procedure for doing this based
on the set of rules in Figure 7. In these rules, we use T
to range over all type constructors, either built-ins (# and
#), user-defined g.r. datatype constructors, or skolemized
constants.
Theorem 2.2. #1 #2 holds if and only if #1 #
#2 is derivable.
Proof By induction on a derivation of #1 #2 .
2.3 G.R. Datatype Constructors
We use # as the kind for types and (# as the
kind for type constructors of arity n, where n the number of
#'s in (#, . We use T for a recursive type constructor
of arity n and associate with T a list of (value) constructors
c1 , . , ck ; for each 1 # i # k, the type of c i is of the form
is for a sequence of types # i
Expression typing rules
(ty-cons)
(ty-snd)
case e of ms : #2

Figure

Typing rules for expressions
T is not T #
# has no free occurrences in #
# has no free occurrences in #
A is a fresh skolemized constant

Figure

7: Rules for solving type constraints
and # i stands for a (possibly empty) sequence of quantifiers
(assuming
In our concrete
syntax, T can be declared as follows.
typecon (type, .,
| {#2
| .
| {# k }.(# n ) ck of #k
We present some simple examples of g.r. datatype constructors
to facilitate the understanding of this concept.
Example 1 The following syntax
Top of 'a
declares a value constructor Top of the type # TOP;
TOP is defined as -t.#, which is equivalent to #.
Example 2 The following syntax
('a) nil | ('a) cons of 'a * 'a list
declares two constructors nil and cons of the types #.1 #
(#)list and #)list #)list , respectively; the type
constructor list is define as follows, which is essentially equivalent
to the type constructor -t.1 #)t.
Note that the usual list type constructor in ML is defined
as t.
2.4 Pattern Matching
We use p for patterns. As usual, either a type variable
or a value variable may occur at most once in each pattern.
We use a judgment of form v # p #) to mean that
matching a value v against a pattern p yields substitutions
# and # for the type and value variables in p. The rules for
deriving such judgments are listed as follows.
Given a type variable context #0 , a pattern p and a type
# , we can use the rules in Figure 5 to derive a judgment of
the form #0 # p #), whose meaning is formally
captured by Lemma 2.4.
2.5 Static and Dynamic Semantics
We present the typing rules for #2,G- in Figure 6. We
assume the existence of a signature # in which the types of
constructors are declared.
Most of the typing rules are standard. The type (ty-eq)
indicates the type equality in #2,G- is modulo type constraint
solving. Please notice the great di#erence between
the rules presented in Figure 5 for typing clauses and the
"standard" ones in [15].
We form the dynamic semantics of #2,G- through the use
of evaluation contexts, which are defined below.
Evaluation context E ::=
[] | fst(E) | snd(E) | #E, e#v, E# | E(e) | v(E) |
case E of ms
Definition 2.3. A redex is defined as follows.
. fst(#v1 , v2 #) is a redex that reduces to v1 .
. snd(#v1 , v2 #) is a redex that reduces to v2 .
. (#x : #.e)(v) is a redex that reduces to e[x # v].
.v)[# ] is a redex that reduces to v[# ].
. let in e end is a redex that reduces to e[x # v].
. fixf : #.v is a redex that reduces to v[f # fixf : #.v].
. case v of ms is a redex if v # p #) is derivable
for some clause p # e in ms, and the redex reduces
to e[#]. Note that there may be certain amount of
nondeterminism in the reduction of case v of ms as v
may match the patterns in several clauses in ms.
Given a redex e1 , we write e1 # e2 if e1 reduces to e2 . If
and e1 is a redex reducing to e2 , then
we say that reduces to e # 2 in one step.
Let # be the reflexive and transitive closure of #. We say
that e1 reduces to e2 (in many steps) if e1 # e2 holds.
Given a closed well-typed expression e in #2,G- , we use
|e| for the type erasure of e, that is, the expression obtained
from erasing all types in e. We can then evaluate |e| in a untyped
#-calculus extended with pattern matching. Clearly,
holds if and only if |e| evaluates to |e # |. In other
words, #2,G- supports type-erasure semantics.
2.6 Type Soundness
Given an expression variable context # such that #(x) is
a closed type for each x # dom(#), we write # if - #
derivable for each x #
In general, we write (#) to mean that # :
# is derivable and #] holds. The following lemma
essentially verifies that the rules for deriving judgments of
the form p #) are properly formed.
Lemma 2.4. Assume that #0 # p #) is derivable
holds. If v is a closed value of type #0 ],
that is, - derivable, and we have v # p #
(#) for some # and #, then (#0 ]; #0 ]) holds.
Proof By structural induction on a derivation of #0 # p #
#)
As usual, we need the following substitution lemma to establish
the subject reduction theorem for #2,G- .
Lemma 2.5. Assume that # e : # is derivable. If
#) holds, then - # e[#] is derivable.
Proof By structural induction on a derivation of # e :
# .
Theorem 2.6. (Subject Reduction) Assume that - # e :
# is derivable. If e # e # holds, then - # e # is also
derivable.
Proof Assume that
e1 that reduces to e2 . The proof follows from structural
induction on E. In the case where [], the proof proceeds
by induction on the height of a derivation of -
handling various cases through the use of Lemma 2.5. For
handling the typing rule (ty-case), Lemma 2.4 is needed.
However, we cannot prove that if e is a well-typed non-value
expression then e must reduce to another well-typed
expression. In the case where
case v of ms that is not a redex (because v does not match
any pattern in ms), the evaluation of e becomes stuck. This
is so far the only reason for the evaluation of an expression
to become stuck.
3. IMPLEMENTING OBJECTS
In this section, we briefly outline an approach to implementing
objects through the use of g.r. datatype constructors

3.1
In Section 1, we have noticed a serious problem with the
type OBJ, as it allows no di#erentiation of objects. We
address this problem by providing the type constructor MSG
with another parameter. Given a type # and a class C,
(#)MSG(C) is a type; the intuition is that a message of type
should only be sent to objects in the class C, to
which we assign the type OBJ(C) defined as follows:
First and foremost, we emphasize that a class is not a type;
it is really a tag used to di#erentiate messages. For instance,
we may declare a class IntPairClass and associate with it the
fun newPair x
val
val
fun dispatch MSGgetfst = !xref
| dispatch MSGgetsnd = !yref
| dispatch (MSGsetfst
| dispatch (MSGsetsnd
| dispatch
in dispatch end
withtype {'a,'b}. 'a -> 'b -> OBJ(PairClass('a,'b))

Figure

8: A constructor for pairs
following message constructors of the corresponding types:
MSGgetfst
MSGsetfst
The function newIntPair can now be given the type int #
int # OBJ(IntPairClass). Since anIntPair has the type
OBJ(IntPairClass), anIntPair (MSGfoo) becomes ill-typed
if MSGfoo has a type (1)MSG(C) for some class C that is
not IntPairClass. Although classes can be treated as types
syntactically, we feel it better to treat them as type index
expressions. Following Dependent ML [20, 18], we use class
as the sort for classes. In the following presentation, we assume
the availability of g.r. datatype constructors in DML.
3.2 Parameterized Classes
There is an immediate need for class tags parameterizing
over types. Suppose we are to generalize the monomorphic
function newIntPair into a polymorphic function newPair ,
which can take arguments x and y of any types and then
return an object representing the pair whose first and second
components are x and y, respectively. We need a class
constructor PairClass that takes two given types #1 and #2 ,
and forms a class (#1 , #2)PairClass . We may use some syntax
to declare such a class constructor and associate with it
the following polymorphic message constructors:
MSGgetfst
MSGsetfst
The function newPair for constructing pair objects is implemented
in Figure 9.
3.3 Subclasses
Inheritance is a major issue in object-oriented programming
as it can significantly facilitate code organization and
reuse. We approach the issue of inheritance by introducing
a predicate # on the sort class; given two classes C1
and C2 , C1 # C2 means that C1 is a subclass of C2 . The
type of a message constructor mc is now of the general
form #a#C.(# )MSG(a) or #a#C.#1 #2)MSG(a),
where a # C means that a is of the subset sort {a : class |
a # C}, i.e., the sort for all subclasses of the class C; for
a sequence of types # with the same length as #, mc[# ]
becomes a message constructor that is polymorphic on all
subclasses of therefore, mc can be used to
fun newPair x
val
fun dispatch MSGgetfst = !xref
| dispatch MSGgetsnd = !yref
| dispatch (MSGsetfst
| dispatch (MSGsetsnd
| dispatch
in dispatch end
withtype {'a,'b}. 'a -> 'b -> OBJ(('a,'b)PairClass)
fun newColoredPair c x
val
and
and
fun dispatch MSGgetcolor = !cref
| dispatch (MSGsetcolor
| dispatch MSGgetfst = !xref
| dispatch MSGgetsnd = !yref
| dispatch (MSGsetfst
| dispatch (MSGsetsnd
| dispatch
in dispatch end
withtype {'a,'b}. color -> 'a -> 'b ->

Figure

9: Functions for constructing objects in the
classes PairClass and ColoredPairClass
construct a message for any object tagged by a subclass of
the class C0 . For instance, the message constructors associated
with PairClass are now assigned the types in Figure
10. Suppose we introduce another class constructor
ColoredPairClass , which takes two types to form a class.
Also assume the following, i.e., (#1 , #2 )ColoredPairClass is a
subclass of (#1 , #2)P airClass for any types #1 and #2 :
#)ColoredPairClass #)PairClass
We then associate with ColoredPairClass the message constructors
MSGgetcolor and MSGsetcolor , which are assigned
the types in Figure 10. We can then implement the function
newColoredPair in Figure 9 for constructing colored pairs.
Clearly, the implementation of newColoredPair shares a lot
of common code with that of newPair . We will provide
proper syntax later so that the programmer can e#ciently
reuse the code in the implementation of newPair when implementing
newColoredPair .
3.4 Binary Methods
Our approach to typed object-oriented programming offers
a particularly clean solution to handling binary meth-
ods. For instance, we can declare a class EqClass and associate
with it two message constructors MSGeq and MSGneq
which are given the following types:
Suppose self is an object of type OBJ(C) for some C # Eq.
If we pass a message MSGeq(other ) to self , other is required
to have the type OBJ(C) in order for self (MSGeq(other
to be well-typed. Unfortunately, such a requirement cannot
be enforced by the type system of Java; as a consequence,
MSGgetfst
MSGsetfst
MSGgetcolor : #a #)ColoredPairClass .(color )MSGgetcolor (a)
MSGsetcolor : #a #)ColoredPairClass .color # (1)MSGsetcolor (a)

Figure

10: Some message constructors and their types
type downcasts are often needed for implementing and testing
equality on objects.
3.5 The Self Type
Our approach also o#ers a particularly clean solution to
handling the notion of self type, namely, the type of the receiver
of a message. Suppose we want to support a message
MSGcopy that can be sent to any object to obtain
a copy of the object. 3 . We may assume MSGcopy is a
message constructor associated with some class ObjClass
and C # ObjClass holds for any class C. We can assign
MSGcopy the following type to indicate that the returned
object is in the same class as the object to which the message
is sent.
If this is done in Java, all we can state in the type system
of Java is that an object is to return another object after
receiving the message MSGcopy. This is imprecise and is a
rich source for the use of type downcasting.
3.6 Inheritance
Inheritance is done in a Smalltalk-like manner, but there is
some significant di#erence. We now use a concrete example
to illustrate how inheritance can be implemented. This is
also a proper place for us to introduce some syntax that
is designed to facilitate object-oriented programming. We
use the following syntax to declare a class ObjClass and a
message constructor MSGcopy of the type:
Note selfType is merely syntactic sugar here.
class ObjClass {
MSGcopy: selfType => self;
In addition, the syntax also automatically induces the definition
of a function superObj, which is written as follows in
ML-like syntax.
(* self is just an ordinary variable *)
fun dispatch MSGcopy = self
| dispatch
in dispatch end
withtype {a <: ObjClass} OBJ(a) -> OBJ(a)
The function superObj we present here is solely for explaining
how inheritance can be implemented; such a function is
3 It is up to the actual implementation as to how such a copy
can be constructed.
not to occur in a source program. The type of the function
#a # ObjClass.OBJ(a) # OBJ(a) indicates this is a
function that takes an object tagged by a subclass C of
ObjClass and returns an object tagged by the same class.
In general, for each class C, a "super" function of type
#a # C.OBJ(a) # OBJ(a) is associated with C. It should
soon be clear that such a function holds the key to implementing
inheritance. Now we use the following syntax to
declare classes Int1Class and ColoredInt1Class as well as
some message constructors associated with them.
class Int1Class inherits ObjClass {
MSGget_x: int;
MSGset_x (int): unit;
MSGdouble: unit =>
class ColoredInt1Class inherits Int1Class {
(* color is just some already defined type *)
MSGget_c:
MSGset_c
The "super" functions associated with the classes Int1Class
and ColoredInt1Class are automatically induced as follows.
fun dispatch MSGdouble =
| dispatch
in dispatch end
withtype {a <: Int1Class} OBJ(a) -> OBJ(a)
fun dispatch
in dispatch end
withtype {a <: ColoredInt1Class} OBJ(a) -> OBJ(a)
The functions for constructing objects in the classes Int1Class
and ColoredInt1Class are implemented in Figure 11. There
is something really interesting here. Suppose we use newInt1
and newColoredInt1 to construct objects o1 and o2 that are
tagged with Int1Class and ColoredInt1Class , respectively.
If we send the message MSGcopy to o1 , then a copy of o1
(not o1 itself) is returned. If we send MSGdouble to o2 ,
then the integer value of o2 is doubled as it inherits the
corresponding method from the class Int1Class . What is
remarkable is that the object o2 itself is returned if we send
the message MSGcopy to o2 . The reason is that no copying
method is defined for o2 ; searching for a copying method,
eventually finds the one defined in the class ObjClass
(as there is no such a method defined in either the class
ColoredInt1Class or the class Int1Class). This is a desirable
consequence: if o2 were treated as an object in the
fun newInt1 (x0:
val
fun dispatch
| dispatch (MSGset_x
| dispatch MSGcopy = newInt1 (!x)
| dispatch dispatch msg
in dispatch end
withtype int -> OBJ(Int1Class)
fun newColoredInt1 (c0: color, x0:
val
fun dispatch
| dispatch (MSGset_c
| dispatch
| dispatch (MSGset_x
| dispatch dispatch msg
in dispatch end
withtype int -> OBJ(ColoredInt1Class)

Figure

11: Functions for constructing objects in
Int1Class and ColoredInt1Class
class Int1Class (through either F-bounded polymorphism or
match-bounded polymorphism), the returned object would
be in the class Int1Class , not in the class ColoredInt1Class ,
as it would be generated by newInt1 (o2(MSGget x)), making
the type system unsound. We are currently not aware
of any other approach to correctly typing this simple exam-
ple. Note that the function newInt becomes ill-typed if we
employ the notion MyType here.
3.7 Subtyping
There is not an explicit subtyping relation in our ap-
proach. Instead, we can use existentially quantified dependent
types to simulate subtyping. For instance, given a class
tag C, the type #a#C.OBJ(a) is the sum of
all types OBJ(a) satisfying a # C. Hence, for each C1 # C,
OBJ(C1 ) can be regarded as a subtype of OBJECT(C) as
each value of the type OBJ(C1) can be coerced into a value
of the type OBJECT(C). As an example, the type
OBJ((OBJECT(EqClass),OBJECT(EqClass))PairClass)
is for pair objects whose both components support equality
test.
4. RELATED WORK AND CONCLUSION
Our work is related to both intentional polymorphism and
type classes.
There have already been a rich body of studies in the literature
on passing types at run-time in a type-safe manner [11,
10, 17]. Many of such studies follow the framework in [13],
which essentially provides a construct typecase at term level
to perform type analysis and a primitive recursor Typerec
type names at type level to define new type construc-
tors. The language # ML
in [13] is subsequently extended
to #R in [11] to support type-erasure semantics. The type
constructor R in #R can be seen as a special g.r. datatype
constructor.
The system of type classes in Haskell provides a programming
methodology that is of great use in practice. A
common approach to implementing type classes is through
dictionary-passing, where a dictionary is essentially a record
of the member functions for a particular instance of a type
class [1]. We encountered the notion of g.r. datatype constructors
when seeking an alternative implementation of type
classes through intensional polymorphism. An approach to
implementing type classes through the use of g.r. datatype
constructors can be found at [19].
The dependent datatypes in DML [20, 18] also shed some
light on g.r. datatype constructors. For instance, we can
have the following dependent datatype declaration in DML.
datatype 'a list with
| {n:nat} cons(n+1) of 'a * 'a list(n)
The syntax introduces a type constructor list that takes a
type and a type index of sort nat to form a list type. The
constructors nil and cons are assigned the following types.
cons
Given a type # and natural number n, the type (# )list(n) is
for lists with length n in which each element has the type # .
Formally, the type constructor list can be defined as follows:
clearly, this is also a form of guarded datatype constructor,
where the guards are constraints on type index expressions
(rather than on types).
Our notion of objects in this paper is largely taken from
Smalltalk [12], for which a particularly clean and intuitive
articulation can be found in [14]. The literature on types
in object-oriented programming is simply too vast for us to
give an even modestly comprehensive overview of the related
work. Please see [5] for references. Instead, we focus on
some closely related work that either directly influences or
motivates our current work.
Bounded polymorphism [8, 6] essentially imposes subtyping
restrictions on quantified type variables. For instance,
suppose we want to implement a class for ordered sequences.
In order to insert an element into a sequence, we must compare
it with other elements in the sequence. Therefore, we
should only insert elements of a class that provide the appropriate
methods for comparison. This can be achieved
through bounded polymorphism.
F-bounded polymorphism [7], which generalizes the simple
bounded polymorphism, was introduced to handle some
complex issues such as typing binary methods in object-oriented
programming. It has since been adopted in the
design of GJ [2], helping to significantly increase the expressiveness
of the type system of Java. However, F-bounded
polymorphism does not seem to interact well with the sub-class
relation (e.g., please see the example on page 59 [5]).
Matching-bounded polymorphism is similar to bounded
polymorphism. The main di#erence is that matching constraints
are imposed on quantified type variables instead
of subtyping constraints. The notion of MyType [4] essentially
refers to the type of the receiving object of a mes-
sage. With match-bounded polymorphism, the notion of
MyType can allow the possibility of dispensing with most of
the uses of F-bounded polymorphism. The language in [4]
is really a state-of-the-art object-oriented programming language
(when static typing is concerned). This work is carried
further in [3], where imperative features are introduced. The
type system that we are to design shares many common features
with the work in [4], though we employ a completely
di#erent type-theoretical approach. In particular, we intend
to not only simplify the notion of MyType but also make it
more e#ective in capturing program invariants.
Currently, we are particularly interested in implementing
a CLOS-like object system on the top of DML extended with
g.r. datatype constructors, facilitating object-oriented programming
styles in a typed functional programming setting.
5.



--R

Implementing Haskell overloading.
Making the future safe for the past: Adding genericity to the Java programming language.

A paradigmatic object-oriented programming language: design
Foundations of Object-Oriented Languages
A modest model of records

On understanding types
A formulation of the simple type theory of types.
Flexible Type Analysis.
Intensional polymorphism in type-erasure semantics

Compiling polymorphism using intensional type analysis.

The Definition of Standard ML (Revised).
Computation and Deduction.
Fully Reflexive Intensional Type Analysis.
Dependent Types in Practical Programming.
Guarded Recursive Datatype Constructors
Dependent types in practical programming.
--TR
Smalltalk-80: the language and its implementation
On understanding types, data abstraction, and polymorphism
F-bounded polymorphism for object-oriented programming
Implementing Haskell overloading
Compiling polymorphism using intensional type analysis
Smalltalk, objects, and design
Making the future safe for the past
Intensional polymorphism in type-erasure semantics
Dependent types in practical programming
Flexible type analysis
Foundations of object-oriented languages
The Definition of Standard ML
Dependent types in practical programming
dependent types;DML;object-oriented