Unifying Dynamic Type Tests and Type Refinement

Sunday, September 3rd 2017

Programs often need to perform different actions based on the type of an object. Here’s an example from one of my projects, which is an Android app for the board game Hnefatafl. A class called GameState encompasses all of the infomation about a specific Hnefatafl game. Each GameState has a GameType field, which holds data specific to different types of games. The three types are GameType.PassAndPlay, GameType.PlayerVsAI, and GameType.OnlineMatch 1.

Here’s an excerpt of some code where I have to perform a different operation depending on the type of gameState.getType().

GameType type = gameState.getType();
if(type instanceof GameType.PassAndPlay) {
    GameType.PassAndPlay pap = (GameType.PassAndPlay) type;
    // ...
} else if(type instanceof GameType.PlayerVsAI) {
    GameType.PlayerVsAI pvai = (GameType.PlayerVsAI) type;
    // ...
} else if (type instanceof GameType.OnlineMatch) {
    GameType.OnlineMatch om = (GameType.OnlineMatch) type;
    // ..
} else {
    throw new UnsupportedOperationException("Unknown GameType: "
        + type.getClass().getName());

Because I need to access data on the type as part of my operation, I need to downcast it 2. However, there’s some obvious redundancy here - I already know the type of an object in each branch, yet I still have to downcast it to access it’s unique members. If the Java type-checker understood the instanceof operator, it could simply set the static type of type to be GameType.PassAndPlay within the associated branch.

It turns out that some languages do exactly that. Here’s an example from Kotlin. Check Kotlin’s docs on typecasts.

fun demo(x: Any) {
    if (x is String) {
        print(x.length) // x is automatically cast to String

Here’s an example from Flow, a typechecker for Javascript. Flow understands many forms of dynamic type checks 3. See Flow’s docs on refinements.

// @flow
function method(value: boolean | Array<string> | Event) {
  if (typeof value === "boolean") {
    // value is a boolean
  } else if (Array.isArray(value)) {
    // value is an Array
  } else if (value instanceof Event) {
    // value is an Event

Here’s an example from Hack, a type checker for PHP. See Hack’s docs for type refinement.

function foo(mixed $x): int {
  $a = 4;
  if (is_int($x)) { // refine $x to int by checking to see if $x is an int
    return $x + $a;
  } else if (is_bool($x)) {
    return (int) $x + $a; // know it is a bool, so can do safe cast
  return $a;

Finally, here’s an example from C#. In C#, the refined value has to be bound to another variable name. See the docs for pattern matching.

public static double ComputeAreaModernIs(object shape)
    if (shape is Square s)
        return s.Side * s.Side;
    else if (shape is Circle c)
        return c.Radius * c.Radius * Math.PI;
    else if (shape is Rectangle r)
        return r.Height * r.Length;
    throw new ArgumentException(
        message: "shape is not a recognized shape",
        paramName: nameof(shape));

Similarities to Pattern Matching

This feature can be seen as a subset of pattern matching in functional programming languages like OCaml and Haskell. Pattern matching combines value checks, type tests, destructuring assignment, and type refinement into one construct.

Below is an implementation take in Haskell using patterm matching. take returns the first m elements of an array, dropping the rest. See the Haskell tutorial on pattern matching.

take m ys = case (m,ys) of
    (0, _)    -> []
    (_, [])   -> []
    (n, x:xs) -> x : take (n-1) xs

  1. This could have been implemented using inhertance, with different types of games being subclasses of GameState. However, I decided to go with composition over inheritance

  2. This type of operation can also be written using the visitor pattern. Unfortunately, the visitor pattern in Java is verbose, and it moves code away from the place where the behavior is used, introducing an uncessary layer of separation. The code can also be added as virtual methods to the GameType class itself, but that may not always make sense, especially if the operation is not intuitively “owned” by the GameType

  3. Flow is a gradual typechecker for an existing dynamic language. Thus Flow must understand existing forms of runtime type checks that Javascript programmers use. 

#programming-languages #java #kotlin #type-systems

Similar Posts