A Practical Gradual Type System For Smalltalk

Gradualtalk is a gradually-typed Smalltalk, which is fully compatible with existing Smalltalk code. Following the philosophy of Typed Racket, a major design goal of Gradualtalk is for the type system to accomodate existing programming idioms in order to allow for an easy, incremental path from untyped to typed code. The design of Gradualtalk was guided by a study of existing Smalltalk projects, and incrementally typing them in Gradualtalk.

The type system of Gradualtalk supports as many Smalltalk idioms as possible through a number of features: a combination of nominal and structural types, union types, self types, parametric polymorphism, and blame tracking, amongst others.

Gradualtalk team: Esteban Allende, Oscar Callaú, Johan Fabry, Éric Tanter

Kind of Types

These are the different kinds of types that the typing system supports. For each kind, one example is provided.

  • Nominal: String
  • Nominal metaclass: Integer class
  • Dynamic type: ?
  • Self: Self
  • Instances of self: Self instance
  • Class of self: Self class
  • Lambdas (or Blocks): Integer Integer → Integer
  • Structural type: {x (→Number). y (→Number) }
  • Bounded structural type: Morph{changeColor: (Color → Self)}
  • Parametric type: A
  • Nominal parametrized: Dictionary<Symbol, Integer>
  • Self parametrized: Self<Integer>
  • Union type: String | Integer

However the types are only a half of the story, using them is the another half. Gradualtalk allows programmers to use these types in any place where declaring a variable or typing an expression is need. Quick Reference refers to these with several examples.

Download

There are two images to download:

  • gradualtalk.zip: The basic image of the Gradual Type System
  • gradualtalk-typedkernel.zip: Has the same functionalities that the basic image, but additionally some kernel classes and the type system has been typed.

We recommend using the latest PharoVM.

As examples, we include some typed projects, available for download:

Publications

These are the research publications related with Gradualtalk:

Quick Reference

Activating the Type System

The type system is optional and by default it is deactivated. The reason for this is that most packages in the Pharo VM are untyped. Activating Gradualtalk by default will lead to an unnecessary agglomeration of implicit casts.

To activate the type system in a given class (and all its subclasses), the TTyped trait needs to be added to the class like this:

Object subclass: #Point
	uses: TTyped
	instanceVariableNames: 'x y'
	classVariableNames: ''
	poolDictionaries: ''
	category: 'Tutorial'

Typing Language Entities

The following are a series of example to typing language entities, such as methods, variables, blocks, etc.

Typing a method declaration

(Number) distanceTo: (Point) p
  ^ ((self x - p x) squared + (self y - p y) squared) sqrt

Typing local variables

(Number) distanceTo: (Point) p
  |(Number) dx (Number) dy|
  dx := (self x - p x).
  dy := (self y - p y).
  ^ ( dx squared + dy squared) sqrt

Typing block variables

(Number) distanceTo: (Point) p
  |(Number Number -> Number) block|
  block := [:(Number)dx :(Number)dy| ( dx squared + dy squared) sqrt].
  ^ block value: (self x - p x) value:  (self y - p y).

Typing instance variables

Object subclass: #Point
	uses: TTyped
	instanceVariableNames: '(Integer)x (Integer)y'
	classVariableNames: ''
	poolDictionaries: ''
	category: 'Tutorial'

Parametric Polymorphism

Declaring class parametric types

Object subclass: #Point
	uses: TTyped
        parametricVariableNames: 'N'
	instanceVariableNames: '(N)x (N)y'
	classVariableNames: ''
	poolDictionaries: ''
	category: 'Tutorial'

Multiple parametric variables can be defined in a class. Their order in the definition is important.

Object subclass: #Dictionary
	uses: TTyped
        parametricVariableNames: 'K V'
	instanceVariableNames: '...'
	classVariableNames: ''
	poolDictionaries: ''
	category: 'Tutorial'

With this definition, Dictionary<String, Integer> would define that K=String and V=Integer. Type variables for ancestor classes are superseeded by default when declaring new parametric variables.

Redefining old class parametric types

When declaring new type variables in a class where its ancestor has type variables, the old type variables maintain their old significance. However, this may not be the desired effect. Using 'oldParametricVariablesAs' allows to redefine them as necessary.

ArrayedCollection subclass: #String
	parametricVariableNames: ''
	oldParametricVariablesAs: 'E := Character'
	instanceVariableNames: ''
	classVariableNames: '...'
	poolDictionaries: ''
	category: 'Collections-Strings'

Upperbounding class parametric types

Object subclass: #Point
	uses: TTyped
        parametricVariableNames: 'N <: Number'
	instanceVariableNames: '(N)x (N)y'
	classVariableNames: ''
	poolDictionaries: ''
	category: 'Tutorial'

Upperbounding method parametric types

True >> (A) & (A) aBoolean
	<whereType: 'A <: Boolean'>
	^aBoolean

Other features

Explicit Casts

(SmallInteger) smallX
  ^ (<SmallInteger> self x) "parenthesis are not optional"

Type aliasing

ProtoObject asType addAlias: #Any

addAlias: is a common method between Type objects that its supported by all types except Self, Dyn and Parametric types. For the moment, Type objects must be generated manually.

Runtime casts

By default, method instrumentation and runtime casts are enabled. However in some cases, programmers do not want to worry about method instrumentation and runtime casts, eg. type annotations are only a checked documentation of the project. Because of this, we include the ability to disable runtime casts:

Gradualtalk configuration enableInstrumentation: false.
Gradualtalk configuration enableCasts: false.

Then, recompile the code that you want to be free of method instrumentation and runtime casts.

The type system performs blame tracking to appropriately blame the wrong expressions. For higher-order casts, the blame tracking is lazy and only blames downcasts (casts from dyn to concrete types). This means that cast errors are detected only when the block is invoked and downcasts are wholly responsible for potential errors.

Tool Support

Performing a full type check

Because of the dynamic nature of the system, it is possible to bring the system in an inconsistent state with regards to the types declared on the methods. This will typically manifest itself when filing in code that has been inconsistently typed. To avoid this problem, we recommend performing a full type check regularly, or at least on the code that will be filed out. To perform this, do the following:

TypeSystem typeCheckCategory: <categoryname>

Exporting and Importing

To export and import typed code, the user need to use the filein and fileout facilities. Monticello is not supported yet.

Filein of new code have problems when typechecking, because another method could not exist yet when is being imported. To solve that problem, the user should:

  1. Disable the type system
    Gradualtalk configuration disable: true
  2. Import the code using filein
  3. Enable the type system
    Gradualtalk configuration disable: false
  4. Import again the code using file in. A second “file in” is needed in order to properly load the types of instance variables.

Or the user could import a untyped version of the code first.

We are working into provide support to Monticello in order to easily upload/download typed code.