Typing and Subtyping

We first start with some design goals for the language

Language Design Principles

Simplicity Syntax and semantics can easily be understood by users and implementers of the language Expressiveness: Language can (easily) express complex processes and structures, conflicting with simplicity. Safety: Language discourages errors and allows errors to be discovered and reported, ideally at compile time Modularity: Language allows modules to be type-checked and compiled separately Performance: Programs written in the language can be executed efficiently Productivity: Language leads to low costs of writing programs like Python. Backwards Compatibility: Newer language versions work and interface with programs in older versions (dependency injection for examples helps for this.)

“The basic philosophy underlying object-orientedprogramming is to make the programs as far aspossible reflect that part of the reality they are goingto treat. It is then often easier to understand and toget an overview of what is described in programs.The reason is that human beings from the outset areused to and trained in the perception of what is goingon in the real world. The closer it is possible to usethis way of thinking in programming, the easier it is towrite and understand programs.“ ~Object-oriented Programming in the BETA Programming Language

This node should be something very similar to what present in Teoria dei Tipi. But here we revise it for the master’s course in another manner.

Types allow you do something more statically detect some errors.

Message not understood

When some method does not exist we should get this kind of error, the message not understood (using the class as message passing example.) Static type systems should be able to understand this kind of messages.

Java Security Model

Code could come from arbitrary sources. For security reason, we pass code to API, and in this manner we can implement access control at this level. For this reason we don’t allo type automatic type casting like moving int to a pointer implicitly as you can do it in C. Java clearly separates the OS with some API interface, in this manner we have some sort of isolation.

Type Systems

Definition of Type System

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute B.C. Pierce 2002

• Syntactic: Rules are based on form, not behavior
• Phrases: Expressions, methods, etc. of a program
• Kinds of values: Types

A Type and Its Properties

A type is a set of values sharing some properties.A value v has type T if v is an element of T.

The properties consist on syntactical principles but also behavioural principles.

We have Nominal Types based on type names, so you just define one type is equal to another based on this kind of relationships. In this case, even if they have the same functionality, but they are called differently, then they are different. And Structural Types: you say they are equivalent when they have the same methods and fields, so its based on their availability.

In the past we have defined a concept of type equivalence based on these properties, see Algebra dei tipi.

Weakly and Strongly-Typed languages

The main distinction we make here, is the difference between type and value, and the operations that you can do about those.

Untyped languages: Do not classify values into types- Example: assembly languages. This is one of the oldest and most difficult ways to deal with code, basically you don’t have any abstraction.

Weakly-typed languages: Classify values into types, but do not strictly enforce additional restrictions- Example: C, C++. In this case, you can freely convert one value with another, the system does not check constraint before execution. This is also a reason why you get segmentation faults and stuff similar to this.

Strongly-typed languages: Enforce that all operations are applied to arguments of the appropriate types- Examples: C#, Eiffel, Java, Python, Scala, Smalltalk

Static and Dynamic Type Checking

See Teoria dei Tipi#Dynamic and static typing. The thing you have to remember is that with static you can check at compile time while with dynamic you usually just can check at runtime.

Static Type Safety

A programming language is called type-safe if its design prevents type errors.

Statically type-safe object-oriented languages guarantee the following type invariant:In every execution state, the value held by variable is an element of the declared type of v

Some of the errors are thus prevented in this manner.

Consider

Object[ ] oa = new Object[ 10 ];
String s = “A String”;
oa[ 0 ] = s;
...
s = (String) oa[ 0 ];
s = s.concat( “Another String” );

There is a runtime check at (String) to check if the thing is really a string, if not it breaks.

Usually with dynamic type checking, we get much more flexibility. For example checking the safety of generated code. You cannot do that with static since you don’t know the type during compilation. In this sense dynamic type checkers are more expressive.

Bypassing type checks

dynamic v = getPythonObject( );
dynamic res = v.Foo( 5 ); 

This is an example in C# that does this. This is useful for inter-operation or interacting with the DOM

Gradual Typing

We call gradual typing these kind of types where we have optional type checks, when you have a type annotation, you check it. This does not give you a guarantee, but its safer compared to not having it. For example in Python we can use type annotations and we have some optional static type checking in the code. We can also use Any to say that it doesn’t have any static type.

Duck Typing

When I see a bird that walkslike a duck and swims like aduck and quacks like a duck,I call that bird a duck.“ ~James Whitcomb Riley

Subtyping

Objects of subtypes can be used wherever objects of supertypes are expected

Introduction to Subtyping

Subtyping is a set relation between the types. And again, here we can decide nominal or structural subtyping. It depends on the properties that the types have! Again, see Algebra dei tipi.

Classification principles

We have mainly two ways to decide whether to classify the syntactic and semantic parts.

• Syntactic Subtype objects can understand at least the messages that supertype objects can understand
• Semantic Subtype objects provide at least the behavior of supertype objects

Other than this, we also have structural and nominal subtyping, but you already know these from bachelor courses.

