[skybrian]

I'm wondering what programmers in functional programmers do about this sort of thing? It seems like they have much stronger type constrants; subclassing and upcasting just plain don't work. And if they did work, it would invalidate the sort of proofs that functional programmers like to do.

[pcwalton]

Treating "upgrades" as a specific case of reflection, typically what happens is that the function that wants to do reflection declares that it wants to perform reflection on its arguments via the type system. For example, in Haskell this mechanism is called "typeable" and in Rust this is called "any".

The nice thing about this approach is that it signals to callers that reflection is going to happen, so callers can be ready for it—the types become a form of documentation. If reflection is unrestricted it's easy for callers to get surprised when methods are called that they didn't expect. (Go has had breakage during point release upgrades from this, for example.)

This stricter approach requires that you plan ahead for "upgrading" in advance since you can't change a non-upgradeable argument to an upgradeable one without changing the type signature and breaking your callers. On the other hand, your callers are secure in the knowledge that you won't do that: they know that if you didn't give them access to one of your type's methods they can't sneak around and get access to it through the "back door". Non-upgradeable interfaces can also be more efficient since there is no need to store the reflection metadata at runtime; with this approach you only pay for what you use. Altogether it's a classic static-versus-dynamic-typing tradeoff.

[lmm]

Usually we have a more powerful type system that means we don't need to. E.g. in something like Go you might have a Reader, whereas in a functional language you might have [A: Reader], i.e. a generic type A for which a Reader typeclass instance exists. This means you don't have to throw away the specific type (ReaderCloseable) to be able to use it as a Reader.

If you really need to cast, most functional languages will still let you - but as you say, it invalidates the proofs so is very much discouraged (e.g. the scalazzi safe subset requires you to not cast).