Can a dynamically typed language support type inference?

In a post about Ruby's dynamic typing, I made the claim:

Meta-programming makes the type inference problem equivalent to the halting problem.

Am I wrong? Basically, I am wondering if there are type inference algorithms (or better still, implementations) that can handle programming languages where the operations permitted with respect to a variable (a/k/a types) change at run time.

Your corrections and pointers to current research and/or implementations would be greatly appreciated.

Thanks in advance...

Comment viewing options

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

Dynamic metaprogramming is the problem

Change your italicized phrase to "Dynamic meta-programming..." and I think you're right. However, static metaprogramming (e.g. many macro systems) doesn't interfere with typing in any insurmountable way.

Also, I think your definition of "dynamically typed" seems somewhat conflated with the issue of dynamic metaprogramming. You can have dynamically typed languages that don't support much dynamic metaprogramming at all, and such languages are much more amenable to type inference.

Regarding research and implementations, the work on soft typing (e.g. in Scheme and Erlang) is all about type inferencing for dynamically typed langages. However, I don't think that kind of work contains much about type inference in the presence of dynamic metaprogramming, except perhaps to exclude it from consideration.

Wrong/Nonsensical question

First, you would have to define what types the type inference algorithm is supposed to produce. For example, Ruby is dynamically typed which we can view as statically typed with a trivial type system; namely every term has type "Dynamic". Type inference for this type system is clearly decideable.

Furthermore, your statement does not make sense if interpreted as follows: "Assume we have a language without metaprogramming and some, object based say, type system for it. When we add metaprogramming (specifically the ability to add and remove methods), type inference cannot be decideable with respect to the old type system." This blatantly does not make sense as the new language will have terms that don't even have types in the old languagge. Certainly, they can no longer be simply a set of operations. So it is necessary to create a new type system. We can include the old type system as a subset of the new one where terms having an old type provably support the given type. This last part is certainly undecidable in general, but that doesn't make type inference for the new type system undecidable it just means the types will have to be weaker (i.e. less informative). In fact, this will be necessary for type checking let alone type inference.

What you want to say, it seems, is: No decideable type inference algorithm for any type system can produce informative results for Ruby (for realistic code).

That is probably more or less true for any language, including Ruby, that allows unrestricted reflection. As Anton mentions soft typing is closest to what you want, but as he also mentions it usually (never?) deals with this kind of reflection, e.g. see this for MrSpidey. I think most research along this vein is more interested on controlling reflection to make type checking/inference interesting and feasible.

Excellent feedback

Thanks, Anton and Derek. I am going to update the terminology and point back to this node.

GHC typechecker

Not sure what to make of it but the post on The GHC typechecker is Turing-complete would seem to indicate that even static type checking may eventually run into the halting problem.

All type systems...

All type systems are ALWAYS a compromise with the Halting problem.

A type system is a way of proving that programs have certain properties, and proving properties about arbitrary programs is just what the Halting problem is. So we try to come up with systems that type most of the programs people naturally write, and don't take too long to run, and don't fail to terminate.

This is always a tradeoff, and sometimes it's a good idea to give up on termination for all programs in order to get success on the programs people do write.

All programming languages

sometimes it's a good idea to give up on termination for all programs in order to get success on the programs people do write

Sadly, sometimes language designers go the other way and say "it's a good idea to give up on all of the programs people might write in order to get decidable type checking for all of the programs we will let them write."

;-)

Actually...

In fact, I am one of the people who say "it's a good idea to give up on all of the programs people might write in order to get decidable type checking for all of the programs we will let them write."

That's because a restriction cuts two ways. First, it sets limits on the data you can construct as output. This is obvious.

Second, and less obviously, a restriction strengthens the invariants on the data you receive as input. This means that you can make stronger assumptions about your input, and this means you can do more things with your input data!

For example, in a language like Scheme or ML, there's no way to ensure that repeated calls to a function will return the same results, since the function might rely on a piece of imperative state.

So a pair expression like (f(x), f(x)) can't be safely refactored into let v = f(x) in (v,v). In Haskell, by contrast, this IS a correct transformation. And it's only correct because the language is restricted so that all functions are pure, which gives you stronger invariants to work with.

So there isn't any simple tradeoff between restrictions and expressiveness. Adding a restriction can increase the strength of your invariants, which can increase expressiveness more than it costs. That's why language design can get tricky....

Happily

Just a nitpick, since I agree with your comment in general: in the example you chose, if the compiler has access to enough of the source code and is sufficiently smart(tm), e.g. a whole-program compiler, then it can make that transformation.

That's why language design can get tricky....

Right - rather than the "sadly" of the OP, I'd say "happily, language designers are exploring all parts of the PL type system universe."

If you're receiving f as an

If you're receiving f as an argument to a function, then you can't always make that transformation, because you don't know what you're going to get as an argument. A whole program optimizer can find that out some of the time, but not all of the time.

As Homer would say...

D'oh!

Pure ML

Well, one can express pure constructions in ML using abstract types. Here is the basic idea expressed in Standard ML:

infix 9 $

structure SKI :>
   sig
      type 'a t
      val prj : 'a t -> 'a
      val $ : ('a -> 'b) t * 'a t -> 'b t
      val S : (('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c) t
      val K : ('a -> 'b -> 'a) t
      val I : ('a -> 'a) t
   end = struct
      type 'a t = 'a
      fun prj x = x
      fun f $ x = f x
      fun S x y z = x z (y z)
      fun K x _ = x
      fun I x = S K K x
   end

There is no way in SML to construct impure values of type t, because there is no function for injecting arbitrary values to the type and the only values of that type are pure.

Harder

I'm pretty sure that for most of the languages you're probably thinking of (e.g Ruby), meta-programming makes the type inference problem strictly harder than the halting problem. That is to say if someone handed you a sound-and-complete Ruby type-inferencing oracle, you could use it to produce a halting oracle, but not vice versa. Turing-equivalent dynamic meta-programming means that type-inferencing is at least as hard as determining whether a program halts on all inputs, which is the canonical "slightly harder than the halting problem" problem.

Cabernet and recursive function theory pedantry. It's shaping up to be a great Friday evening.