type-checking programs with unknown types

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.

Comment viewing options

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

Not a good example

The whole point of WSDL is to allow to generate a compile time interface for web services.

I have always wanted a language where you could generate compile time types using IO. A way to do that would be to do partial evaluation with two interfaces for IO: a run time one and a compile time one. You could then resolve the wsdl url with the compile time IO interface, and do the actual web service call with the run time IO interface.

Whole point of WSDL

Yes, I see your point, I should have made my example clearer. The essence of the problem is that even if you use WSDL to create a binding and check types at compile time, the service definition may change after you have compiled, so it is still necessary to insert run-time checks wherever you use a service. In a language like Java these run-time checks show up as downcasts. I would like to make this uncertainty explicit in the type system.

Another use for unknown types would be to stand in for types which cannot be represented in the compilation type system. For example, web services may use schemas like RELAX NG which support regular expression types, but you may not want to support these in the compiler (because it makes type inference more complicated, for example). By treating such types as unknown, I hope it is possible to keep compile-time type-checking simple and general.

Complete Type Inference

Complete Type Inference is exactly "soft" typing where you also get an error when your code is provably incorrect, though, I think many soft typing systems usually give warnings in such cases anyway.

A Sketch of Complete Type Inference for Functional Programming also 1991.

Thank you

That sounds exactly like what I'm looking for.

HM + type dynamic

Without extending standard Hindley-Milner type inference, it's easy to provide dynamic typing as a library. For example, Haskell's fromDynamic has the type "(Typeable a) => Dynamic -> Maybe a", which will detect the problem with your "results" without any annotation.