Lambda the Ultimate

I find myself in need of a type system which can deal well with types that are unknown at compile time, by doing as much static type-checking as possible and then inserting downcasts to deal with unknown types at runtime. Is anybody aware of such a system already in use? Let me motivate this by a short example in some functional pseudo-code:

useNumber(number) = number + 2
useList(list) = head(list)
googleURL = "http://api.google.com/GoogleSearch.wsdl"
google = Webservice(googleURL)
results = google.search("testing")
a = useNumber(results)
b = useList(results)


Clearly the type of a dynamically-generated proxy like google may be, in general, unknowable at compile time. The obvious way to handle this is to use a Univ type which is downcast, either implicitly or explicitly, as needed. That approach seems to be typical for current languages from Java to Haskell. However I'd like to go a bit further and reject programs like the above where it's clear that some variable (in this case results) could never satisfy the constraints on its type.

This sounds to me (perhaps deceptively) like a simple problem which someone is bound to have solved already, but if so I have yet to find the solution in the literature. Maybe that's because it's so simple that it's not worth publishing, and I just need to think about it a bit.

Here are some examples of ideas I have reviewed and rejected:

• Static Typing Where Possible, Dynamic Typing When Needed -- a provocative title, unfortunately not borne out by the content of the paper.
• Cartwright and Fagan's "Soft Typing" (1991). If I have understood this paper, soft typing cannot distinguish between programs which it merely cannot prove are correct and programs which are obviously incorrect. In both cases, types simply fail to unify. However I would like to make such a distinction, so that at least some programs can be definitively rejected at compile time, and I don't mind forcing programmers to make some concessions to the type system to allow this.
• Boo is a language I've seen mentioned as supporting both static and latent typing with type inference. Based on a cursory review of their documentation, it seems they just have a Univ type with implicit casting (and a somewhat ad hoc type system in general).
• HaXe is another such language, which I rejected when I saw that their idea of type inference is "the first time the function is used, the type of the parameter will be set to the type it was used with".

Thank you for your help.

Hardware Design and Functional Programming: a Perfect Match by Mary Sheeran, Journal of Universal Computer Science, Special issue devoted to the Brazilian Symposium on Programming Languages, 2005.

This is a slightly odd paper that explains why I am still as fascinated by the combination of functional programming and hardware design as I have ever been. It includes some looking back over my own research and that of others, and contains 60 references. It explains what kinds of research I am doing now, and why, and also presents some neat new results about parallel prefix circuits. It ends by posing lots of hard questions that we need to answer if we are to be able to design and verify circuits successfully in the future.