Tony Morris on static types

Tony's blog has an interesting discussion of API design and static typing that includes one of the best reasons for very strongly typed interfaces:

Now, why these rules? Well, because if you can achieve the goal of enforcing these rules, then the next phone call that I get in L3 support from an upset client, I can be guaranteed that one of the following are true:

• I have a bug in my code, in which case, the sooner the call, the better! …unless of course, fixing the bug results in only more bugs — but we have avoided that possibility — hopefully you can see why.
• The client has misused the API and circumvented the type system. The client has used null, thrown an exception or performed a side-effect within the API or perhaps even used such things as Java reflection or even type-casting or type-casing. Unfortunately, in some environments, there’s not much I can do about enforcing that except impose a de facto rule where you assume non-existence of these possibilities (Just don’t do that!). Hopefully you haven’t yet jumped to the conclusion that any of these things are necessary or even useful — they aren’t.
• The client is simply mistaken about the merits of their complaint.

The only better reason I have heard of is the one I use: I would rather think hard for an hour or so to come up with an interface I would have a hard time screwing up than spend the next weeks or months trying to remember what is and what is not legitimate. In short, I'm lazy.

What are the rules Morris is talking about? He has an advanced programming course assignment for

students to write an API for the game tic-tac-toe. No need for the computer to tactically play tic-tac-toe — just an API that you can use to model the game itself. You can use any programming language you like, however, I think you will find certain environments to be lacking in the available tools, so I will guide you so that you’re not off somewhere “shaving yaks” so to speak.

The rules of the assignment are:

• If you write a function, I must be able to call it with the same arguments and always get the same results, forever.
• If I, as a client of your API, call one of your functions, I should always get a sensible result. Not null or an exception or other backdoors that cause the death of millions of kittens worldwide.
• If I call move on a tic-tac-toe board, but the game has finished, I should get a compile-time type-error. In other words, calling move on inappropriate game states (i.e. move doesn’t make sense) is disallowed by the types.
• If I call takeMoveBack on a tic-tac-toe board, but no moves have yet been made, I get a compile-time type-error.
• If I call whoWonOrDraw on a tic-tac-toe board, but the game hasn’t yet finished, I get a compile-time type-error.
• I should be able to call various functions on a game board that is in any state of play e.g. isPositionOccupied works for in-play and completed games.
• It is not possible to play out of turn.

The first rule is a typical virtue of functional programming: referential transparency; a piece of code which violates that rule unnecessarily is much harder to understand than code that obeys it. The second rule is somewhat less typical, but still a well-known virtue: the function should be total. A total function always returns a meaningful value, as opposed to a partial function which is not well-defined on some part of its domain; in other words, if the code calling it compiles without error, a total function always returns a useful value, while a partial function may throw an exception or return a bad value for some arguments.

