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:
- Gradual Typing for Smalltalk: Accepted for publication in Science of Computer Programming, 2013 (PDF available)
- Cast Insertion Strategies for Gradually-Typed Objects: Published in Proceedings of the 9th ACM Dynamic Languages Symposium (DLS 2013)
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:
- Disable the type system
Gradualtalk configuration disable: true
- Import the code using filein
- Enable the type system
Gradualtalk configuration disable: false
- 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.