Static Typing and Expressivity

I recently discovered an essay, "What To Know Before Debating Type Systems." It is an excellent essay, and I highly recommend reading all of it. However, there was one particular section that really caught my attention: "Fallacy: Static types imply longer code." The author suggests that a static type system can actually allow a programmer to write more concise solutions to some problems.

There is one Haskell example given to support this: if you compare the return value of Data.Map.lookup to "Nothing" or "Just object", then the function's return value will be of type "Maybe object". If you don't do this check, then the function will throw an exception if the search value isn't found. Unfortunately, I'm new to Haskell and having trouble understanding how this capability can make code more concise. If I'm not mistaken, the "lookup" function is polymorphic on the return type. The person that wrote "lookup" created several versions with different return types, and Haskell can infer the correct one to use based on the way that the return value is used. But if I were using an untyped language, wouldn't it be possible for me to write the same functions with slightly different names for different return types? Perhaps "lookupEx" could throw an exception while "lookupNull" could return some sort of Null value. I admit that this solution seems somewhat less elegant and reliable, but I think the code would be about the same length.

I would really appreciate it if anyone could offer some insight into this issue. Also, if you happen to know of any other articles or papers describing examples of improved expressivity through static typing, I'd love to read them.

To clarify, I certainly agree that a static type system can catch errors at compile time that wouldn't be caught until runtime in a dynamically typed language (even including some infinite loop bugs!). However, right now I'm mainly curious about expressiveness. Unfortunately, many people refer to a static type system that can express a lot of information about the variables and thus catch more bugs as an "expressive" type system. This ambiguity has made it difficult to find answers with Google.


Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Only one lookup

The person that wrote "lookup" created several versions with different return types

There's only one lookup. Underneath the hood it executes a function called fail or a function called return (not the same thing as return in many common imperative languages) depending on whether the key requested is in the map. The concision comes from the fact that return and fail are overloaded. Maybe has one return/fail pair, List has another pair, etc. Haskell's type system statically figures out which pair is appropriate based on how you use the result of lookup.

You can, of course, encode this in a dynamically typed language. You could, as you suggest, have different forms lookup1 and lookup2 etc. Or, for more generality, you could have one lookup that explicitly takes a pair of functions or an object with fail and return methods. But that was his point, in this particular case the static typing system reduces the need for explicit work (even if only a bit) which runs contrary to the more popular assumption that static typing systems always lead to an increase in verbosity.

That won't always be the case. Some dynamically typed language with a powerful dynamic metaprogramming facility might get another job done much more concisely than Haskell could. The point the essay makes is that the tradeoff between static and dynamic typing shouldn't be seen in terms of verbosity, or performance, or most of the other red herrings people use to "support" their point of view.

Haskell type classes are implicit parameters.

Update: Hmm... I misread your post. Feel free to ignore my post, it's mostly irrelevant.

Here's a simpler (though less impressive) example. Imagine a language that let you overload functions based on the return type. (Java doesn't but I think C++ might with const vs non-const).

int Read();
String Read();

int x = Read();      // Calls the first function.
String x = Read();   // Calls the second function.

It's not that hard to just name the functions "ReadInt" and "ReadString" (and, honestly, I probably would in this case) but that's not the point. By assigning the result to an "int" in the first case, the programmer has already specified that he wants to read an integer. Requiring him to also tack "-Int" on to the name of the function makes the code slightly redundant. Redundancy is not always a bad thing, but here you have the ability to avoid it if you want to.

Now back to the Haskell example... When "lookup" is called, the requested key may or may not exist in the map. The "lookup" function is not hard-coded to return a value of type "Maybe" -- it uses type class magic to let the caller decide how to handle those two cases. Here's a version of "lookup" that doesn't leverage Haskell type classes.

lookup :: k -> Map k a -> (a -> r) -> r -> r
-- Param 1: The key you're looking up
-- Param 2: The map
-- Param 3: The function to apply to the value if the key exists.
-- Param 4: The value to return if the key doesn't exist.

