<p>For type theory of object oriented programming, see [1].</p>
<p>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 &quot;OO object state&quot; (preserve the coalgebra structure and contents of existential packages). Downcasts specifically can be modelled as inverses to an &quot;upcast&quot; 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.</p>
<p>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.</p>
<p>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.</p>
<p>[1] Abadi, Cardelli: &quot;A Theory of Objects&quot;, <a href="http://lucacardelli.name/indexPast.html" rel="nofollow noreferrer">http://lucacardelli.name/indexPast.html</a></p>
<p>[2] Poll: &quot;Coalgebraic semantics of subtyping&quot;</p>
<p>[3] Crole: &quot;Categories for Types&quot;</p>
<p>[4] Muchnick: Advanced Compiler Design and Implementation&quot;</p>

CC BY-SA 4.0
2023-06-14T18:10:58.517Z
2023-06-14T19:01:53.183Z
2023-06-14T19:01:53.183Z
Esa Pulkkinen
<p>AFAIK &quot;type theory&quot; doesn't care about those problems (there are no classes there, anyway :-), but you can always encode those things into a new <code>cast_to_A</code> method whose implementation in <code>B</code> returns something like <code>null</code> and that is overridden with an &quot;identity method&quot; in <code>A</code>.</p>
<p>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.</p>

CC BY-SA 4.0
2023-05-30T15:29:22.700Z
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?
nullUser
CC BY-SA 4.0
2023-05-30T14:25:22.097Z
2023-05-30T14:25:22.097Z
Stefan
<p>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.</p>
<p>Suppose I have types <code>A &lt; B</code> and <code>C</code> as in the following Python pseudo-code.</p>
<pre><code>class C:
    ...

class B:
    def b_func() -&gt; C:
        ...

class A(B):
    def a_func() -&gt; C:
        ...
</code></pre>
<p>Further suppose I have a function</p>
<pre><code>def f(b: B) -&gt; C
   ...
</code></pre>
<p>I am tempted to say &quot;It would be a type error to call <code>b.a_func()</code> inside <code>f</code>.&quot;</p>
<p>On the other hand, if the implementation of <code>f</code> looked like this</p>
<pre><code>def f(b: B) -&gt; C
    if isinstance(b, A):
        return b.a_func()
    else:
        return b.b_func()
</code></pre>
<p>then it appears the call to <code>b.a_func()</code> is perfectly fine.</p>
<p>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 &quot;It depends on what kind of type safety you are using, in ABC system only static information is allowed, so the <code>isinstance</code> check would be invalid in that system, whereas in XYZ type system the <code>isinstance</code> check is allowed. ...&quot;.</p>

CC BY-SA 4.0
2023-05-30T09:41:36.910Z
*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.
Martin Berger
CC BY-SA 4.0
2023-05-30T15:25:17.290Z
@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?
nullUser
CC BY-SA 4.0
2023-05-30T20:09:32.550Z
The tags are fine. This is a genuine type-theoretic Q.
Martin Berger
CC BY-SA 4.0
2023-05-31T19:05:10.053Z
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.
Martin Berger
CC BY-SA 4.0
2023-05-31T20:02:09.837Z
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.
Andrej Bauer
<type-theory><type-systems>
How is runtime downcasting modeled in type theory?
nullUser
# How is runtime downcasting modeled in type theory?

(Asked by: username_0 on 2023-05-29)

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

**Tags:** type-theory, type-systems

> **Comments:**
> **username_1**: *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.  
> **username_0**: @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?  
> **username_1**: The tags are fine. This is a genuine type-theoretic Q.  
> **username_1**: 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.  
> **username_2**: 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.  

---

## 2 answers

### Answer by username_3 on 2023-06-14. Score: 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 by username_4 on 2023-05-30. Score: 0

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.

> **Comments:**
> **username_0**: 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?  

---

