Lambda the Ultimate

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.

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?

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.

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" :)

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 compilers (so far as I know) implement type classes using added dictionary parameters, this is not the only feasible implementation.

JHC does not.

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

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.

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 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.

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.

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 =
struct
   type t = int
   val n = ref 0
   fun fresh () = (n := !n+1; !n)
end

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" 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, 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.

...is 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.

Andreas:

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.

... 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 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 -> Foo then f (read "123") will infer the Int instance of read. The 'dispatch' is based on the required return type. (Edit: Had 'show')

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)

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).

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 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.

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.