The age of type inference

Main stream languages have been continuously adopting good ideas from functional programming. Java and C# has gradually added programming constructs such as garbage collection, parametric polymorphism, lambda expressions and closures.

In spit of these ongoing endeavors, dynamically typed languages such as Python, Ruby, JavaScript and even Clojure are gaining popularity over statically typed languages. These languages are concise and elegant, and you don’t need to spend your precious time writing complex type annotations.

To regain the power stolen by dynamic languages, statically typed main stream languages have begun to introduce local type inference. For example, C++11 added auto keyword, which directs the compiler to use the initialization expression of a declared variable to deduce its type. Java and C# also added similar constructs.

#include <iostream>
using namespace std;
int main( )
    int count = 10;
    int& countRef = count;
    auto myAuto = countRef;
    countRef = 11;
    cout << count << " ";
    myAuto = 12;
    cout << count << endl;

Unfortunately, the power of type inference in these languages are very limited. Because type inference is tightly coupled with type system, we can’t introduce global type inference such as Hindler-Milner to these languages. Because of compatibility, it is practically impossible to retrofit the type system to allow global type inference.

I think it is time to design and implement a new statically typed language which looks almost the same to dynamic typed languages. Developers from Python, Ruby and JavaScript must be able to use it without learning how to put types all over the program. Dynamic vs Static typing controversy is meaningless if you don’t need to annotate any type in both languages. A statically typed language is always better because it detects errors at compile time for free.

Daniel Spiewak expects in his talk that statically typed languages with structural type systems (necessary for type inference) will dominate in the future and I totally agree with him.

The guilt of impurity

ML is guilty of impurity, so it can’t escape from a restriction. In other words, the presence of mutable ref cells and parametric polymorphism in ML requires the language to be controlled by the value restriction.

Here is a small example which shows that the ML type system is unsound without the value restriction. This allows putting a value of int where we expect a value of type string.

val r = ref NONE (* val r: 'a option ref *)
val _ = r := SOME "hi"
val i = 1 + valOf (!r)

ML fixes this by enforcing the value restriction: a variable-binding can have a polymorphic type only if the expression is a variable or value. ref NONE is a function call which belongs to neither, so the type of ref NONE is filled with dummy types that are no longer usable.

But there is a downside too. The value restriction can cause problems even when we don’t use mutable cells. The type-checker does not know that is not making a mutable reference, so it must impose the value restriction.

val pairWithOne = (fn x => (x, 1))

To circumvent the value restriction, we must wrap it in a function binding (η-conversion).

fun pairWithOne xs = (fn x => (x, 1)) xs

Haskell is free from the guilt of impurity. In Haskell, because IORefs can only be created (and used) in the IO monad, no such restriction is necessary. This is another reason why we love purity of Haskell.

Learning Prolog to be a better Haskell programmer

While learning some advanced topics of the Haskell type system, I found type level programming is reminiscent of logic programming.

For example, Fun with Functional Dependencies shows how to implement insertion sort using functional dependencies in a programming style similar to Prolog. Fun with Type Functions also shows a similar example using type families.

This similarity is not a coincidence because of the correspondence between a logic system and a type system, which is known as Curry-Howard isomorphism.

Lesson: Learn Prolog to be a better Haskell programmer!


There is a discussion on the Haskell-cafe.