<p>Let us assume a language that has final with Java semantics, i.e. a final type cannot have subtypes. Further, let that language have a full lattice type theory with at least one bottom type, e.g. NoReturn marking unreachable code.</p>
<p>Now, from the perspective of type theory, is it sound to make use of a final property of a type or value. In the sense that if e.g. a <code>system.exit()</code> is observed, to use knowledge about bottom or final types during type inference or type checking?
Or is any rule that even considers final during type checking unsound?</p>
<p>Would the answer change if other concepts like intersection types are added to the language?</p>
<p>Edit: Adding an example to illustrate my issue.</p>
<p>Let us assume we have three types Top, F and Bottom.
The compiler of the hypothetical language allows inlining.
The inlining is used to create a substitution without adding more type theory.</p>
<p>If we have an F identity function <code>id(x : F) : F = x</code>, is it valid to assume that the type of x is always exactly F if F is final?</p>
<p>Edit2: This question is not about Java or the JVM.</p>

<types><object-oriented><type-inference><soundness>
Can final and full lattice type theory be combined?
CC BY-SA 4.0
2024-02-10T13:11:53.170Z
To add some context: What made me ask is that I discovered that a rule essentially saying the type of `3` is `IntegerLiteral` irrespective of the context seems to be unsound as it conflicts with a substitution rule that, to me, looks perfectly fine.
feldentm
CC BY-SA 4.0
2024-02-10T13:21:43.580Z
I'm a but rusty with Java, but isn’t `final` just a restriction on a class itself, not the type of its values?
MisterMiyagi
CC BY-SA 4.0
2024-02-10T15:38:42.170Z
@feldentm Can you expand one why you expect this to be possibly unsound? I also don't quite see where the unsoundness would happen in the comment with extra context. What substitution rule? In what way does it conflict?
David Young
CC BY-SA 4.0
2024-02-10T16:08:19.860Z
`final` has a few different meanings in Java. Here it should refer to the case as in `public final class A` where there couldn't be a `class B extends A`. [Example.](https://tio.run/##LY2xDsIgFEXn9iuenSDR/oBxd3Hq4GAcngUb6gMaoFXT8O2IpNPNzTm5d8QFD3aSZhSvlKb5QaqHpzJI0BN6DxdUBta62pAPGHIsVgnQGbEuOGWG2x3QDZ7/zar7@iB1a@fQThkGMqw5SyK7h6t1JHYNP2atLGs4gZHvcsP4ur2U@U/uMWYz1jGlHw)
user23013
CC BY-SA 4.0
2024-02-10T16:18:34.473Z
I don't think there is any significance of `final` in type theory. Maybe it's better to understand it as "you need permission X to create subclasses of it", but you never get permission X except for the built-in special cases.
user23013
CC BY-SA 4.0
2024-02-10T19:47:36.873Z
@user23013 I think your view is correct and the idea that I could make assumptions based on final or similar properties are simply wrong. Also, it seems that at least in my case, I need to extend soundness to any CT evaluation to get a semantic that is useful to me and allows me to implement a compiler and sanity checks that work in such cases.
feldentm
CC BY-SA 4.0
2024-02-10T19:54:37.390Z
@DavidYoung I think the `3` example was a bad one. While it was what made me ask the question, the relation to the question is that I consider the type final, but I equally consider type variables with that type as upper bound subtypes. The longer I think about it the less clarity remains if I should collapse the variable types if the bound contains one element (the final type) or if the behaviour is correct and my treatment of final is plain wrong which I currently consider more likely.
feldentm
CC BY-SA 4.0
2024-02-10T20:28:13.077Z
I've written a draft answer based on the observation that `final` forbids subclassing (i.e. overriding of members) but not subtyping, and in Java for example a final class `A` can have subtypes like a type parameter whose upper bound is `A`, or an intersection type `A & B`. But re-reading my draft, it's not clear that it actually answers your question, and I'm not sure what an answer should look like. I think there is an issue because your question seems to suppose that Java doesn't have intersection types, [but it does](https://docs.oracle.com/javase/specs/jls/se18/html/jls-4.html#jls-4.9).
kaya3
CC BY-SA 4.0
2024-02-11T07:40:40.460Z
@kaya3 I just tried to minimize the scope of required language features; I could extend it to `&` and `|` if that makes providing an answer easier as long as there is no answer. But, to me, it looked as if that should not be required if there are bottom types anyway.
feldentm
CC BY-SA 4.0
2024-02-11T21:05:38.070Z
Can you explain what it would mean to 'use' final for the purposes of type-checking?  In the case of your identity example, what does it mean for the type of x to be 'exactly F'?—I can see why this might matter for optimisation, but not typechecking.  (Further, even for optimisation purposes, the existence of bottoms would not let you violate the assumption that x is always exactly an F.)
Moonchild
CC BY-SA 4.0
2024-02-12T19:10:24.800Z
It means that it is assumed that any observable value of x would have exactly the type F. The relation to bottom types like NoReturn is that, while the statement remains true at runtime, it doesn't at compile time if a value of type NoReturn is substituted into x during an inline substitution. I.e. the statement still holds for actual execution but not for symbolic execution.
feldentm
CC BY-SA 4.0
2024-02-12T19:31:12.150Z
Can you give a complete example where type soundness seems like it doesn't hold in the system you have in mind? Or are you asking if such an example exists? Either way, it'd probably help to have all the relevant details of your system spelled out.
David Young
CC BY-SA 4.0
2024-02-12T20:11:41.013Z
I think I'm starting to understand what you mean. There's a conflict between (1) `final` not allowing subtypes and (2) because subtyping is a lattice by assumption here, `NoReturn` must be a subtype of every type. A `NoReturn` value should never be reached so this shouldn't matter at run-time. However, the type checker doesn't necessarily know this at compile-time.
David Young
CC BY-SA 4.0
2024-02-13T14:57:29.210Z
@DavidYoung Yes, I think that's the issue I faced. I think the bigger picture is that for real world projects, soundness should be extended to compile-time evaluations.
feldentm
<p>I think this is fine.</p>
<p>Normally with subtyping you have an open-world assumption: for some type <span class="math-container">$T$</span> you can’t assume that there’s no subtype <span class="math-container">$S \le T$</span>, so even if you know <span class="math-container">$x : T$</span>, you can’t for example eliminate dynamic dispatch of a method on <span class="math-container">$T$</span>, because it could be overridden by some <span class="math-container">$S$</span>. Whereas if <span class="math-container">$T$</span> is final, you can relax that assumption with the additional knowledge that there is no such <span class="math-container">$S$</span>.</p>
<p>Subtyping <span class="math-container">$S \le T$</span> is sound if there’s a typing of <span class="math-container">$x : S \vdash x : T$</span>, which represents an identity coercion—in other words, subtyping is witnessed by eta-expanded identity functions like <code>\case { False -&gt; False; True -&gt; True } :: Bool -&gt; Bool</code>. (The existence of a witness like this is sufficient but possibly stronger than necessary.)</p>
<p>So I believe it should be sound to combine finality with the presence of a bottom type, provided that you reinterpret <span class="math-container">$\nexists S &lt; T$</span> as saying that any subtype of <span class="math-container">$T$</span> must be <em>uninhabited</em>, so <span class="math-container">$S &lt; T \implies S = \bot$</span>. In that case, <span class="math-container">$x : \bot \vdash x : T$</span> holds trivially (by <code>absurd = \case {}</code>).</p>

CC BY-SA 4.0
2024-02-20T07:30:21.200Z
2024-02-25T18:51:45.513Z
2024-02-25T18:51:45.513Z
Jon Purdy
CC BY-SA 4.0
2024-02-20T17:47:56.403Z
While I respect the answer, my issue with it is that *uninhabited* would kind of require the compiletime elaboration to create an *uninhabited value* as a placeholder which, in turn, seems paradoxical to me.
feldentm
CC BY-SA 4.0
2024-02-20T19:25:05.723Z
@feldentm Where does an uninhabited value need to be created?
David Young
CC BY-SA 4.0
2024-02-22T17:54:35.327Z
@DavidYoung if you perform a CT evaluation of an expression, you need a value to operate on, right?
feldentm
CC BY-SA 4.0
2024-02-22T18:19:46.397Z
@feldentm Hmm, what do you mean by "CT evaluation"? Also, I think this answer is mainly saying that it *is* sound to do the combination you're describing, rather than prescribing specific implementation details.
David Young
CC BY-SA 4.0
2024-02-24T07:07:05.600Z
@DavidYoung I thinkt that the issue I faced that made me ask the question is that I could observe such values during symbolic interpretation during compilation of the program. At least for me, the takeaway is that the way I do symbolic execution requires me to extend the notion of soundness to the way I do this interpretation. Maybe I should provide such an answer but still accept this one as most people will likely be in this situation.
feldentm
CC BY-SA 4.0
2024-02-24T18:43:14.520Z
@feldentm Maybe the answer to this would involve more details than would be appropriate here, but wouldn't you still not need to construct values like that during symbolic execution since you know from their type that they cannot exist? If you ever are in a situation where you have an "uninhabited value," you should be able to do whatever you want without causing problems (since execution can never reach that place).
David Young
# Can final and full lattice type theory be combined?
Posted by: username_0 on 2024-02-10
Let us assume a language that has final with Java semantics, i.e. a final type cannot have subtypes. Further, let that language have a full lattice type theory with at least one bottom type, e.g. NoReturn marking unreachable code.

Now, from the perspective of type theory, is it sound to make use of a final property of a type or value. In the sense that if e.g. a `system.exit()` is observed, to use knowledge about bottom or final types during type inference or type checking?
Or is any rule that even considers final during type checking unsound?

Would the answer change if other concepts like intersection types are added to the language?

Edit: Adding an example to illustrate my issue.

Let us assume we have three types Top, F and Bottom.
The compiler of the hypothetical language allows inlining.
The inlining is used to create a substitution without adding more type theory.

If we have an F identity function `id(x : F) : F = x`, is it valid to assume that the type of x is always exactly F if F is final?

Edit2: This question is not about Java or the JVM.
**Tags:** types object-oriented type-inference soundness
> **Comments:**
> **username_0**: To add some context: What made me ask is that I discovered that a rule essentially saying the type of `3` is `IntegerLiteral` irrespective of the context seems to be unsound as it conflicts with a substitution rule that, to me, looks perfectly fine.  
> **username_1**: I'm a but rusty with Java, but isn’t `final` just a restriction on a class itself, not the type of its values?  
> **username_2**: @feldentm Can you expand one why you expect this to be possibly unsound? I also don't quite see where the unsoundness would happen in the comment with extra context. What substitution rule? In what way does it conflict?  
> **username_3**: `final` has a few different meanings in Java. Here it should refer to the case as in `public final class A` where there couldn't be a `class B extends A`. [Example.](https://tio.run/##LY2xDsIgFEXn9iuenSDR/oBxd3Hq4GAcngUb6gMaoFXT8O2IpNPNzTm5d8QFD3aSZhSvlKb5QaqHpzJI0BN6DxdUBta62pAPGHIsVgnQGbEuOGWG2x3QDZ7/zar7@iB1a@fQThkGMqw5SyK7h6t1JHYNP2atLGs4gZHvcsP4ur2U@U/uMWYz1jGlHw)  
> **username_3**: I don't think there is any significance of `final` in type theory. Maybe it's better to understand it as "you need permission X to create subclasses of it", but you never get permission X except for the built-in special cases.  
> **username_0**: @user23013 I think your view is correct and the idea that I could make assumptions based on final or similar properties are simply wrong. Also, it seems that at least in my case, I need to extend soundness to any CT evaluation to get a semantic that is useful to me and allows me to implement a compiler and sanity checks that work in such cases.  
> **username_0**: @DavidYoung I think the `3` example was a bad one. While it was what made me ask the question, the relation to the question is that I consider the type final, but I equally consider type variables with that type as upper bound subtypes. The longer I think about it the less clarity remains if I should collapse the variable types if the bound contains one element (the final type) or if the behaviour is correct and my treatment of final is plain wrong which I currently consider more likely.  
> **username_4**: I've written a draft answer based on the observation that `final` forbids subclassing (i.e. overriding of members) but not subtyping, and in Java for example a final class `A` can have subtypes like a type parameter whose upper bound is `A`, or an intersection type `A & B`. But re-reading my draft, it's not clear that it actually answers your question, and I'm not sure what an answer should look like. I think there is an issue because your question seems to suppose that Java doesn't have intersection types, [but it does](https://docs.oracle.com/javase/specs/jls/se18/html/jls-4.html#jls-4.9).  
> **username_0**: @kaya3 I just tried to minimize the scope of required language features; I could extend it to `&` and `|` if that makes providing an answer easier as long as there is no answer. But, to me, it looked as if that should not be required if there are bottom types anyway.  
> **username_5**: Can you explain what it would mean to 'use' final for the purposes of type-checking?  In the case of your identity example, what does it mean for the type of x to be 'exactly F'?—I can see why this might matter for optimisation, but not typechecking.  (Further, even for optimisation purposes, the existence of bottoms would not let you violate the assumption that x is always exactly an F.)  
> **username_0**: It means that it is assumed that any observable value of x would have exactly the type F. The relation to bottom types like NoReturn is that, while the statement remains true at runtime, it doesn't at compile time if a value of type NoReturn is substituted into x during an inline substitution. I.e. the statement still holds for actual execution but not for symbolic execution.  
> **username_2**: Can you give a complete example where type soundness seems like it doesn't hold in the system you have in mind? Or are you asking if such an example exists? Either way, it'd probably help to have all the relevant details of your system spelled out.  
> **username_2**: I think I'm starting to understand what you mean. There's a conflict between (1) `final` not allowing subtypes and (2) because subtyping is a lattice by assumption here, `NoReturn` must be a subtype of every type. A `NoReturn` value should never be reached so this shouldn't matter at run-time. However, the type checker doesn't necessarily know this at compile-time.  
> **username_0**: @DavidYoung Yes, I think that's the issue I faced. I think the bigger picture is that for real world projects, soundness should be extended to compile-time evaluations.  
---
## 1 answers
### Answer by username_6 on 2024-02-20. Score: 3 | Accepted answer
I think this is fine.

Normally with subtyping you have an open-world assumption: for some type $T$ you can’t assume that there’s no subtype $S \le T$, so even if you know $x : T$, you can’t for example eliminate dynamic dispatch of a method on $T$, because it could be overridden by some $S$. Whereas if $T$ is final, you can relax that assumption with the additional knowledge that there is no such $S$.

Subtyping $S \le T$ is sound if there’s a typing of $x : S \vdash x : T$, which represents an identity coercion—in other words, subtyping is witnessed by eta-expanded identity functions like `\case { False -> False; True -> True } :: Bool -> Bool`. (The existence of a witness like this is sufficient but possibly stronger than necessary.)

So I believe it should be sound to combine finality with the presence of a bottom type, provided that you reinterpret $\nexists S < T$ as saying that any subtype of $T$ must be *uninhabited*, so $S < T \implies S = \bot$. In that case, $x : \bot \vdash x : T$ holds trivially (by `absurd = \case {}`).
> **Comments:**
> **username_0** (2024-02-20): While I respect the answer, my issue with it is that *uninhabited* would kind of require the compiletime elaboration to create an *uninhabited value* as a placeholder which, in turn, seems paradoxical to me.  
> **username_2** (2024-02-20): @feldentm Where does an uninhabited value need to be created?  
> **username_0** (2024-02-22): @DavidYoung if you perform a CT evaluation of an expression, you need a value to operate on, right?  
> **username_2** (2024-02-22): @feldentm Hmm, what do you mean by "CT evaluation"? Also, I think this answer is mainly saying that it *is* sound to do the combination you're describing, rather than prescribing specific implementation details.  
> **username_0** (2024-02-24): @DavidYoung I thinkt that the issue I faced that made me ask the question is that I could observe such values during symbolic interpretation during compilation of the program. At least for me, the takeaway is that the way I do symbolic execution requires me to extend the notion of soundness to the way I do this interpretation. Maybe I should provide such an answer but still accept this one as most people will likely be in this situation.  
> **username_2** (2024-02-24): @feldentm Maybe the answer to this would involve more details than would be appropriate here, but wouldn't you still not need to construct values like that during symbolic execution since you know from their type that they cannot exist? If you ever are in a situation where you have an "uninhabited value," you should be able to do whatever you want without causing problems (since execution can never reach that place).  
---
