I follow some programming language people on Twitter. Last week an interesting discussion broke out between David Pollak, James Iry and Paul Snively. Eventually Manuel Simoni, Daniel Spiewak and others got involved.

David Pollak (@dpp) is working on a new programming language, he imagines it as a cross between Haskell and Excel. He asked:

Should code fail to compile if tests/contract and documentation are missing for public functions/structures/methods?

Paul Snively (@psnively) mentioned that types are all of the above:

@dpp Of course it should fail to compile if your types are wrong. ;-)

James Iry (@jamesiry) said maybe compile-time type errors could instead become warnings and emit runtime errors:

@psnively It’s sometimes useful for an IDE to “warn” on type errors and generate exception code in place of the type problem.

The Eclipse JDT compiler is one that does this. I’m not sure why the Eclipse IDE needed this functionality but it seems like the Play framework uses it to present nice-looking compilation errors on page refresh:

The compiler works by noticing type errors (amongst others) like this:

int foo(String x) {
    return x * 2;
}

But continues by emitting code like this:

int foo(String x) {
    throw new TypeError("Expected an int but got a String at line 42 of Bar.java.");
}

Play comes along, catches that runtime exception and turns it into a pretty screen.

Haskell

Interestingly, this is exactly what Simon Peyton-Jones talked to me about during a YOW! Night here in Sydney. His idea is that people want to be able to run programs, even when the compiler is telling them that parts are wrong. He wants to add a mode to the Glasgow Haskell Compiler so code like this:

foo :: String -> Int
foo x = x * 2

Is transformed into:

foo :: String -> Int
foo x = error "Expected an Int but got a String at line 2 of Foo.hs"

And the Haskell compiler will print a warning during compilation:

WARNING: Foo.hs:2:8:
    Couldn't match expected type `Int' against inferred type `String'
    In the expression: x * 2
In the definition of `foo': foo x = x * 2

The following program would execute fine with no command-line arguments but otherwise show the type error at runtime:

import System (getArgs)

main = do
  args <- getArgs
  print $ if length args > 0 then foo [1, 2, 3] else 100

This might be useful for incomplete refactoring during development. You can modify part of your program and still run that part’s tests while the types in other parts have become inconsistent.

Manuel Simoni (@msimoni) says it’s also beneficial to go into inconsistency while redefining parts of your program, interactively:

Without the ability to be inconsistent, you can’t support the Lisp Experience™

In any case, you’d definitely want to turn on treating type warnings as errors in production code.

Questions

Do you think this is a good option for statically-typed languages?

Simon seems to think this could attract fans of dynamic languages to Haskell. Would this sole feature satisfy them?

Temporary inconsistencies also play a part in distributed systems, could a similar idea be used?