Search code examples
scalatype-parametertype-constructor

Why do proper types Any and Nothing fit type constructor shape F[_] when they are different kinds?

Consider the following method which takes type parameter of * -> * kind

def g[F[_]] = ???

Why is the following not a syntax error

g[Any]       // ok
g[Nothing]   // ok

since

scala> :kind -v Any
Any's kind is A
*
This is a proper type.

scala> :kind -v Nothing
Nothing's kind is A
*
This is a proper type.

so Any and Nothing should be of wrong shape?

Solution

  • Quotes from Scala spec:

    For every type constructor 𝑇 (with any number of type parameters), scala.Nothing <: 𝑇 <: scala.Any.

    https://scala-lang.org/files/archive/spec/2.13/03-types.html#conformance

    Say the type parameters have lower bounds 𝐿1,…,𝐿𝑛 and upper bounds π‘ˆ1,…,π‘ˆπ‘›. The parameterized type is well-formed if each actual type parameter conforms to its bounds, i.e. πœŽπΏπ‘–<:𝑇𝑖<:πœŽπ‘ˆπ‘– where 𝜎 is the substitution [π‘Ž1:=𝑇1,…,π‘Žπ‘›:=𝑇𝑛].

    https://scala-lang.org/files/archive/spec/2.13/03-types.html#parameterized-types

    A polymorphic method type is denoted internally as [tps]𝑇 where [tps] is a type parameter section [π‘Ž1 >: 𝐿1 <: π‘ˆ1,…,π‘Žπ‘› >: 𝐿𝑛 <: π‘ˆπ‘›] for some 𝑛β‰₯0 and 𝑇 is a (value or method) type. This type represents named methods that take type arguments 𝑆1,…,𝑆𝑛 which conform to the lower bounds 𝐿1,…,𝐿𝑛 and the upper bounds π‘ˆ1,…,π‘ˆπ‘› and that yield results of type 𝑇.

    https://scala-lang.org/files/archive/spec/2.13/03-types.html#polymorphic-method-types

    So since Any and Nothing conform to upper and lower bounds of F[_] (namely, Any and Nothing correspondingly), g[Any] and g[Nothing] are legal.