5
$\begingroup$

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.

$\endgroup$
14
  • $\begingroup$ 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. $\endgroup$ Commented Feb 10, 2024 at 13:11
  • $\begingroup$ I'm a but rusty with Java, but isn’t final just a restriction on a class itself, not the type of its values? $\endgroup$ Commented Feb 10, 2024 at 13:21
  • 4
    $\begingroup$ @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? $\endgroup$ Commented Feb 10, 2024 at 15:38
  • 1
    $\begingroup$ @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. $\endgroup$ Commented Feb 10, 2024 at 19:54
  • 1
    $\begingroup$ 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.) $\endgroup$ Commented Feb 11, 2024 at 21:05

1 Answer 1

Reset to default
3
$\begingroup$

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 {}).

$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$ Commented Feb 20, 2024 at 17:47
  • 1
    $\begingroup$ @feldentm Where does an uninhabited value need to be created? $\endgroup$ Commented Feb 20, 2024 at 19:25
  • $\begingroup$ @DavidYoung if you perform a CT evaluation of an expression, you need a value to operate on, right? $\endgroup$ Commented Feb 22, 2024 at 17:54
  • $\begingroup$ @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. $\endgroup$ Commented Feb 22, 2024 at 18:19
  • 1
    $\begingroup$ @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). $\endgroup$ Commented Feb 24, 2024 at 18:43

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.