Irregular type inference for `Nothing`

Type inference for Nothing does not always follow the usual rules. According to Martin Odersky:

If a type variable X with an upper bound needs to be instantiated, and the lower bound is Nothing, the upper bound is taken instead.

The quote above comes from the discussion on the issue I opened about it because I thought it was a compiler bug.

I do not know the use cases for the exceptional treatment of Nothing when it comes to type inference. However, my language design sense tells me that such ad-hoc rules usually do more harm than good.

It superficially reminds me of void in Java that has to be treated differently from other types, rather than being recognized as the regular Unit type. The latter is of course much worse, as it does not only affect type inference.

Still, I hope it is not too late to fix this irregularity in the Scala 3 type inference logic.

Below is a motivating toy example (already mentioned in this discussion) illustrating how the ad-hoc inference rule for Nothing can be detrimental in practice:

// This code represents part of the HOAS of an object language
// (let's call it OL) using Scala types.

// Upper bound of all Scala types used to represent syntactic sorts of OL
sealed trait CodeType

// Upper bound of all Scala types used to represent types in OL
sealed trait ValTop

// Lower bound of all Scala types used to represent types in OL
type ValBot = Nothing
// Note that Nothing is the only expressible valid lower bound.

// Scala type to represent OL expressions
sealed trait Expr[+T <: ValTop] extends CodeType

// Scala type to represent OL patterns
sealed trait Ptrn[+P <: N, -N <: ValTop] extends CodeType

// Scala type to represent OL values
// Values are expressions, and can also be used in patterns.
sealed trait Val[+T <: ValTop] extends Expr[T], Ptrn[T, ValTop]

// Scala type to represent OL cell references
// Example of a higher-kinded type with an invariant parameter
final case class CellRef[T <: ValTop](name: String) extends ValTop, Val[CellRef[T]]
// Due to invariance, no other lower bound is expressible.

// Scala type to represent OL pairs
final case class Pair[+T1 <: ValTop, +T2 <: ValTop](
  t1: Val[T1],
  t2: Val[T2],
) extends ValTop, Val[Pair[T1, T2]]

// Scala type to represent an OL wildcard pattern
case object Ignore extends Ptrn[ValBot, ValTop]
type Ignore = Ignore.type

// Scala type to represent OL pair patterns
final case class MatchPair[
  +P1 <: N1,
  +P2 <: N2,
  -N1 <: ValTop,
  -N2 <: ValTop,
  +L <: Pair[P1, P2],
  -U >: Pair[N1, N2] <: ValTop,
](
  t1: Ptrn[P1, N1],
  t2: Ptrn[P2, N2],
)(using
  // This additional constraint represents the unification
  // equation    L | Pair[ValBot, ValBot]  ==  Pair[P1, P2],
  // meant to define the variable L.
  Pair[P1, P2] <:< (L | Pair[ValBot, ValBot]),
  // This additional constraint represents the unification
  // equation    U & Pair[ValTop, ValTop]  ==  Pair[N1, N2],
  // meant to define the variable U.
  (U & Pair[ValTop, ValTop]) <:< Pair[N1, N2],
) extends Ptrn[L, U]

// Because of the abnormal treatment of Nothing by Scala, this pattern cannot be
// expressed without explicitly specifying the type arguments.
val pattern: Ptrn[ValBot, ValTop] = MatchPair[
  ValBot, // Boilerplate due to irregular type inference
  ValBot, // Boilerplate due to irregular type inference
  ValTop, // Boilerplate due to irregular type inference
  ValTop, // Boilerplate due to irregular type inference
  ValBot, // Boilerplate due to irregular type inference
  ValTop, // Boilerplate due to irregular type inference
](Ignore, Ignore)

Yes, Nothing is special.

You might want to read Programming in Scala, 5th Edition Chapter 7.4 “Exception Handling” and Chapter 17.3, “Bottom types”.

Nothing is used as the type for exceptions (for one), and no value of type Nothing can be instantiated, so that when a branch of some expression throws an exception, while the other branch is, say, Int, then the whole expression type-checks. This is a price to pay for combining FP + OOP + Imperative… (Note that throwing an exception is different than Unit.)

What Martin describes makes sense to me: if all you have is Nothing as a lower-bound and, say, T as an upper-bound, it makes sense to infer T instead of Nothing. Inferring Nothing would be “smashing” the type lattice all the way down, losing valuable type information in the middle and near the top (way too much narrowing). Nothing is clearly not the intention there.

If we changed the rule to infer Nothing instead of T then it would be detrimental for many other cases that need wider type inference. Those are a lot more frequent. Again, it’s a trade-off decision…

In Scala you can express the lower bound of two types, and that’s definitely not Nothing, it sits above Nothing as a greatest lower bound. But yes… there isn’t a way to express an “infinite intersection” (which still may not be Nothing). For that kind of mechanism you might want to look into other languages like Agda or Idris (with generalized product types), or Haskell with some language extensions, but those languages don’t have subtyping…

Anyway good luck on your pursuits! :wink:

I don’t dispute that, but that is not what this post is about.

I don’t have the book.

That is exactly what one would expect from Nothing. Nothing being an extreme type (the smallest) does not imply the need for any ad-hoc inference rules.

I don’t see any price there. Exceptions can and should be of type Nothing, since they never actually evaluate to a value; it’s their natural (i.e. tightest) type.