Subtyping rules

We have three main subtyping rules: Existence: Subtypes cannot remove any method or field that was present in the supertype

Accessibility: We cannot make stuff less accessible.

Overriding rules: There are many overriding rules, the most important ones are the covariant and contravariant rules. But you also need to keep in mind that the type of bound methods should not be changed.

Covariant and Contravariant Rules

• Contravariant parameters: An overriding method must not require more specific parameter types than the methods it overrides
• Covariant results: An overriding method must not have a more general result type than the methods it overrides- Out-parameters and exceptions are results
  • For example Java and C# arrays are covariant, meaning they can also contain subtypes underneath it. (another method to do it would be to have generics, which would be more type safe compared to this).

Why this should be valid can be easily seen with some examples.

Drawbacks of Nominal Subtyping

Nominal Subtyping Reuse

class Resident { String getName( ) { ... }; Data dateOfBirth( ) { ... }; Address getAddress( ) { ... }}

class Employee { String getName( ) { ... }; Data dateOfBirth( ) { ... }; int getSalary( ) { ... }}

Consider the above two classes, even if underneath in the memory you will have the same results, one type is not a subtype of another, and you cannot make a common Person[] collection type. This problem is trivially not present with structural subtyping.

Normal resolution of these problems involve the adapter pattern. The main drawback of this method is added complexity in implementation and a little runtime overhead to implement this abstraction on the virtual machine.

interface Person {String getName( );Data dateOfBirth( );}

class EmployeeAdapter implements Person {
     private Employee adaptee;
     String getName( ) { return adaptee.getName( ); }
     Data dateOfBirth() { return adaptee.dateOfBirth( ); }
}

Generalization Problems

void printData( Collection<String> c ) {
	if( c.isEmpty() ) 
		System.out.println( “empty” );
	else {
		Iterator<String> iter = c.iterator( );
		while( iter.hasNext() ) System.out.println( iter.next() );
	}
}

We just needed two methods, but we had to define an input with 13 methods. So there is some inefficiency from this point of view.

How this is generally solved is to make weaker interfaces and make them extend these, but this needs lots more boilerplate code. Looks like to me code doesn’t have that human contextual understanding that makes communication very efficient. When a programmer writes code, in some sense it is communicating with the machine. The machine tells you back if he understood correctly the message, and if not, it just behaves erroneously.

Behavioral Principles

We will explore all the principles of behavioural subtyping here, which can be summarized as follows:

Subtype objects must fulfill contracts of supertypes, but:

• Subtypes can have stronger invariants
• Subtypes can have stronger history constraints
• Overriding methods of subtypes can have:
  • weaker preconditions
  • stronger post-conditions

Method Behaviour Terminology

• Preconditions have to hold in the state before the method body is executed
• Post-conditions have to hold in the state after the method body has terminated
• Old-expressions can be used to refer to prestate heap from the postcondition
• Visible States: Visible states are the pre and post states in between a method, they can be violated temporarily
• History Constraints: are reflexive and transitive constraints related to visible states.

Object Invariants

Object invariants describe consistency criteria for objects

These invariants are hold in all states in which an object is accessed.

Contract because we have obligations between the caller and the callee.

Rules for Subtyping

In all cases, the subtype should satisfy the rules of the types.

• Preconditions: they can just be weaker or equal
• Postconditions: they can be stronger or equal
• Invariants: also in this case they should be stronger.
• History conditions: must be stronger

Checking Behavioural Subtyping

We can make some static checking with regards to the types, and overriding, and also checking all heaps and things like that. We check all parameters, heaps and results. This is sound, sometimes too restrictive though, so we try to relax the logical relations to fewer, under the principle:

Any caller that wants to use the supertype postcondition must establish the supertype precondition

This is very difficult to enforce at compile time since entailment is undecidable, for this reason its now on the programmers side to check this. There are other techniques like specification inheritance to check behavioural subtyping by construction, but we will not cover it here. You can check this thread for some more checks.

Behavioural Structural Subtyping

Until now we have explored nominal subtyping, and concluded that static checking of that idea is very difficult to automate, but we have the theory. Here we are leveraging structural subtyping, and we see that the subtype should implement the parent’s contract, and we should also input the signature and behaviour of the parent type. Like:

render( { void draw( ) requires Pensures Q } p ) {p.draw( );}

If the precondition has a failure, it can be understood as a message not understood case. If the postcondition fails, its probably an implementation error.

▪ Structural subtyping ignores the behavior!

This means we cannot do it at compile time. So the semantics should still be checked at runtime and by the developer.

Violation of Inherited Fields

Invariants over inherited field f can be violated by all methods that have access to f

You can see that inheritance does not imply subtying per sé, but needs some additional properties. It’s very difficult to enforce this, which means most of the inherited classes are not behavioural subtypes, but only syntactical subtypes.

Summary

Metaphore of Contracts

Types can be seen as some contracts where static checking is possible, while for contracts is not always possible.