The third, fourth, fifth, and seventh rules are the interesting ones. (The sixth just says that there may be operations that the other rules don't apply to.) These require encoding a model of the valid operations in the game into the types of the API.

First, a little background. The type of a computational artifact (a variable or function, for example) is actually a predicate in a formal system defined by the type system of the programming language. (Go read up on the Curry-Howard correspondence, if you want. I'll still be here.) Some type systems are strong enough to make very strong, and very useful, statements about the program being written. In this case, Morris wants the API to specify limits on its interface to prevent invalid operations in the game of tic-tac-toe.

Take the third rule: the move(board, position, player) operation should be invalid on a board that is in a finished-game state, for example. In other words, if you define "write" to be limited to code that compiles (and in particular, typechecks), then it should not be possible to write code that attempts to make a move on a finished board. Or, the move operation is governed by a predicate that prevents it from being applied to a finished board. Or, a board is governed by a predicate that prevents it from having a move applied to it.

Now, writing the API and the predicates to satisfy these rules is not exactly easy. But it is possible in at least some programming languages. Specifically, Morris mentions Haskell, Scala, C# and Java. (Morris' API for Java uses Functional Java, if you are interested.) There are a fair number of approaches to doing this in various languages, some of which can be euphemistically called "open research areas"; I would like to focus on a few of the less euphemistic.

I found Morris' post from a link in Vasil Remeniuk's solution in Scala that uses phantom types. I may come back in a bit to see how this looks in Java.

If I am not completely confused, Morris' API uses higher-order functions to convince Java's type system to make the correct promises. Rather than have move(board, position, player) return a new board (to drastically oversimplify what I think Morris has done), move effectively takes three additional objects, each of which is a functor (in C++ lingo) or "command object" (in Patternish), an object that encapsulates a function along with necessary data; that is, a half-assed implementation of a closure, or a first-class functional value. These three function-objects handle three possible cases: the move's position is already occupied, the game is already over, or the move is valid and the game should continue. This approach is uncommon in Java, and certainly looks hideous. But, it works.

The third approach I want to mention actually involves weakening Morris' rules, in order to get an API that is somewhat less uncomfortable. Consider what happens if you make a valid move in tic-tac-toe: the resulting board may represent the end of the game, or it may allow the game to continue. Morris' API specifies that client code has to handle this bifurcation (Hi, Del!) by passing in two different function-objects for the two different cases, because Java's options are limited. (As I understand Morris, anyway.) The alternative I have in mind is to allow a certain minimal bit of non-total functionality, by having the move operation return either an in-progress board or a final board, where the "either" is given by an Either algebraic type:

public abstract class Either<S,T> {
  private static class Left<S,T> extends Either<S,T> {
    private final S s;
    private Left(S s) { this.s = s; }
    @Override public S isLeft()  { return s; }
    @Override public T isRight() { return null; }
  }

  private static class Right<S,T> extends Either<S,T> {
    private final T t;
    private Right(T t) { this.t = t; }
    @Override public S isLeft()  { return null; }
    @Override public T isRight() { return t; }
  }

  public abstract S isLeft();
  public abstract T isRight();

  public static <S,T> Either<S,T> left(S s)  { return new Left<S,T>(s); }
  public static <S,T> Either<S,T> right(T t) { return new Right<S,T>(t); }
}

This class is used something like:

    Either<Integer,String> is1 = Either.left(4);
    Either<Integer,String> is2 = Either.right("four");
    
    System.out.println(is1.isLeft() + " " + is1.isRight());
    System.out.println(is2.isLeft() + " " + is2.isRight());

where the output is:

4 null
null four

Notice that Either encodes a type-level choice; a value of Either contains a value of one of two other types. In the tic-tac-toe case, move can return Either<InProgressBoard,FinishedBoard> and the client code can pick out the right board, at which point it can type-safely take the next step. The non-totality enters because calling isRight on a Left value returns null; client code using that value cannot do anything unsound, but it also will not get a compile-time error. This approach provides an API that more closely resembles normal Java but weakens Morris' rule three to something like "If I call move on a tic-tac-toe board, but the game has finished, I should get a compile-time type-error unless I have done something god-awful stupid. In other words, I am required to check the result and actively be idiotic to get a run-time error." Which is bad, don't get me wrong, but may not be as bad as trying to explain Functional Java to the numbskulls soiling your API by trying to use it.

Morris would disagree, as witnessed by his comments quoted above and by the following, from another post:

Some people like to think “correctness” includes the thoughts of one or more persons in order to make the assessment. For example, one might proclaim, “sure you have a proof of program termination, but that is not the program that I asked for!” I think this is a poor use of the term “correctness” and I am not considering it any further here.

As a bit of a formalist myself, I can certainly feel the attraction to that definition of correctness, but it still leaves one in the unpleasant position of having a rather strange, technical meaning for a commonly-used word; somewhat like the difference between true and formally proven. For myself, I have seen too many comments to the effect of "if we proved everything correct, there wouldn't be any bugs" (for example, see David Harel's Algorithmics) or "[system X] has [huge percentage Y] devoted to handling situations that shouldn't occur" (see David Gries' The Science of Programming); even with software that is correct according to Morris, my to-do list would likely not be much shorter and TCP would still have to send retransmissions.

In any case, Morris has given a really nice challenge as well as an excellent description of why the challenge is worthwhile, and I too look forward to the day when I can be assured that that phone call likely represents genuine bug.

[Edit] Amazingly, a quick-and-dirty translation of Remeniuk's Scala code to Java seems to demonstrate the properties I was looking for. (This code was put together very quickly and does not attempt to satisfy all of Morris' rules. Nor does it meet all of the guarantees made by Remeniuk's code. But it's not bad.)

public class Phantom
{
  static abstract class Mark { }
  static class Nought extends Mark { }
  static class Cross extends Mark { }
  
  /* ... */
    
  static abstract class GameState { }

  static class NotFinished extends GameState { }
  static class Started extends NotFinished { }
  static class NotStarted extends NotFinished { }
  
  static class Finished extends GameState { }
  static class Failed extends Finished { }
  static class WinState extends Finished { }
  static class DrawState extends Finished { }

  static class Position {
    public final int x, y;
    Position(int x, int y) { this.x = x; this.y = y; }
  }
  
  static final class NextTurn<Last extends Mark,Next extends Mark> {
    // Type witnesses: values used only to force specific types.
    public final NextTurn<Nought,Cross> crossesTurn = new NextTurn<Nought, Cross>();
    public final NextTurn<Cross,Nought> noughtsTurn = new NextTurn<Cross, Nought>();
  }
  
  // S: Board's position in the game: NotStarted, Started, etc.
  // M: Last mark to be played.
  // Next: Next mark to be played.
  static class Board<S extends GameState, M extends Mark> {
    <Next extends Mark, S extends Started>
      Either<Board<Finished,Next>,Board<Started,Next>>
      move(Position position, NextTurn<M,Next> nextTurn, S isNotFinished) { /*...*/ }
  }

One thing that differs from the Scala code is that I have had to use explicit type witness values; in Scala I believe they are implicit. Also, the Scala code uses the same function argument approach as Morris', by calling Either.fmap.

This code would be very easy to circumvent, but it does demonstrate some of the desired features:

  public static void main(String[] args) {
    new Board<NotStarted,Nought>()
    .move(new Position(1,1), NextTurn.crossesTurn, new Started())
    .isRight() // The resulting board will not be Finished.
    .move(new Position(1,2), NextTurn.crossesTurn, new Started());
  }

The second move() call indicates that Cross is taking another turn, and fails to compile with the following error:

$ javac -cp src src/tictactoe/Phantom.java
src/tictactoe/Phantom.java:87:
 <Next,S>move(tictactoe.Phantom.Position,
              tictactoe.Phantom.NextTurn<tictactoe.Phantom.Cross,Next>,
              S) in 
    tictactoe.Phantom.Board<tictactoe.Phantom.Started,tictactoe.Phantom.Cross>
  cannot be applied to
    (tictactoe.Phantom.Position,
     tictactoe.Phantom.NextTurn<tictactoe.Phantom.Nought,tictactoe.Phantom.Cross>,
     tictactoe.Phantom.Started)
      .isRight().move(new Position(1,2), new NextTurn<Nought, Cross>(), new Started());
                ^
  1 error

Copyright © 2007-2017 Tommy M. McGuire