Note that no value being of type Nothing does not mean that it’s somehow a second-class type. Nothing can be used as a type parameter just like any other type, and is actually particularly useful as the universal lower bound on types, on par with its dual, Any.

It’s the opposite, actually. Not inferring the tightest type is a loss of information. As you can see in my example, due to this rule, Nothing is not inferred even when in a covariant position (+P1, +P2). Inferring any other type in this context strictly loses information. That is why the code does not compile when the type arguments to MatchPair are not explicitly provided.

It is clearly the intention in my code.

Do you have any example?

How would you know that? There is no way to know how often normal inference for Nothing would be used, since it is currently unusable.

Also, statistic arguments seem rather weak. One could similarly argue that 2420394852309L is a very rarely used number, so it would be fine to drop support for it in order to improve Long performance, which are used all the time. To me, it seems more important to have a regular language, even for rarely-used features.

In my experience, when it comes to language design, most trade-offs are actually artificial, and due to earlier imperfect decisions, or an inability to address the issue more deeply.

Exactly, so lower bounds are not as relevant for them, and modeling the typing rules of a language with subtyping in them would be rather less natural. In any case, this post is about type inference in Scala.

Thank you! However, this post really isn’t about them (though it is motivated by them), but about Scala.

1 Like

Thanks for the response!

I disagree with your views, especially Nothing being the tightest (which it isn’t), which should be the greatest lower bound (the “infinite intersection”), not Nothing. That’s the tightest, Nothing would be… “loosest” or “smallest” lower bound.

It’s not a “second class type”, it just makes more sense to infer T instead of Nothing. In fact it’s like that with lower bounds in general. Subtyping makes type inference very difficult. In many cases it’s very useful to infer the upper-bound. (Yes yes I know I can’t prove what I’m saying because statistical argument…) There are some situations where inferring the lower bound makes more sense too, it’s just that Nothing is not one of them.

Your issue is with the lack of this infinite intersection type, not with Nothing. If your project required you to have an “infinite union” type and you ran into a similar issue, then you would ask for a different priority in inference (Any maybe?).

But anyway, not much of a point in debating it back and forth… we are in very clear disagreement. Good luck convincing the language designers! Personally I hope Scala stays the way it is (I would not want Nothing being inferred like that).

I should say one thing, and I’m probably wrong here: I see many of your posts where you keep trying to make Scala do things that its type system is not well-suited to do. That’s why I suggested other languages that have far more powerful type systems. (Yes yes I know this post is about Scala…) Scala is great for what it’s designed to do; it’s OK that it’s not capable of some things.

You are right, Nothing is the loosest lower bound. But, dually, it is the tightest instantiation of a covariant type parameter. The rule being discussed is about type inference, which is about instantiation of types, rather than type bounds.

It is not. This rule is specific to Nothing. In fact, this rule does not apply when the upper bound is Any (unless it is explicitly specified via a type alias, see the issue).

I would like to see the reasoning behind when and why it makes sense to infer upper or lower bounds.

The two are related, and I would like to have infinite intersection types (which would provide an alternative solution for my project). However, this post is not about them. It is about an irregularity in type inference related to Nothing. If Any causes similar irregularities in type inference, then I guess it makes sense to discuss them in this thread as well, but I am not aware of any (no pun intended).

I am not aware of other somewhat mainstream languages that clearly have a far more powerful type system. Subtyping is pretty powerful, particularly when combined with all the other features of the Scala type system.

By the way, thank you for being so active replying on the Scala forums! It makes them a better place.

2 Likes

I just thought of perhaps a clearer way to express the issue. Below is a principle that seems natural:

The tightening of an upper / lower type bound of a covariant / contravariant type parameter should never loosen its inference.

In other words, for the covariant case, given a parametrized type A[+T <: U1], U1 >: U2, and a context in which T gets inferred to be I1, it should never be the case that, when A’s upper bound is tightened to U2, (i.e. A[+T <: U2]), T gets inferred to some different I2, not satisfying I2 <: I1, in the same context.

If that principle sounds unreasonable to anyone, I’d love to hear about it.

The irregular type inference mentioned in this thread not only violates this principle, but further violates type alias transparency, by having inference behave differently when the same upper bound (in this case, Any) is provided via an alias.

Hopefully, someone from the Scala team can chime in.

I have some trouble wrapping my head around this, could you give an example ?
(With what you would like, and what happens currently)

1 Like

The issue I mentioned earlier contains one such example. I copied a simplified version below.

The code below compiles fine.

// Wrap's type parameter correctly gets inferred to Nothing.
Wrap(new A[Nothing]{})

final case class Wrap[+T](first: A[T])(using A[T] <:< A[Nothing])

sealed trait A[+T]

When an upper bound is added, the code does not compile anymore:

// Wrap's type parameter gets inferred to U, leading to the compile-error
// "Cannot prove that A[U] <:< A[Nothing].".
Wrap(new A[Nothing]{})

// Wrap's type parameter now is upper-bounded by U.
final case class Wrap[+T <: U](first: A[T])(using A[T] <:< A[Nothing])

sealed trait A[+T]

// Any other type bound (except "Nothing") leads to the same error.
type U = Any

This violates the aforementioned principle, as the addition of an explicit upper type bound U <: Any (even if that bound is actually Any, as in the example) loosens the type inference of Wrap’s type parameter from Nothing to U.

2 Likes

And Wrap(new A[Int]{}) always works, correct ?