Lambda the Ultimate

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

3APL is a programming language for implementing cognitive agents. It provides programming constructs for implementing agents' beliefs, goals, basic capabilities (such as belief updates, external actions, or communication actions) and a set of practical reasoning rules through which agents' goals can be updated or revised. The 3APL programs are executed on the 3APL platform. Each 3APL program is executed by means of an interpreter that deliberates on the cognitive attitudes of that agent. The EBNF specification of 3APL and the deliberation cycle are available through the following links:

Can't find any mention of the 3APL language so I thought I would mention it. There are quite a few papers and a fun download with toy examples.

Oh, and there is also a mobile version 3APL-M, and a Wikipedia entry.