scalascala-3higher-kinded-typesimpredicativetypes

In Scala 3, why is it sometimes possible to do impredicative type assignment?


Scala 3 is an impredicative language, it is generally impossible to assign higher kind to normal type (at the risk of triggering Girard's paradox), but in reality, some type assignment appears to be able to bypass this rule:

      trait Vec[T]

      type VV1 = Vec // paradox!

      type VV2 = [T] =>> Vec[T] // no paradox?

What are the differences between the last 2 lines? Why is the second one possible?


Solution

  • The second line is possible because language authors decided that type alias can contain type constructor for consistency. If List is a type despite not being a proper type, so can be a type alias if we want to be consistent. And if functions can be curried, partially applied or passed over, so can be types.

    trait Vec[T]
    
    type VV1 = Vec // not! a paradox, but shorthand for type VV1 = [T] =>> Vec[T]
    

    Second line is equal to third line:

    A parameterized type definition

    type T[X] = R
    

    is regarded as a shorthand for an unparameterized definition with a type lambda as right-hand side:

    type T = [X] =>> R
    

    A partially applied type constructor such as List is assumed to be equivalent to its eta expansion. I.e, List = [X] =>> List[X]. This allows type constructors to be compared with type lambdas.

    See specification for more details.