1
$\begingroup$

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. ...".

$\endgroup$
5
  • $\begingroup$ Could you clarify the question? There are languages that allow branching on runtime type information and languages that don't. If you do want branching on type information the run-time needs to retain that information, this has performance implications. $\endgroup$ Commented May 30, 2023 at 9:41
  • 1
    $\begingroup$ @MartinBerger Perhaps type-theory is not the correct tag (suggestions welcome). In terms of programming to an interface, if a function takes a B, it seems (dare I say) obvious that calling methods that B does not have is breaking some kind of rules. I assumed that those rules are type-related, but perhaps that is incorrect terminology. What is the name for the sense in which that is wrong? $\endgroup$
    – nullUser
    Commented May 30, 2023 at 15:25
  • $\begingroup$ The tags are fine. This is a genuine type-theoretic Q. $\endgroup$ Commented May 30, 2023 at 20:09
  • 1
    $\begingroup$ You are right with both your assumptions, and programming languages that do either exist. From the point-of-view of type theory, the issue is that when type-checking if B then P else Q you want to push the type constraints you get from the condition B into the two branches: when type-checking P you want to assume the truth of B. For Q you want to assume the negation of B. Simple typing systems do not allow you to do this, but more sophisticated ones to. Setting up a typing system that lets you do this is a bit non-trivial. $\endgroup$ Commented May 31, 2023 at 19:05
  • $\begingroup$ In other words, you shouldn't be using if-then-else because you become a victim of boolean blindness. A better construct is some sort of a downcast with an optional result. $\endgroup$ Commented May 31, 2023 at 20:02

2 Answers 2

1
$\begingroup$

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"

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Perhaps I made a mistake using the type-theory tag then. In terms of programming to an interface, if a function takes a B, it seems that calling methods that B does not have is breaking some kind of rules. What is the name for those kinds of rules so that I can read further on them? $\endgroup$
    – nullUser
    Commented May 30, 2023 at 15:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.