How is runtime downcasting modeled in type theory?

Question

I'm trying to reconcile two opposing viewpoints I have relating to runtime type introspection and whether or not it is a type-safe operation or how that is modeled in type theory.

Suppose I have types A < B and C as in the following Python pseudo-code.

class C:
    ...

class B:
    def b_func() -> C:
        ...

class A(B):
    def a_func() -> C:
        ...

Further suppose I have a function

def f(b: B) -> C
   ...

I am tempted to say "It would be a type error to call b.a_func() inside f."

On the other hand, if the implementation of f looked like this

def f(b: B) -> C
    if isinstance(b, A):
        return b.a_func()
    else:
        return b.b_func()

then it appears the call to b.a_func() is perfectly fine.

I don't know how to even formalize the question, but is there a sense in which both of these viewpoints are valid? I'm imagining something like "It depends on what kind of type safety you are using, in ABC system only static information is allowed, so the isinstance check would be invalid in that system, whereas in XYZ type system the isinstance check is allowed. ...".

Answer 1

For type theory of object oriented programming, see [1].

There are many models for object oriented programming language concepts. Often type theory of OO is expressed in terms of category theory for modelling functions and abstractions, and domain theory for modelling recursive definitions. Usual models in terms of category theory use final coalgebras [2] [3] to model classes of objects from OO - with recursive types and existentially quantified types used for modelling stateful externally visible behaviour and references to (state of) objects. Methods are typed by signatures. Usually subtyping is preferred to subclassing to focus on interfaces rather than implementations. In such models, subclass coercions that model both downcasts and upcadts between object classes are just functions that preserve the external behaviour, subject to constraints requiring preservation of the hidden contents of existentially quantified "OO object state" (preserve the coalgebra structure and contents of existential packages). Downcasts specifically can be modelled as inverses to an "upcast" projection functions that forget some operations and state - notice the failure possibility from such operation must be carefully modelled, usually in terms of Maybe monad modelling partiality.

Notice though that object oriented programming does not in general have a common theoretical foundation, and many programming language concepts are language specific. Theoretical models usually only address public behaviour of systems consisting of OO objects, and try to abstract out the internal implementation details - i.e. primarily modelling interfaces. The models are sometimes used in discussions on language design and for implementation of compilers for the languages [4]. The theoretical models usually use same foundation that is used for modelling functional programming, to unify the foundational concepts.

A complication that often comes up when discussing theoretical models of object oriented programming is the covariance and contravariance of method signatures with respect to subclassing and subtyping relations. Different parts of the OO object model behave differently with respect to whether subclass and subtype relationships allow generalization or specialization of the corresponding method and function signatures and state, and theoretical models spend lots of time discussing when covariance or contravariance is appropriate. The subclassing relation is very complicated as a consequence, and usual approaches on abstracting that can produce unreadable descriptions involving order relationship between models of class types.

[1] Abadi, Cardelli: "A Theory of Objects", http://lucacardelli.name/indexPast.html

[2] Poll: "Coalgebraic semantics of subtyping"

[3] Crole: "Categories for Types"

[4] Muchnick: Advanced Compiler Design and Implementation"

Answer 2

AFAIK "type theory" doesn't care about those problems (there are no classes there, anyway :-), but you can always encode those things into a new cast_to_A method whose implementation in B returns something like null and that is overridden with an "identity method" in A.

IOW, even for those OO languages which claim they don't carry runtime type information, you can use the method table as the runtime type information.