<p>Context:
Let us assume a full-lattice type theory with at least types <code>any</code>, <code>bool</code>, <code>Exception</code>, <code>SpecificException</code>, <code>WillThrow</code> and <code>NoReturn</code>.
Here, the Exception sub half lattice contains <code>Exception</code> and <code>SpecificException</code>.</p>
<p>A function's return type <code>bool</code> would express that if the function returns, it returns a bool, but it may throw or not return. <code>WillThrow</code> means that it may throw or not return. <code>NoReturn</code> means that it does not throw and does not return.</p>
<p><strong>Question</strong>:
Can <code>WillThrow</code> take a covariant type parameter <code>T</code> to restrict the type that the thrown exception can have?</p>
<p>Examples:</p>
<pre><code>f = true // implicitly bool, ok
g : bool = throw Exception // explicitly bool, ok
h = throw Exception // explicitly WillThrow[Exception], ok
i : WillThrow[Exception] = throw SpecificException // ok
j : WillThrow[SpecificException] = throw Exception // not ok
</code></pre>

<types><object-oriented><type-inference><exceptions>
Can WillThrow as a Bottom Type of a Full-Lattice Type Theory take the thrown Exception Type as Covariant Type Argument?
CC BY-SA 4.0
2024-10-28T14:00:59.643Z
To be clear, `WillThrow` would not be a bottom type; if anything, `NoReturn` would be, because any function which never returns and never throws, can be used in place of any other function which is allowed to throw or return (but isn't required to). But if `WillThrow[E]` and `NoReturn` are only allowed as function return types, and not in other places where types would normally occur, then they aren't even obviously types.
kaya3
CC BY-SA 4.0
2024-10-28T14:08:01.863Z
For example, `NoReturn` is defined to be equivalent to `WillThrow[never]` where `never` is a bottom type. But `WillThrow[NoReturn]` doesn't make sense.
kaya3
CC BY-SA 4.0
2024-10-28T19:36:24.633Z
@kaya3 they both are bottom types; WillThrow[E] would result in an infinite sub half lattice of bottom types that has no bottom type on its own. Willthrow[never] in the sense of nothrow is identical to NoReturn. TBH, I do not get the comment on types and likely do not share your position on what that word means if that statement can be true. A consequence would be that void or Top equally aren't types.
feldentm
CC BY-SA 4.0
2024-10-28T20:45:34.410Z
Well, a bottom type must be a subtype of all other types. If `NoReturn` is a type then `WillThrow[Exception]` is not a bottom type, since it is not a subtype of `NoReturn`. Likewise `WillThrow[Exception]` is not a subtype of `WillThrow[SpecificException]`, so the former cannot be a bottom type.
kaya3
<p>Firstly, how could it be useful? Not only does it guarantee the code following it will not be executed, it also says it will never throw exceptions other than the specified one. It's natural to think, to make it cover every case, you would also want types for functions that return a specific type, but also would never throw exceptions other than the specified ones, i.e. the Java way of specifying throwable exceptions. With also this feature, your problem is solved automatically.</p>
<p>But how could it be implemented if the language does not require the programmers to specify every throwable exceptions? Let's just move it to a dynamically typed language. Statically, could it have a function that is labeled to be only able to throw specific exceptions, even if exceptions from subroutine calls might be unmarked? Yes, we don't care about anything statically. What happens if it throws another exception anyway, and caused a type error? It... throws another exception. That's the source of the feel of inconsistency. But starting from here, there are many ways you could consider:</p>
<ul>
<li>To have multiple levels of exceptions. Specifications of exceptions only cover the lower levels. It would correctly mark catch routines of other exceptions unreachable, until the first catch routine of higher level exceptions. So it does make a difference.</li>
<li>To make it possible to catch this exception mismatch exception, and this exception rethrown from the catch routine, and so on. If it is not caught for the last time, it is a fatal.</li>
<li>Just make it a special case.</li>
</ul>

CC BY-SA 4.0
2024-10-29T07:15:01.407Z
2024-10-29T07:15:01.407Z
user23013
CC BY-SA 4.0
2024-10-29T07:52:58.543Z
"the Java way of specifying throwable exceptions" I think Java goes a step further by requiring the specified exceptions to be handled immediately in the callee. Most people complaining about the feature seem to mind only the latter.
MisterMiyagi
CC BY-SA 4.0
2024-10-29T11:35:55.300Z
@MisterMiyagi With things like anonymous functions being used more frequently, it's not likely there will be a lot of people who like this feature, even if they didn't complain. But here I didn't say Java is right or wrong, but the feature is needed to make it consistent with OP's idea, whether it is really like Java, optional, or auto-deduced.
user23013
CC BY-SA 4.0
2024-10-29T12:08:44.617Z
@MisterMiyagi Java doesn't require exceptions to be handled immediately in the callee. It only requires that (checked) exceptions be declared if they can be thrown immediately or transitively by another function call. So if `foo` calls `bar` and `bar` throws `BarException` then `foo` must declare `BarException` if it doesn't catch it. If that weren't required then there would be no sense in declaring exceptions at all, because you could get out of declaring them by wrapping the `throw` in some other call.
kaya3
# Can WillThrow as a Bottom Type of a Full-Lattice Type Theory take the thrown Exception Type as Covariant Type Argument?
Posted by: username_0 on 2024-10-27
Context:
Let us assume a full-lattice type theory with at least types any, bool, Exception, SpecificException, WillThrow and NoReturn.
Here, the Exception sub half lattice contains Exception and SpecificException.
A function's return type bool would express that if the function returns, it returns a bool, but it may throw or not return. WillThrow means that it may throw or not return. NoReturn means that it does not throw and does not return.
Question:
Can WillThrow take a covariant type parameter T to restrict the type that the thrown exception can have?
Examples:
f = true // implicitly bool, ok
g : bool = throw Exception // explicitly bool, ok
h = throw Exception // explicitly WillThrow[Exception], ok
i : WillThrow[Exception] = throw SpecificException // ok
j : WillThrow[SpecificException] = throw Exception // not ok
**Tags:** types object-oriented type-inference exceptions
> **Comments:**
> **username_1**: To be clear, `WillThrow` would not be a bottom type; if anything, `NoReturn` would be, because any function which never returns and never throws, can be used in place of any other function which is allowed to throw or return (but isn't required to). But if `WillThrow[E]` and `NoReturn` are only allowed as function return types, and not in other places where types would normally occur, then they aren't even obviously types.  
> **username_1**: For example, `NoReturn` is defined to be equivalent to `WillThrow[never]` where `never` is a bottom type. But `WillThrow[NoReturn]` doesn't make sense.  
> **username_0**: @kaya3 they both are bottom types; WillThrow[E] would result in an infinite sub half lattice of bottom types that has no bottom type on its own. Willthrow[never] in the sense of nothrow is identical to NoReturn. TBH, I do not get the comment on types and likely do not share your position on what that word means if that statement can be true. A consequence would be that void or Top equally aren't types.  
> **username_1**: Well, a bottom type must be a subtype of all other types. If `NoReturn` is a type then `WillThrow[Exception]` is not a bottom type, since it is not a subtype of `NoReturn`. Likewise `WillThrow[Exception]` is not a subtype of `WillThrow[SpecificException]`, so the former cannot be a bottom type.  
---
## 1 answers
### Answer by username_2 on 2024-10-29. Score: 0
Firstly, how could it be useful? Not only does it guarantee the code following it will not be executed, it also says it will never throw exceptions other than the specified one. It's natural to think, to make it cover every case, you would also want types for functions that return a specific type, but also would never throw exceptions other than the specified ones, i.e. the Java way of specifying throwable exceptions. With also this feature, your problem is solved automatically.

But how could it be implemented if the language does not require the programmers to specify every throwable exceptions? Let's just move it to a dynamically typed language. Statically, could it have a function that is labeled to be only able to throw specific exceptions, even if exceptions from subroutine calls might be unmarked? Yes, we don't care about anything statically. What happens if it throws another exception anyway, and caused a type error? It... throws another exception. That's the source of the feel of inconsistency. But starting from here, there are many ways you could consider:

* To have multiple levels of exceptions. Specifications of exceptions only cover the lower levels. It would correctly mark catch routines of other exceptions unreachable, until the first catch routine of higher level exceptions. So it does make a difference.
* To make it possible to catch this exception mismatch exception, and this exception rethrown from the catch routine, and so on. If it is not caught for the last time, it is a fatal.
* Just make it a special case.
> **Comments:**
> **username_3** (2024-10-29): "the Java way of specifying throwable exceptions" I think Java goes a step further by requiring the specified exceptions to be handled immediately in the callee. Most people complaining about the feature seem to mind only the latter.  
> **username_2** (2024-10-29): @MisterMiyagi With things like anonymous functions being used more frequently, it's not likely there will be a lot of people who like this feature, even if they didn't complain. But here I didn't say Java is right or wrong, but the feature is needed to make it consistent with OP's idea, whether it is really like Java, optional, or auto-deduced.  
> **username_1** (2024-10-29): @MisterMiyagi Java doesn't require exceptions to be handled immediately in the callee. It only requires that (checked) exceptions be declared if they can be thrown immediately or transitively by another function call. So if `foo` calls `bar` and `bar` throws `BarException` then `foo` must declare `BarException` if it doesn't catch it. If that weren't required then there would be no sense in declaring exceptions at all, because you could get out of declaring them by wrapping the `throw` in some other call.  
---
