Haskell as a gradually typed dynamic language

I spent a few days this week at POPL (one day too short due to a massive blizzard currently pounding Philadelphia). As always at conferences, I had a great time and left full of new ideas.

This time, I sat in on a series of talks on gradual typing. Forgive me as I’m nowhere near an expert on gradual typing, but I took away this gist: with a gradual typing system, a type-checker does the best it can to assign static types; anything it can’t do is deferred to runtime in a dynamic type check.

As I nearly always do when considering a type system concept, I thought about how this might apply to Haskell. And I realized with a start that Haskell is only a stone’s throw away from a very spiffy gradually typed dynamic language! Let’s explore how this is the case.

(Disclaimer: I have no plans to implement any idea in this post. I also apologize, specifically, if I’m misusing the term “gradual typing”, which I’m not deeply versed in. This is all meant to be a bit tongue-in-cheek, though I think there’s a proper good idea in all of this.)

First, I wish to address a common fallacy about an existing feature in GHC:

Deferred type errors do not make Haskell a dynamic language

Recent versions of GHC come with a flag -fdefer-type-errors. (Naturally, this feature comes with its own published paper from ICFP’12.) With this flag enabled, type errors become warnings. When you try to run the code that contains a type error, you get a runtime exception. To wit:

> {-# OPTIONS_GHC -fdefer-type-errors #-}
> module GradualHaskell where
> 
> import Data.Typeable
> 
> ex1 = not 'x'

Compiling produces

/Users/rae/work/blog/011-dynamic/post.lhs:32:13: warning:
    • Couldn't match expected type ‘Bool’ with actual type ‘Char’
    • In the first argument of ‘not’, namely ‘'x'’
      In the expression: not 'x'
      In an equation for ‘ex1’: ex1 = not 'x'

Running produces

*** Exception: /Users/rae/work/blog/011-dynamic/post.lhs:32:13: error:
    • Couldn't match expected type ‘Bool’ with actual type ‘Char’
    • In the first argument of ‘not’, namely ‘'x'’
      In the expression: not 'x'
      In an equation for ‘ex1’: ex1 = not 'x'
(deferred type error)

What’s nice about deferred type errors is that they let you compile a program even with errors. You can then test the type-correct parts of your program while you’re still developing the type-incorrect parts.

However, deferred type errors don’t make Haskell a dynamic language.

Consider

> silly :: a -> b
> silly True  = False
> silly False = "Howdy!"
> silly 'x'   = 42

This, of course, compiles with lots of warnings. But you can’t successfully call silly, even at one of the values matched against. Running silly True produces a runtime type error. This is not what one would expect in a dynamic language, where silly True is perfectly False. The problem in Haskell is that we have no way to know if the type silly is called at is really Bool: all types are erased. All deferred type errors do is to take the normal compile-time type errors and stuff them into thunks that get evaluated when you force the ill-typed expression. Haskell still never does a runtime type check.

Preserving type information to runtime

The way to make Haskell into a proper dynamic language must be to retain type information to runtime. But we already have a way of doing runtime type checks: Typeable and friends.

The constraint Typeable a means that we know a’s type at runtime. The Typeable interface (from Data.Typeable) includes, for example, the function

cast :: (Typeable a, Typeable b) => a -> Maybe b

which does a runtime type equality test and, if the test succeeds, casts an expression’s type.

As of GHC 7.10, all statically-known types are Typeable. (Saying deriving Typeable is a no-op.) But type variables might still have a type unrecoverable at runtime.

So, all of this adds up to an interesting idea. I propose a new language extension -XDynamicTypes with two effects:

1. All type variables automatically get a Typeable constraint.
2. The type-checker behaves quite like it does with -fdefer-type-errors, but instead of putting an unconditional type error in an expression, it does a runtime type check. If the check succeeds, the expression evaluates normally; otherwise, a runtime error is thrown.

Change (1), coupled with the fact that all non-variable types are already Typeable, means that all types are known at runtime. Then, change (2) enabled runtime typing. Under this scenario, my silly function above would elaborate to

> forceCast :: (Typeable a, Typeable b) => a -> b
> forceCast x = case cast x of
>   Just y  -> y
>   Nothing -> error "type error" -- could even print the types if we wanted
> 
> notSilly :: (Typeable a, Typeable b) => a -> b
> notSilly true  | Just True  <- cast true  = forceCast False
> notSilly false | Just False <- cast false = forceCast "Howdy!"
> notSilly x     | Just 'x'   <- cast x     = forceCast (42 :: Int)

This definition works just fine. It does do a lot of casting, though. That’s because of silly’s very general type, a -> b, which is necessary due to the differing types of silly’s equations. However, if all the equations of a function have the same type, then the function is inferred with a precise type, and no casting is necessary. Indeed, in a program that is type-correct without -XDynamicTypes, no runtime checks would ever take place.

This idea seems to give you get the flexibility of dynamic types with the speed of static types (if your program is statically type-correct). And this general model seems to fit exactly in the space of possibilities of gradual type systems.

I’ve heard it said that Haskell is the best imperative programming language. Could it also become the best dynamic language?