Seeking Grace: A new object-oriented language for novices Andrew P. Black, Kim B. Bruce, Michael Homer, James Noble, Amy Ruskin, and Richard Yannow. Proceedings of SIGCSE Computer Science Education 2013. ACM, New York, NY, USA, 2013, pp. 129-134. pdf
Abstract We are designing a new object-oriented language, Grace, whose target audience is novices. Grace is intended to integrate proven new ideas in programming languages into a conceptually simple language that allows the instructor and students to focus on the essential complexities of program- ming, while supporting a variety of approaches to teaching.
Abstract Object orientation and pattern matching are often seen as conflicting approaches to program design. Object-oriented programs place type-dependent behavior inside objects and invoke it via dynamic dispatch, while pattern-matching programs place type-dependent behavior outside data structures and invoke it via multiway conditionals (case statements). Grace is a new, dynamic, object-oriented language designed to support teaching: to this end, Grace needs to support both styles. We explain how this conflict can be resolved gracefully: by modelling patterns and cases as partial functions, reifying those functions as objects, and then building up com- plex patterns from simpler ones using pattern combinators. We describe the implementation of this design as an object-oriented framework, and a case study of its effectiveness.
Abstract We are engaged in the design of a small, simple program- ming language for teaching novices object-oriented programming. This turns out to be far from a small, simple task. We focus on three of the problems that we encountered, and how we believe we have solved them. The problems are (1) gracefully combining object initialization, inheritance, and immutable objects, (2) reconciling apparently irreconcilable views on type-checking, and (3) providing a family of languages, each suitable for students at different levels of mas- tery, while ensuring conceptual integrity of their designs. In each case our solutions are based on existing research; our contribution is, by design, consolidation rather than innovation.
A History of the Liberal Arts Computer Science Consortium and its Model CurriculaACM Transactions on Computing Education (TOCE), 2010
Journal of Semantics. 27 (2010), pp. 81--118. Preprint available. Also pdf file of draft version.
Abstract The aim of this paper is to capture the similarities and differences between assertions and polar questions so as to be able to account for the systematic partial overlap that exists in reactions to these speech acts in English and beyond. We first discuss the discourse components we assume, and then define default assertions and default polar questions in a way that allows us to characterize two types of responses to these speech acts, confirming and reversing reactions. The common characteristics of assertions and polar questions are responsible for the fact that both allow these reactions; the differences between the two speech acts explain the different contextual effects confirming and reversing moves have depending on whether they react to an assertion or a polar question. We then examine the distribution of a set of 'polarity' particles in Romanian in terms of the notions defined in the rest of the paper, and end with a series of predictions concerning polarity particles across languages.
Extended abstract. Proceedings of ECOOP 2004. LNCS 3086, Springer-Verlag, pp. 390-414, 2004. pdf file.
Abstract LOOJ is an extension of Java obtained by adding bounded parametric polymorphism and new type expressions ThisClass and ThisType, which are similar to MyType in LOOM. Through examples we demonstrate the utility of this language even over very expressive extensions such as GJ. The LOOJ compiler generates standard JVML code and supports instanceof and casts for all types including type variables and the other new type expressions. The core of the LOOJ type system is sound, as demonstrated by a soundness proof for an extension of Featherweight GJ. This paper also highlights difficulties that arise from the use of both classes and interfaces as types in Java.
Extended abstract. Electronic Notes in Theoretical Computer Science 82, no. 8 (2003). Last revised 6/2003. pdf file.
Abstract In this paper we discuss some of the remaining problems in the design of static type systems for object-oriented programming languages. We look at typing problems involved in writing a simple interpreter as a good example of a simple problem leading to difficult typing issues. The difficulties encountered seem to arise in situations where a programmer desires to simultaneously refine mutually interdependent classes and object types.
by Kim B. Bruce and Joseph Vanderwaart
Proceedings of MFPS '99. Electronic Notes in Theoretical Computer Science, 82(8), 29 pages. Last revised 2/25/99. dvi file, postscript
Abstract The virtual class construct was first introduced in the language Beta to provide added expressiveness when used with inheritance. Unfortunately, the virtual class construct in Beta is not statically type-safe. In this paper we show how a generalization of the semantics of object-oriented languages with a MyType construct leads to a variant of virtual classes which needs no run-time checks. This results in an object-oriented language in which both parametric types and virtual classes (or types) are well-integrated, and which is statically type-safe.
Keywords: Language design, semantics, virtual classes, parametric polymorphism, static type checking
by Kim B. Bruce, Leaf Petersen, and Joseph Vanderwaart.
Extended abstract submitted to OOPSLA98. Last revised 4/13/98. dvi file, postscript
Abstract Pure object-oriented languages have tended to assume that classes can take the place of modules in programming in the large. We argue that modules are still needed in these languages and present the design of a module construct for our language LOOM which works well with the object-oriented paradigm. We discuss and illustrate the advantages of these modules over a class-only approach. In particular we illustrate the advantages of modules in supporting better control over information hiding, including the support of access like C++'s friends.
Keywords: Language design, modules.
by Kim B. Bruce, Martin Odersky, and Philip Wadler
ECOOP '98 Proceedings, LNCS 1445. pp 523-549. Last revised 4/1/98. dvi file, postscript
Abstract Parametric types and virtual types have recently been proposed as extensions to Java to support genericity. In this paper we investigate the strengths and weaknesses of each. We suggest a variant of virtual types which has similar expressiveness, but supports safe static type checking. This results in a language in which both parametric types and virtual types are well-integrated, and which is statically type-safe.
Keywords: Language design, virtual types, parametric polymorphism, static type checking
by Kim B. Bruce
Draft. dvi file, postscript
Abstract This paper proposes some relatively minor additions to Java's syntax and semantics in order to increase the expressiveness of the language with little cost in semantic complexity. No changes are suggested that would invalidate or change the semantics of programs written in the current version of Java.
While the main point of the language extensions are to support parametric polymorphism, we also added features which provide better support for binary methods, a kind of method that is often difficult to support in a statically typed language. (See \cite{BinMeth} for an extensive discussion of the difficulties of statically type-checking binary methods.)
Briefly, the changes proposed are to add a ``ThisType' construct to represent the type of ``this'' (the name of the object executing a method), to provide a mechanism for the programmer to specify that a variable hold values of exactly the type given (and not a type that extends it), to reinterpret ``extends'' as ``matching'' rather than ``subtyping'', and to add a form of constrained polymorphism which depends on matching.
Category: Language design
by Kim B. Bruce
Draft. dvi file, postscript
Abstract Virtual classes, which were first used in Beta \cite{VirtClass}, have recently been suggested by Thorup \cite{Thorup} as an extension to Java to support genericity. While virtual classes are a convenient mechanism to support simultaneous modification of mutually recursive classes, they rely on dynamic type checking for type safety. We suggest a variant which has similar expressiveness as virtual classes, but supports safe static type checking. To ease the comparison with earlier work we express our construct as an addition to Java, though similar constructs may be added to a variety of object-oriented languages. For example, this proposal can also be seen as a statically type-safe alternative to Eiffel's ``anchored types''.
Category: Language design
Information and Computation 155(1999), pp 108-133 : comp.dvi, comp.ps, 23 pp.
ABSTRACT
Recent years have seen the development of several foundational
models for statically typed object-oriented programming. But despite
their intuitive similarity, differences in the technical machinery
used to formulate the various proposals have made them difficult to
compare.
Using the typed lambda-calculus \FOMEGASUB{} as a common basis, we now offer a detailed comparison of four models: (1) a recursive-record encoding similar to the ones used by Cardelli \cite{Cardelli88}, Reddy \cite{Reddy88->KaminReddy94,KaminReddy94}, Cook \cite{Cook89,CookCH90}, and others; (2) Hofmann, Pierce, and Turner's existential encoding \cite{PTSimple,HofmannPierce94}; (3) Bruce's model based on existential and recursive types \cite{Bruce92}; and (4) Abadi, Cardelli, and Viswanathan's type-theoretic encoding \cite{AbCardV} of a calculus of primitive objects.
Categories: Semantics, Foundations of object-oriented languages.
Extended abstract appeared in ECOOP '97 Proceedings, LNCS 1241, Springer-Verlag, pp. 104-127: LOOM.dvi, LOOM.ps, 24 pp.
ABSTRACT
We present the design and rationale of a new
statically-typed object-oriented language, LOOM. LOOM retains most
of the features of the earlier language PolyTOIL. However the
subtyping relation is dropped from LOOM in favor of the matching
relation. ``Hash types'', which are defined in terms of matching,
are introduced to provide some of the benefits of subtyping.
These types can be used to provide support for heterogeneous
data stuctures in LOOM. LOOM is considerably simpler than PolyTOIL, yet
the language is just as expressive. The type system for the language
is decidable and provably type safe. The addition of modules to the
language provides better control over information hiding and allows
the provision of access like that of C++'s friends.
Categories: Type systems and language design for object-oriented languages.
Technical report: Static.dvi, Static.ps,33 pp, Lecture notes (postscript).
ABSTRACT
While simple static-typing disciplines exist for object-oriented
languages like C++, Object Pascal, and Modula-3, they are often so
restrictive that programmers are forced
to by-pass the type system with type casts. Other languages allow more
freedom, but require run-time checking to pick up the type errors that
their more permissive systems missed.
This paper consists of a survey of problems (illustrated by a series of sample programs) with existing type systems, and suggests ways of improving the expressibility of these systems while retaining static type safety. In particular we will discuss the motivations behind introducing "MyType", "matching", and "bounded matching" into these type systems.
We also suggest a way of simplifying the resulting type system by replacing subtyping by a type system with a new type construct based on matching. Both systems provide support for binary methods, which are often difficult to support in statically-typed languages.
The intent is to avoid pages of type-checking rules and formal proofs, but instead explain why the problems are interesting via the series of sample programs. The technical details (including proofs of subject reduction and type safety) are available elsewhere.
Categories: Type systems for object-oriented languages.
PolyTOIL: A type-safe polymorphic object-oriented languageACM Transactions on Programming Languages and Systems (TOPLAS), 2003
In this paper we present the design of PolyTOIL, a provably type-safe polymorphic object-oriented programming language. PolyTOIL is designed to be significantly more expressive than statically-typed languages like C++. Innovative features include The proof of type safety is obtained with the aid of a subject reduction theorem which ties together the type-checking rules with a (natural) operational semantics. The proof of subject reduction may be of independent interest in that it applies to an environment-based natural semantics for a polymorphic language.
Categories: Type systems, design and semantics of object-oriented languages.
Theory and Practice of Object Systems, 1(1995), pp. 221-242. binary.dvi , binary.ps
ABSTRACT
Giving types to binary methods causes significant problems for
object-oriented language designers and programmers. This paper offers
a comprehensive description of the problems arising from typing binary
methods, and collects and contrasts diverse views and solutions.
It summarizes the current debate on the problem of binary
methods for a wide audience.
Technical Report TOILwPf.dvi
ABSTRACT
In \cite{BrPOPL93}, the first author introduced the language
TOOPLE, a statically-typed functional object-oriented programming language
which has a number of desirable properties. In this and a series of other
papers (\cite{Bruce92,BCDMMG,BrCrKan}), the denotational and natural
semantics of TOOPLE have been presented and shown to be relatively consistent,
subject-reduction and type-safety have been proven,
and the type-checking problem has been shown to be decidable.
In this paper we introduce TOIL, a statically-typed object-oriented imperative language, which is based on the same semantic principles as TOOPLE and shares many of the same desirable properties. We include type-checking rules, an operational semantics, and prove a subject-reduction theorem for TOIL, showing that the operational semantics is type-safe.
This paper is an application of the theoretical work on the semantics of object-oriented programming languages done over the last decade to the design of real object-oriented programming languages.
Journal of Functional Programming 4(1994), pp. 127-206: ObjDesign.dvi, ObjDesign.ps
ABSTRACT
In order to illuminate the fundamental concepts involved in object-oriented
programming languages, we describe the design of TOOPL, a paradigmatic
statically-typed functional object-oriented programming language
which supports classes, objects, methods, hidden instance variables,
subtypes, and inheritance.
It has proven to be quite difficult to design such a language which does not contain holes in the type system. A particular problem with statically type checking object-oriented languages is designing type-checking rules which ensure that methods provided in a superclass will continue to be type correct when inherited in a subclass. The type checking rules for TOOPL have this feature, enabling library suppliers to provide only the interfaces of classes with actual executable code, while still allowing users to safely create subclasses.
The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a model of the F-bounded second-order lambda calculus with fixed points at both the element and type level. This semantics supported the language design by providing a means to prove that the type checking rules are sound, providing a guarantee that the language is type-safe.
While the semantics of our language is rather complex, involving fixed points at both the element and type level, we believe that this reflects the inherent complexity of the basic features of object-oriented programming languages. Particularly complex features include the implicit recursion inherent in the use of the keyword, self, to refer to the current object, and its corresponding type, MyType. The notions of subclass and inheritance introduce the greatest semantic complexities, whereas the notion of subtype seems relatively straightforward.
OOPSLA '93 proceedings, pp. 29-46. OOPSLA.dvi
ABSTRACT
Over the last several years, much interesting work has been done in modelling
object-oriented programming languages in terms of extensions of the bounded
second-order lambda calculus, $F_{\le}$. Unfortunately, it has recently been
shown by Pierce (\cite{Pierce92}) that type checking $F_{\le}$ is undecidable.
Moreover he showed that the undecidability arises in the seemingly simpler
problem of determining whether one type is a subtype of another.
In \cite{Bruce92,BrPOPL93}, the first author introduced a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variables, subtypes, and inheritance. The semantics of TOOPL is based on $F_{\le}$, so the question arises whether type checking in this language is decidable.
In this paper we show that type checking for TOOPLE, a minor variant of TOOPL (Typed Object-Oriented Programming Language), is decidable. The proof proceeds by showing that subtyping is decidable, that all terms of TOOPLE have minimum types (which are in fact computable), and then using these two results to show that type checking is decidable. Interestingly, conditional statements introduce significant problems which necessitated the computation of generalized least upper bounds of types. The interaction of the least upper bounds with the implicit recursion in object and class definitions and the contravariant nature of function spaces makes the computation of appropriate least upper bounds more subtle than might be expected. Our algorithm fails to be polynomial in the size of the term because the size of the type of a term can be exponential in the size of the term. Nevertheless, it performs well in practice.
This paper concentrates on the language without instance variables, though the results can be extended to the full language, at the cost of some added complexity.
Proceedings of MFPS '93, LNCS 802, Springer-Verlag, 1994, pp. 603-626. TPLNatSem.dvi
ABSTRACT
In this paper we present an operational semantics for the language
TOOPLE, a statically-typed, functional, object-oriented programming language
which has a number of desirable properties.
The operational semantics, given in the form of a natural semantics, is
significantly simpler than the previous denotational semantics for the
language. A ``subject reduction'' theorem for the natural semantics provides
a proof that the language is type-safe. We also show that the natural
semantics is consistent with the denotational semantics of the language.
Proc ACM Symp. Principles of Programming Languages, 1993, pp. 285-298: TCPOPL.dvi
ABSTRACT
In this paper we introduce a statically-typed, functional, object-oriented
programming language, TOOPL, which supports classes, objects, methods, instance
variables, subtypes, and inheritance.
It has proved to be surprisingly difficult to design statically-typed object-oriented languages which are nearly as expressive as SmallTalk and yet have no holes in their typing systems. A particular problem with statically type checking object-oriented languages is determining whether a method provided in a superclass will continue to type check when inherited in a subclass. This problem is solved in our language by providing type checking rules which guarantee that a method which type checks as part of a class will type check correctly in all legal subclasses in which it is inherited. This feature enables library providers to provide only the interfaces of classes with executables and still allow users to safely create subclasses.
The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a sufficiently rich model of the F-bounded second-order lambda calculus. This semantics supported the language design by provided a means of proving that the type-checking rules for the language are sound, ensuring that well-typed terms produce objects of the appropriate type. In particular, in a well-typed program it is impossible to send a message to an object which lacks a corresponding method.
Proceedings of POPL '92, pp. 316-327: BrMitPOPL.dvi
ABSTRACT
We relate standard techniques for solving recursive domain
equations to previous models with types interpreted as partial
equivalence relations (per's) over a $D_\infty$ lambda model.
This motivates a particular choice of type functions,
which leads to an extension of such models to higher-order polymorphism.
The resulting models provide natural interpretations for
function spaces, records, recursively defined types, higher-order type
functions, and bounded polymorphic types forall X <: Y. A where the bound
may be of a higher kind. In particular, we may combine recursion
and polymorphism in a way that allows the bound Y in forall X <: Y. A
to be recursively defined. The model may also be used to interpret so-called
F-bounded polymorphism. Together, these features allow us to represent
several forms of type and type functions that seem to
arise naturally in typed object-oriented programming.
Proceedings of the MFPS '91 Conference, pp. 102-124: inherit.dvi
ABSTRACT
A simple language is presented which supports inheritance in
object-oriented languages. Using this language, the definitions for
the semantics of inheritance given in \cite{CookCH90} and \cite{MitchPOPL90}
are compared and shown to be equivalent. The equivalence is shown
by presenting and comparing two denotational semantics of the simple
language which capture the essence of each of the earlier semantics.
by Kim B. Bruce
Extended abstract. SIGCSE 99, pp 331-335. SIGCSEPL.ps.gz, SIGCSEPL.dvi.gz
ABSTRACT
It is unfortunate that in most computing curricula, the uses of
theory and formalisms are limited to the algorithms and theory of computation
courses. In fact, as indicated in the ``Logic in Computer
Science'' panel BKLV98 in SIGCSE `97, logic and logic-related
formalisms can play important parts of a wide variety of courses.
In this paper we explain how logic-based ideas involving formal
operational semantics and
type-checking rules can play an important role in upper-level
principles of programming languages courses.
Education and Computing, 7(1991), pp. 23-42 IFIPCurric.ps.gz, IFIPCurric.dvi.gz
ABSTRACT
In 1988 the ACM and the IEEE Computer Society formed a Joint Curriculum Task
Force to create a new model curriculum to replace Curriculum '88. Three
years later the committee produced the report, titled Computing Curricula' 91.
In this paper we discuss informally some of the considerations involved
in creating the curriculum report, with the hopes that this will be helpful
to anyone interested in implementing a curriculum in Computer Science based
on the Task Force's report.
by Kim B. Bruce, Charles Keleman, and Allen Tucker.
ITICSE Proceedings, pp. 132-135 iticse.pdf.gz, ABSTRACT
We are concerned about a view in undergraduate computer science education, especially in the early courses, that it's okay to be math-phobic and still prepare oneself to become a computer scientist. Our view is the contrary: that any serious study of computer science requires students to achieve mathematical maturity (especially in discrete mathematics) early in their undergraduate studies, thus becoming well-prepared to integrate mathematical ideas, notations, and methodologies throughout their study of computer science. A major curricular implication of this theme is that the prerequisite expectations and conceptual level of the first discrete mathematics course should be the same as it is for the first calculus course -- secondary school pre-calculus and trigonometry. Ultimately, calculus, linear algebra, and statistics are also essential for computer science majors, but none should occur earlier than discrete mathematics. This paper explains our concerns and outlines our response as a series of examples and recommendations for future action.
by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
SIGCSE 2001 Proceedings, pp 6-10. SIGCSE2001Lib.dvi.gz, SIGCSE2001Lib.ps.gz, SIGCSE2001Lib.pdf, ABSTRACT
In this paper we describe a library we have developed that supports an ``OO-from-the-beginning'' approach to CS 1. The design of interactive graphical programs helps students to both use objects and write methods early while designing and implementing interesting programs. The use of real graphics ``objects'' and event-driven programming are important components of this approach.
by Kim B. Bruce, Charles Keleman, and Allen Tucker.
SIGCSE 2001 Proceedings, pp. 243-247. SIGCSE2001MathPhobic.dvi.gz, SIGCSE2001MathPhobic.ps.gz, ABSTRACT
The paper \cite{Kelemen2000} argued that mathematical ideas play an important role in the computer science curriculum, and that Discrete Mathematics needs to be taught early in the computer science curriculum. In this follow-up paper, we present evidence that computer science curricula are drifting away from a fundamental commitment to theoretical and mathematical ideas. We propose some actions that can be taken to help reverse this drift.
ITiCSE 2001 proceedings, pp. 1-4. eventsREZ.pdf ABSTRACT
We have recently designed a CS 1 course that integrates event-driven programming from the very start. Our experience teaching this course runs counter to the prevailing sense that these techniques would add complexity to the content of CS 1. Instead, we found that they were simple to present and that they also simplified the presentation of other material in the course. In this paper, we explain the approach we used to introduce event-driven methods and discuss the factors underlying our success.
Proceedings of 2004 OOPSLA Educator's symposium, OOPSLA '04 companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications pp 96-100. Last revised 7/2004.
event2.pdf
ABSTRACT
We have designed a CS 1 course that integrates event-driven programming from the very start. In earlier papers we argued that event-driven programming is simple enough for CS 1 when introduced with the aid of a library that we have developed. In this paper we argue that early use of event-driven programming makes many of the standard topics of CS 1 much easier for students to learn by breaking them into smaller, more understandable concepts.
by Kim B. Bruce
Inroads (newsletter of SIGCSE), December, 2004 Last revised, 11/04
Inroads.pdf
ABSTRACT
A discussion took place on the SIGCSE mailing list in late March of 2004 that raised important issues on how to teach introductory courses using Java. This article attempts to summarize several of the important points raised during this discussion, among them whether or how objects should be taught early or late in a CS 1 course, or indeed whether object-oriented languages should be postponed until a second course.
by Kim B. Bruce, Scot Drysdale, Charles Kelemen, and Allen Tucker
CACM, September, 2003 pp. 41-44.
WhyMath.pdf
(C) ACM, 2003. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in CACM, Volume 46, Issue 9 (September 2003), pp. 40-44
ABSTRACT
The mathematical thinking, as well as the mathematics,
in a computer science education prepares students for all stages
of system development, from design to the
correctness of the final implementation.
by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
Proceedings of the 2005 ACM Symposium on Computer Science Education, pp. 246-250, 2005.
p266-bruce.pdf
ABSTRACT
The approach to teaching recursion in introductory programming
courses has changed little during the transition
from procedural to object-oriented languages. It is still common
to present recursion late in the course and to focus on
traditional, procedural examples such as calculating factorials
or solving the Towers of Hanoi puzzle. In this paper,
we propose that the shift to object-oriented programming
techniques calls for a significant shift in our approach to
teaching recursion. First, we argue that in the context of
object-oriented programming students should be introduced
to examples of simple recursive structures such as linked lists
and methods that process them, before being introduced to
traditional procedural examples. Second, we believe that
this material should be presented before students are introduced
to structures such as arrays. In our experience,
the early presentation of recursive structures provides the
opportunity to reinforce the fundamentals of defining and
using classes and better prepares students to appreciate the
reasons to use classes to encapsulate access to other data
structures when they are presented.
by Liberal Arts Computer Science Consortium.
J. Educ. Resour. Comput. 7, 2 (Jun. 2007)
LACS_JERIC.pdf
(C) ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in J. Educ. Resour. Comput. 7, 2 (Jun. 2007)