The paper reference is: Siek & Taha: Gradual Typing for Functional Languages http://ecee.colorado.edu/~siek/pubs/pubs/2006/siek06:_gradual.pdf http://ecee.colo

The paper reference is: Siek & Taha: Gradual Typing for Functional Languages http://ecee.colorado.edu/~siek/pubs/pubs/2006/siek06:_gradual.pdf http://ecee.colorado.edu/~siek/pubs/pubs/2006/siek06:_gradua... (Of course, the "functional languages" bit isn't critical here --- the paper defines gradual typing for a lambda calculus, which is the usual vehicle for explaining type systems.) Basically, you want to partition the program into parts with and without known types. If you know the types, they must be equal. If a type is unknown, it is "equal" (consistent) with anything. The conclusion of the paper is that you need a different, symmetric notion of consistency, that is different from subtyping. Making Any the root of the type hierarchy doesn't work. You explicitly want to allow things like implicitly passing an Any as an argument where, say, an Int is expected, which would be a down-cast. You don't want to allow implicit down-casts all over the place, because that causes the type hierarchy to collapse --- if you allow implicit down casts, you can always up cast to Any, and then immediately down cast to any other type.