HomeToolsAbout

Gradual Type System

What is Gradual Type System

source

Allows parts of a program to be dynamically typed and other parts to be statically typed.

The programmer controls which parts are which by either leaving out type annotations or by adding them in.

No one solution

Large software systems are often developed in multiple languages partly because dynamically typed languages are better for some tasks and statically typed languages are better for others.

Gradual type system allows programmers to choose between a dynamic or static type system without dealing with pains of language interoperability.

Dynamic Type System

In a dynamically typed language, type checking is performed during program execution, immediately before the application of each operation, to make sure that the operand type is suitable for the operation.

def add1(x):
  return x + 1

class A(object):
  pass

a = A()
add1(a)

# TypeError: unsupported operand type(s) for +: 'A' and ‘int'

Static Type Checking

Some or even all type errors are caught by a type checker prior to running the program.

The type checker is usually part of the compiler and is automatically run during compilation.

class A {
  int add1(int x) {
    return x + 1;
  }

  public static void main(String args[]) {
    A a = new A();
    add1(a);
  }
}

/* A.java:9: add1(int) in A cannot be applied to (A)
 add1(a);
 ^ 1 error
*/

Static Type Checkers are Approximations

How can a type checker predict that a type error will occur when a particular program is run?

  • The answer is that it can’t.

It is impossible to build a type checker that can predict in general which programs will result in type errors and which will not.

  • This is equivalent to the well-known halting problem.

Instead, all type checkers make a conservative approximation of what will happen during execution and give error messages for anything that might cause a type error.

For example, the Java compiler rejects the following program even though it would not actually result in a type error.

class A {
  int add1(int x) {
    return x + 1;
  }

  public static void main(String args[]) {
    A a = new A();

    // never
    if (false)
      add1(a);
    else 
      System.out.println("Hello World!");
  }
}

The Java type checker does not try to figure out which branch of an if statement will be taken at runtime.

Instead, it conservatively assumes that either branch could be taken and therefore checks both branches.

Gradual Type System

Gradual type checker is a type checker that checks, at compile-time, for type errors in some parts of a program, but not others.

  • Directed by which parts of the program have been annotated.
def add1(x: int):
  return x + 1 # x should be an int

  class A:
    pass

  a = A() # a is a class
  add1(a) # a is not int

Type checker signals an error when a type annotation is inconsistent.

The gradual type checker deals with unannotated variables by giving them the unknown type (also called the dynamic type in the literature), which we abbreviate as ? and by allowing implicit conversions from any type to ? and also from ? to any other type.

Allowing the implicit converson from ? to int is unsafe, and is what gives gradual typing the flavor of dynamic typing.

Just as with dynamic typing, the argument bound to x will be checked at run-time to make sure it is an integer before the addition is performed.

AboutContact