This is an old revision of the document!
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 that the type system should 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 much 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.
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 this types in any place where declaring a variable or typing an expression is need. Quick Reference refers to these with several examples.
Download
The latest version of Gradualtalk can be found here: Gradual Typing (Jenkins)
There are two images:
- Types.zip: The basic image of the Gradual Type System
- Types-KernelTyped.zip: Has the same functionalities that the basic image, but additionally some kernel classes and the type system has been typed.
We recommend to use the Cog VM.
As examples, we include some typed projects, available for download:
Quick Reference
Activating the Type System
The type system is optional and by default it is deactivated. The reason for this is that the most packages in the Pharo VM are untyped. Activating Gradualtalk by default will leave to an unnecessary agglomeration of implicit casts.
To active the type system in a given class (and all its subclasses), it is needed to add the TTyped trait 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 type 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 its old significance. However, this maybe is not 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: '(Number)N' instanceVariableNames: '(N)x (N)y' classVariableNames: '' poolDictionaries: '' category: 'Tutorial'
Upperbounding method parametric types
True >> (A) & (A) aBoolean <whereType: '(Boolean)A'> ^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 enable. 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:
TypeConfiguration uniqueInstance enableInstrumentation: false. TypeConfiguration uniqueInstance 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 strategy 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 have all responsibility 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
TypeConfiguration uniqueInstance disable: true
- Import the code using filein
- Enable the type system
TypeConfiguration uniqueInstance 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.