Now let's say we had a "Map" that mapped employee names to salaries. Depending on what we pass as the third and fourth argument to "lookup", we can handle the "missing key" case differently.

-- If the employee doesn't exist, return zero.  Otherwise return his salary.
-- ('id' is a function that just returns its first argument)
lookup "Bob" salaries id 0

-- If the employee doesn't exist, return 'Just salary', otherwise return 'Nothing'
lookup "Bob" salaries Just Nothing

Here's the example from the article modified to use our new "lookup" function:

case (lookup bobBarker employees Just Nothing) of
    Nothing     -> hire bobBarker
    Just salary -> pay bobBarker salary

The point the author was making is that we actually don't have to pass in "Just" and "Nothing". The "lookup" function instead says in its type declaration that it requires a "Monad" instance for type "r". Every "Monad" instance contains a function and a value -- exactly the two extra parameters that "lookup" needs.

Because the Haskell type inference algorithm can figure out that "r" is of type "Maybe ...", it will automatically locate the Monad instance for the "Maybe" type and pass it along (it's a hidden parameter). So we no longer need those two extra parameters.

Object oriented languages often achieve a similar effect by putting this extra information in the virtual method table. For example, the virtual method table for "Maybe" could have two functions: one for "Just" and one for "Nothing". However, notice that in this case we aren't passing any parameters of type "Maybe" to the "lookup" function. So it wouldn't even have an object to perform virtual method calls on. It's the implicit parameter magic of Haskell's type classes along with the inference of the return type that allows this to work.


Your post may be slightly tangential, but it is definitely illuminating. As I mentioned, I'm still learning Haskell, and it seems to me that you must have a very deep understanding of these things to be able to explain monads and typeclasses so clearly.

I don't understand why this is tangential

Obviously you're right because even the author of this post admits they misread your post. But it seems to me that they are precisely replying to your question: one piece of code called 'lookup' can serve multiple purposes and so we can get more things done with less code, exactly what you were asking about. So what did I misunderstand?

He understood more than I thought

His original post acknowledged that return type inference was saving you some work (something that I patronizingly repeated in my post). I think James Iry better answered his question. But I'm glad the explanation of Haskell type classes was useful.

I still don't understand monads

Just to be clear, my post was really only about Haskell type classes. The use of "Monad" in the example is somewhat superficial. I'm getting more comfortable with monads as I use them more, but I'm quite a ways away from any form of "deep understanding" :)

Implementation, not language

While all current Haskell compilers (so far as I know) implement type classes using added dictionary parameters, this is not the only feasible implementation. BitC, for example, uses polyinstantiation to emit procedures that do not require any additional parameters at all. Each method is expanded independently for each combination of parameter types.

We did this because the language supports unboxed value types. While you could handle those by extending the dictionary pointer idea to include frame offset indices, but the resulting generated code is not terribly efficient. Since one of BitC's goals is to preserve the programmer's source-level intuitions about code execution costs, we didn't want to go there.

A lesser reason is that we can preserve a more straightforward interface to C.

On the whole, I would say that polyinstantiation has worked very well. Fortunately, it is easy to do duplicate suppression for the really common cases.

While all current Haskell

While all current Haskell compilers (so far as I know) implement type classes using added dictionary parameters, this is not the only feasible implementation.

JHC does not.

Another argument for better expressivity

I discovered a blog post discussing Ada's type system as a method to achieve better productivity.

I think that I can summarize the author's main argument with this: Ada allows a programmer to create a type declaration, and then have the language generate a lot of attributes that the programmer can then use without having to write them manually.

For example, you create this type:
type Speed_Range is range 0 .. 1000;
and then you can get the maximum number of characters needed to represent a value of that type as a string, as well as various other things.

This is just available as soon as you declare the type, with no other work required by the programmer. If I wanted that information in a dynamically-typed language, I'd probably have to write a procedure to calculate it.

I'm not sure what to think of this argument myself. Ada's type system sure does have a different flavor compared to Haskell.

I think Ada's approach has

I think Ada's approach has some merit. Basically, each type definition automatically produces a standard set of polytypic functions.

