PolyFunType syntax consistency with TypeLambda

azolotko · June 8, 2019, 8:35pm

Hi everyone. I was wondering, why it was decided to use => in
PolyFunType :: = HKTypeParamClause '=>' Type?

Wouldn’t it be better if it was consistent with type lambdas?

For example,

[T <: AnyVal] =>> List[T] => List[(T, T)]

instead of current

[T <: AnyVal] => List[T] => List[(T, T)]

After all, =>> is for types and => is for terms, aren’t they?

LPTK · June 11, 2019, 2:50pm

Hi @azolotko. It is indeed tempting to try and bring the different lambda syntaxes more in line with each other. Unfortunately, your proposal would lead to ambiguities.
We need to be able to determine whether [A] => B => C denotes a polymorphic function value (i.e., the type corresponding to def f[A](b: B): C), or whether it denotes a type lambda (i.e., the type corresponding to type F[A] = B => C.
We currently solve the ambiguity by writing the latter [A] =>> B => C, and leaving the former as is.

azolotko · June 12, 2019, 5:21pm

Thank you. Could you please suggest where I can find explanation of why the distinction needs to be preserved? It seems if we apply some type to both types, we will get a type B => C in return. I feel like I lack understanding of some important part of Scala’s/Scala compiler’s design here.

LPTK · June 14, 2019, 12:55pm

One year ago, I proposed to unify the two concepts:

github.com/lampepfl/dotty

Comment by LPTK to [Proof of concept] Polymorphic function types

lampepfl:master ← dotty-staging:poly-functions

> using the same syntax is likely to confuse users Are you sure about that? A…fter all, aren't they conceptually the same? – and if so, I think having several syntaxes for the same thing would be the more confusing approach. At least in dependently-typed systems, there is no distinction. So _in principle_ they could indeed be unified. Now, the question is: would that really work for Scala? About giving values higher-kinded types, according to you is there a fundamental difference between these two? ```scala trait A0 { val a: [T] -> a[T] ; type a[T] } // ^ using the syntax of your PR trait A1 { val a: [A] => a[T] ; type a[T] } // i.e.: trait A1 { val a: a ; type a[T] } // ^ using the unified approach ```

The main arguments against, IIRC, were:

It could be confusing for users (though personally, I’m not sure it would be more confusing than having different lambda syntaxes).
It would require some measure of kind polymorphism, and would probably not be easy to implement in the compiler. See @smarter’s message in the discussion mentioned above:

in this PR, the type [T] -> A => B is a subtype of Any , whereas with real polymorphic values it would be a subtype of [T] => Any

Note that currently, only a few rather arcane dependent subtype systems unify the two concepts, so it’s not so much of an obvious thing to do.