A bit hair splitting

A bit hair splitting perhaps, but I seem to remember that Ada only checks range types dynamically, so saying that you cant have that in a dynamically typed language seems wrong to me.

Doesn't sound correct to me

I don't see how static typing leads to shorter code. I mean, consider a language with the same syntax/semantics of Ocaml/Haskell/SML, except that instead of static typing, it's run-time type checked. If the program has no type annotations (i.e. all types are inferred for the static typing), then the exact same code will work exactly the same on both languages. But if the program contains a single type annotation for the static checker, that annotation could be omitted for the dynamic checking version, making the dynamic checked version shorter. Note that languages like Ocaml, Haskell, et. al. generally contain syntactic/semantic features which do allow you to write shorter code than languages without those features (variant types, pattern matching, and partial function application spring to mind)- but those features are not dependent upon static type checking to exist.

What static type checking does do, rather than making the code shorter, is to make the development time for the code shorter (the variable we're really interested in optimizing). But not by making the code shorter, but by making the debugging process significantly shorter.

I mean, consider a language

I mean, consider a language with the same syntax/semantics of Ocaml/Haskell/SML, except that instead of static typing, it's run-time type checked.

This assumes that the only role of the type system is in checking that programs are well typed. It's pretty obvious that, were this the case, static typing could offer no increase in expressiveness. But consider Haskell typeclasses where the types are used to drive overload resolution. How do translate that into your run-time type checked language?

With great difficulty, as

With great difficulty, as I'm discovering while contemplating the idea of a monad-heavy dynamically-typed functional language. It's bad enough handling the evidence passing neatly once you've picked an instance.

By backtracking?

Run all the methods of the typeclass that might be applicable in parallel, until one of the method returns with a type that match the expected type.

Does not work

In general, there is no actual object of the type that drives the type class dispatch - neither in the arguments, nor in the result. It really is dispatch on types, not values.

Also, the number of possible instances potentially is infinite.

(Also, you seem to assume here that static and dynamic "types" are the same thing, which they aren't - the former carry much more information, which is available to dispatch. The article mentions this.)


Matt M: This assumes that the only role of the type system is in checking that programs are well typed. It's pretty obvious that, were this the case, static typing could offer no increase in expressiveness.

Even that "obvious" conjecture is, in fact, false. Typeful programming uses types actively to ensure properties that otherwise have to be enforced by other, additional language features. One such property is encapsulation.

Here is a simple example in SML: an abstract type for names/timestamps that can be generated fresh and be compared:

structure Name :> sig eqtype t; val fresh : unit -> t end =
   type t = int
   val n = ref 0
   fun fresh () = (n := !n+1; !n)

Here, the type system makes Name.t an abstract type, which prevents any client code from forging names. This is crucial for correctness of the implementation, because otherwise the fresh function wouldn't be guaranteed to return a fresh name on each call.

In other words, removing the type constraints would break the code. You would need to add something to fix the implementation (of course, there are various ways to do this).

Even that "obvious"

Even that "obvious" conjecture is, in fact, false. Typeful programming uses types actively to ensure properties that otherwise have to be enforced by other, additional language features. One such property is encapsulation.

My claim wasn't a conjecture so much as it was a tautology; if type erasure preserves program behavior then types needn't be written at all to achieve a particular program behavior. That types establish properties of your programs is ... pretty obvious.

Well, the point is

Well, the point is, the ability to enforce properties in a certain programmatic way that is not possible without types is a gain in expressiveness - contrary to what you said.

A major value of types... not the correct programs are accepted by the compiler.

It's the numerous incorrect programs which are rejected by the compiler, but which a language with a less-powerful type system might permit.

Alternate reality


Matt M: This assumes that the only role of the type system is in checking that programs are well typed. It's pretty obvious that, were this the case, static typing could offer no increase in expressiveness.

You should be careful about the meaning of 'expressiveness' here. If this just refers to ease of expressing program behaviors, then it is true, but if it includes ease of expressing program fragments (e.g. libraries) that must enforce certain usage patterns, it is not.

I agree. Good point Andreas.

How do you do overload resolution

... in a dynamic language? Virtual method invocation and/or dynamic dispatch. Talk to any Lisp, Scheme, Ruby, Python, or Smalltalk programmer- dynamically typed languages do this all the time.

There is a performance advantage to static typing- you don't need to spend the time at runtime checking types which are generally correct. And there is a development advantage to static typing, in which correctness problems are detected sooner and more accurately, which makes them easier/cheaper to fix. So it's generally easier/faster to develop in a statically typed language, IMHO. But not because you have to type in less code.

Actually, I take that back, there is one way that statically typed languages require less code- unit tests. Many, possibly most, unit tests written by agile, test-driven developers in dynamically typed languages could be replaced with static type checks, eliminating the need to write all that code associated with all those tests. Not all unit tests, I agree. But many.

Given that it's not unusual for unit tests to approach 80% of the total code, reducing the number of necessary unit tests (for a given level of code correctness) by, say, 50%, reduces the total amount of code needed for the project by 40%. And my suspicion is that good utilization of types actually reduces the number of necessary unit tests by way more than 50%.

How do you do overload

How do you do overload resolution ... in a dynamic language? Virtual method invocation and/or dynamic dispatch.

But then your simple argument that statically typed programs must be larger breaks down, since you now need to show how to convert type class based dispatch in Haskell to whatever encoding you have in mind for your language, and show that this encoding doesn't increase the size of the program.


The key thing to understand about Haskell style type dispatch is that the overload resolution can occur based on information that is "later" in the program. Types don't need to live in the world of operations occurring in sequence. Runtime dispatch, on the other hand, must be based on information that is available at the moment of dispatch. In a case like "lookup" that means a certain amount of redundancy. First you must specify the object or pair of functions to be used inside "lookup" then you examine a tag on the result to see what you got. But the tags you look for in the result are going to be correlated to the object/functions you passed to lookup. So, to some extent, you've just said the same thing twice.


overload resolution can occur based on information that is "later" in the program

I was a bit confused when I first read this, but I think I get it now. In a dynamically-typed language, a bit of code is fully evaluated to a value, and then that value has a type assigned to it, so you can only ever do type-based dispatch during the program's execution, using the information available at that time. In a statically-typed language, the type information for a bit of code is calculated first, before that code is fully evaluated. Thus, you can use that information to choose when and how (even if) the full evaluation of that code takes place. So a statically-typed language can use information that wouldn't be available until "later" if you were using a dynamically-typed language. Is this about right?

For example if f :: Int ->

For example if f :: Int -> Foo then f (read "123") will infer the Int instance of read. The 'dispatch' is based on the required return type. (Edit: Had 'show')

Interesting point

I think that I've understood most of your post, so I'm going to try to paraphrase what I think you've said.

Haskell has some features that make it more expressive than other languages. For example, if you have a Haskell function that takes three arguments:

foo x y z = (x + y) * z

We can use partial application to easily use that old function to create a new function that only takes one argument and calls it:

result = (foo 2 3) 5

In Python, a rough translation would be:

def foo(x, y, z):
    return (x + y) * z

def partialfoo(z):
    return foo(2, 3, z)

result = partialfoo(5)

As you can see, that is somewhat more verbose. However, this handy feature of Haskell doesn't actually depend on static typing. It would be possible to create a dynamically-typed version of Haskell that also supported this feature.

It's rather odd to think about a dynamically typed version of Haskell, but I'll try it anyway. In the real version of Haskell, some things are checked at compile time, while some things would fail with runtime exceptions. In this new dynamic version, anything that would have failed at compile time with the original language would simply become a runtime exception. So, does this mean that "static" and "dynamic" typing systems can be equally strict, in terms of the bugs that they catch, but with the checks happening at different times?

But going back to expressiveness, there is a quote from the original article that I have just re-read and think is relevant: "Static types often allow one to write much more concise code! This may seem like a surprising claim, but there's a good reason. Types carry information, and that information can be used to resolve things later on and prevent programmers from needing to write duplicate code."

The author asserts that "Types carry information." Isn't this also true of dynamic types? If a dynamic type system carried the same information, couldn't it resolve things in exactly the same way? (Note: I'm not actually trying to argue a point here; I'm just thinking out loud)

Dynamic types, overloading, and laziness

Pick any two.

Having all three is difficult. Consider the following scenario:

* You have a nontrivial term T which evaluates to an unknown (by the compiler) type.
* You have a function foo() which has multiple versions, dispatching on type;
* foo() is lazy WRT its argument.

What to do? In order to select which version of foo to use, you have to know the actual type of T. Since this is a dynamically-typed environment, it is not known a priori. But wait--there is an easy way to find about. Modulo divergence, the type of T can be discovered by evaluating T and examining the meta-object pointer (or whatever) of its result. Problem solved! Except--guess what--this makes foo() eager in its arguments; as selection of the correct version of foo requires evaluation of the argument to recover the type. If T contains no side effect and always returns a value, no big deal; however, if foo() is a function that depends on laziness to avoid divergence (or to correctly order side-effects), you're hosed.

While the value of a given term in Haskell is not computed until it is absolutely, positively needed, the type of each term is known prior to the program's execution. So types of terms can participate in dispatch schemes (whether its simple overloading, pattern matching, etc).

Type dispatch

Thank-you for explaining this. Your post seems to express a deep insight into static typing. I've spent some time in the last few days doing some investigation into dispatch schemes involving types, particularly type classes. I found a mailing-list thread describing the use of multi-parameter type classes to achieve something like multiple dispatch in dynamic languages, only statically. The example describes how to create a 'collide' operation that does different things depending on which astronomical bodies are colliding:
*Collide> collide (Asteroid, Earth)
"the end of the dinos"

This is a neat demonstration of the power of type-classes, but one of the messages in the thread suggested that this technique could not be applied to solve the same sort of problems that dynamic multiple-dispatch solves, and I think I understand why. Dynamic multiple-dispatch could be used to dispatch on the types of some data read in from a file or entered by the user, whereas static dispatch requires the types to be known at compile-time.

So, if type-dispatch isn't the right way to solve this kind of problem, does anyone know of a different example problem that type-based dispatching is well-suited to solve?

Types are semantic

Types are semantic information about a program. With more information, more things are possible. This information must be constructed manually in a dynamically typed language (say, by explicit registration), resulting in less expressiveness. As another poster mentioned, typeclasses may very well be one such example. Of course, many typed languages may not exploit this additional information very well at present.

Not all statically-typed languages are created equal

Type classes effectively use type information to do term inference as well as type inference - a corresponding explicitly-typed language needs some notion of 'evidence passing', which corresponds to additional parameters (the obvious example being the dictionary-passing transformation in which => becomes ->) and generating evidence (building dictionaries) from the available instances.

Idea for expressivity example

This thread has continued to occupy my thoughts a great deal in the past week, and I would like to thank everyone who has helped me to understand these difficult concepts. I have an idea that I would like some feedback on. Based on what I have learned from this thread, some languages choose to implement dynamic typing and overloading. Other languages give preference to overloading and laziness. However, it isn't possible to utilize all three of these features together. I believe that I might be able to write a short series of blog posts to describe a situation in which Haskell can demonstrate a significant gain in expressivity compared with dynamically-typed languages. Here's how it would go:

Part 1: Overloading. This is an important feature, as it allows you to write a function that uses an equality operator (==), for example, but still works on many different types. Haskell achieves this with typeclasses, while a dynamically-typed language such as Python offers operator overloading and duck typing.

Part 2: Laziness. Laziness is important because it allows the separation of generation from selection. Haskell is lazy by default, while Python offers generators.

Part 3: Overloading and Laziness combined. This is an important feature to have in this situation (have not yet developed a good example). Haskell can combine laziness and overloading like so. In Python you can start like this, and do this, and... Oh, wait. Maybe you can't do that in Python.

Am I missing something? Would this be a valid demonstration of the existence of a situation in which better expressivity can be achieved with Haskell?