[Proof of concept] Polymorphic function types

[smarter]

EDIT: Everything below is still valid but the syntax has changed from -> to =>.

This is a sketch of how polymorphic function types could be implemented in Dotty, this PR adds types that look like:

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

and a way of writing values of these types:

val f = [T <: AnyVal] -> (x: List[T]) => x.map(e => (e, e))

Just like P => R has a method def apply(x: A): B, [T] => P => R has a method def apply[T](x: P): R (in fact, it doesn't have any other method). Behind the scene, this is erased to a regular scala.FunctionN, see the commit messages for more details.

This PR isn't complete, this is just a quick experiment done in a few hours. In particular, I haven't tried to work out how this interact with implicit/erased/dependent function types and SAM types. I also haven't tried to implement polymorphic eta-expansion yet, e.g. given:

def foo(x: [T] -> T => Option[T]): Unit

we'd like to be able to write:

foo(Some)

but for now you'll have to write:

foo([T] -> (x: T) => Some(x))

[smarter]

@SystemFw has a pretty interesting usecase he presents in https://gist.github.com/SystemFw/256205f51bf0135e4c6fd95dee4590fc, I've verified that it can be implemented with this PR: https://gist.github.com/smarter/9a28e39dfaf0235e9d0a16b09ff8a9a4 (would be nice to minimize this to a zero-dependency file that we can add to our test suite).

[Glavo]

Why use -> instead of =>? I think that -> is just an ordinary identifier and is not suitable for use here.

[smarter]

Yeah I'm not sure about the syntax, this is just a placeholder that works. Currently we can't use => because it conflicts with type lambdas (like [X] => List[X]).

[LukaJCB]

Another use case is for abstracting over tagless final programs and interpreters.
As soon as you try doing that currently, you’ll realize it’s impossible to get the type for a tagless final program without wrapping.
With implicit function types and rank-N-types we can now do it like this:

type Program[Alg[_[_]], A] = [F[_]: Applicative] -> Alg[F] => F[A]

This is super useful for e.g. optimizing tagless final programs. It means that now I can write this general function:

def optimize[Alg[_[_]], F[_]: Applicative, A, M: Monoid]
  (program: Program[Alg, A])
  (extract: Alg[Const[M, ?]])
  (rebuild: (M, Alg[F]) =>  F[Alg[F]]): Alg[F] => F[A] = { (interpreter: Alg[F]) =>
    val m: M = p(extract).getConst

    rebuild(m, interpreter).flatMap(newInterp => program(newInterp))
}

And that is basically what I did in sphynx, though there I still have to wrap every program in an extra wrapper. So this would really help immensely in that regard!

[LPTK]

@smarter would you agree that using -> for type functions and leaving => for value functions (for both type and value parameters) would be more homogeneous?
I've always found the [T] => ... type lambda syntax rather confusing, as to me => is the visual marker of normal function types.

[smarter]

@LPTK we're still hoping to get some sort of effect system in Dotty, and we were planning to use A -> B to mean "pure function" (whereas A => B would be retrofitted to mean "function with an arbitrary effect"). Maybe we can find another syntax but we're running out of arrows.

[LPTK]

@smarter I see.

BTW, why not use type lambdas to represent polymorphic function types (or any polymorphic types really)? So we'd allow values to have higher-kinded types.

Even if that wouldn't work with the current compiler's infrastructure, does the user need to know they are different? What would happen if we used the same syntax for both, letting the compiler distinguish based merely on the context where the type appears?

[smarter]

I think using the same syntax is likely to confuse users, it's also not clear that we can always distinguish between them based on the context. We could maybe look at the kind of the expected type if we have one, but what if there's no expected type? If we enable kind polymorphism in the compiler things would get even more muddled.

[LPTK]

using the same syntax is likely to confuse users

Are you sure about that? After 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?

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

[smarter]

The main difference is in that 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. This means that abstracting over these things would require kind polymorphism, it's a much bigger conceptual leap, and likely to have far-reaching consequences.

[Glavo]

Will types like [A] -> A be supported?

[milessabin]

@smarter seeing as kind polymorphism is on the table, I think we should be seeing if we can take advantage of it here.

[smarter]

Will types like [A] -> A be supported?

To be decided, [A] -> () => A is already supported and makes it clearer that there's a method call involved. On the other hand it's a bit verbose.

seeing as kind polymorphism is on the table, I think we should be seeing if we can take advantage of it here.

Can you think of examples that shows things we could only do, or do better, by taking advantage of kind polymorphism here?

[milessabin]

Can you think of examples that shows things we could only do, or do better, by taking advantage of kind polymorphism here?

@smarter I was responding to your comment,

The main difference is in that 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. This means that abstracting over these things would require kind polymorphism, it's a much bigger conceptual leap, and likely to have far-reaching consequences.

[smarter]

@milessabin Yes, I got that. I mean that if we were to go down that road, it would have to be because it presents significant practical advantages, not just because it's conceptually elegant, since it's likely to be extremely complex to implement and specify.

[Blaisorblade]

BTW, why not use type lambdas to represent polymorphic function types (or any polymorphic types really)? So we'd allow values to have higher-kinded types.

Are you sure about that? After 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.

No they aren't, even tho the difference is subtle (I've been confused for years), but they're clearly distinct things in Haskell Agda Coq Idris... The only system merging them doesn't look compatible with kind polymorphism — not because of a soundness hole, but because it's not clear at all what List would mean there. And what about List => List? Is that ([A] -> List[A]) => ([A] -> List[A]) or [A] -> List[A] => List[A]?

This is not an impossibility result, but absent some extraordinarily compelling argument, I strongly believe we should follow ~50 years of PL theory instead of doing something different here.

So, the correct question is "please find a pretty compelling reason for merging these very different things". And I encourage you to find fault with the existing distinction in languages that have it. In a separate issue, please.

==

Polymorphic function types (which I'll write for now with the existing MethodType syntax [A]List[A]) and type lambdas ([A] => List[A]) are two very different things in theory and practice. The only thing in common is that they bind a type variable A in some type T. But one is a value type (a type of functions), the other only maps value types to value types, that is, it becomes a value type after you apply it to some argument.

There's basically one pretty hairy paper that uses the same type [A]List[A] for both things, but then, each time you use such a type, you must check if you use it at kind * or * -> * to know if you actually meant "polymorphic function type" or "type lambda". Since kind polymorphism lets you upcast [A]List[A] to kind AnyKind forgetting that bit of info, I'd say that identifying polymorphic functions and type functions is incompatible with kind polymorphism.

The main difference is in that 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

IIUC, the subtypes of [T] => Any are type functions, not "real polymorphic values" — I'd love to be corrected if I'm missing something here. And in fact, arguably List would be a subtype of both Any and [T] => Any if it can be used in both roles, which doesn't look any pleasant.

[smarter]

No they aren't, even tho the difference is subtle (I've been confused for years)

Same here, so you should disregard everything I said and listen to @Blaisorblade :)

[LPTK]

@Blaisorblade thanks for the answer. You're right, I think I was confused too.

When looking at the JFP'05 paper on Idris, in the syntax definition on page 560, we can see there is indeed a syntax for functions (lambda abstractions such as \x => x+1 and \tp => List tp) and function spaces for writing the types of such expressions (respectively Int -> Int and Type -> Type). In Scala's type language, the first corresponds to [A] => T and the second to the dependent function type (x: A) => T (or just A => T if x is not free in T).

Now, the [A] -> T form introduced in this PR can be understood as the dependent function type signature (A : *) => T in a hypothetical syntax where * is the type of types; so it's an instance of the second form, not the first –– it's really not a type lambda, it's the type of a type lambda.

Perhaps a more Scala-ish way of writing (A : *) => T would be (type A) => T or [type A] => T.

[sir-wabbit]

Why not

type Foo = [T <: AnyVal] List[T] => List[(T, T)]
val f = [T <: AnyVal] (x: List[T]) => x.map(e => (e, e))
foo([T] (x: T) => Some(x))
// or
foo(Some)

// Polymorphic *values* would be AMAZING:
val f: [T] List[T] = Nil
def runST[A](st: [S] ST[S, A]): A

-> looks confusing when mixed with => (precedence?) IMHO

The example in the gist looks incredibly cryptic:

val fmap: [A, B] -> (A => B) => [F[_]] -> F[A] => implicit Functor[F] => F[B] = 
  [A, B] -> (f: A => B) => ([F[_]] -> (fa: F[A]) => implicit (ev: Functor[F]) => fa.map(f))

// With different syntax it is readable:
val fmap: [A, B] (A => B) => [F[_]: Functor] F[A] => F[B] = 
  [A, B] (f: A => B) => [F[_]: Functor] (fa: F[A]) => fa.map(f)

[Blaisorblade]

@alexknvl Concrete syntax-wise, [A] T would be consistent with MethodTypes as pretty-printed today by Scala 2 and 3 — though that might be confusing if MethodTypes are still around as a distinct thing (maybe we could then change their syntax but that affects current error messages).

// Polymorphic values would be AMAZING:

Yes but they'd turn the design into two research problems. I'd love polymorphic functions, and probably the way to have them is to not make them depend on research-level problems (a bit like the SI-2712).

1. Pure polymorphic values would be cool, but "impure" ones are unsound (like polymorphic references in ML), how do you exclude them?
   -> Unless we managed to adapt ML's value restriction and use it for all polymorphic values, which I'm not sure we have considered — but that would interfere with nullary functions meant to be functions... EDIT: can't think this through now, feel free to figure out if this looks worthwhile.

class Box[T] { var x: List[T] = Nil }
def foo[X]: Box[X] = new Box[X] // a normal polymorphic method
val fooVal1: [X]Box[X] = foo // valid polymorphic value? what are the semantics? probably should be rejected somehow
val fooVal2: [X]Box[X] = new Box[X] // should also be rejected
def higherOrder[M[_]: Monad] = {
  val hoFooVal: [X]M[List[X]] = Nil.pure // should the compiler accept this? does `M[X]` contain say some `var bar: X`? How do we tell, should we refine M's kind to track mutability via some effect system?
}

(See #2500 (comment), one of the reasons that lead to #4670). So, that seems to involve an effect system, for which we don't have a good design yet.

2. A "natural" design for polymorphic values would arguably have yet other properties (such as forall X. F[X] <: F[T] for any T, proposed by @TomasMikula and also discussed in Language request: Add forAll quantifier / Make MethodTypes first-class #2500), but that's even more invasive in terms of required changes to the metatheory.

[smarter]

// With different syntax it is readable

This is tricky to get right. I'd like to add [T: Foo] -> A => B as syntactic sugar for [T] -> implicit Foo[T] => A => B, but that won't help in the fmap example, because [F[_]: Functor] -> F[A] => F[B] will be expanded to:

[F[_]] -> implicit Functor[F] => F[A] => F[B]

instead of:

[F[_]] -> F[A] => implicit Functor[F] => F[B]

which means the implicit search will be done before the type variable F has been constrained and won't succeed.

We could change the desugaring to be "add the implicit parameter just before the last occurence of =>" but that's not very satisfying since it means that in [T: Foo] -> A => B we will add the implicit parameter just before B, even if B is a type alias. Alternatively, the desugaring could use type information to decide where to put the implicit but that's likely to be extremely confusing for readers of the code.

[smarter]

which means the implicit search will be done before the type variable F has been constrained and won't succeed.

Alternatively, it may or may not be possible to delay the implicit search, I haven't tried to work out what that would entail.

[smarter]

Actually no, we can't delay the implicit search even if none of the type variables it references have been constrained, because sometimes the result of the implicit search is legitimately used to constrain type variables (as in https://milessabin.com/blog/2011/07/16/fundeps-in-scala/)

[LPTK]

@smarter at this point, why not just add a syntax much closer to method types, as @Blaisorblade proposed? We already have:

def foo(x: Int): T = t
foo: (x: Int) => T

So why not just go the extra mile and allow the same syntax/syntax sugar as in method definitions with respect to type parameters, currying and implicits? Let [A,B:T](a: A)(b: B) => C mean the same as the current [A] -> [B] -> (a: A) => (b: B) => implicit T[B] => C, which is arguably much less clear (as remarked by @alexander-myltsev).

This would also be a good time for changing the way method types are pretty-printed, as they are currently pretty inscrutable IMHO. (a: A)B does not look like a function-like type to me, and it got me confused when I was seeing this in compiler output as a beginner. It's also pretty hard to read when the A and B types get larger. I think (a: A) => B is much better, especially since it's a type users can write themselves.

[smarter]

Completely revamping the syntactic sugar for function types is out of scope for this PR, this should be a separate discussion. (In general I wonder if we shouldn't always have syntax discussions related to a proposal in a separate thread from the main discussion, since it tends to expand until there's no breathing room for anything else).

[LPTK]

@smarter unfortunately this seems to be true, and was remarked early on by Philip Wadler. For those who have not seen it yet:

  In any language design, the total time spent discussing
  a feature in this list is proportional to two raised to
  the power of its position.
       0. Semantics
       1. Syntax
       2. Lexical syntax
       3. Lexical syntax of comments

Feedback incorporated

[milessabin]

Looks like the CLA bot needs a poke ...

[smarter]

CLA bot breaks down when a commit has more than one author, you can ignore it.

[odersky]

From my side the only thing missing are updated syntax in syntax.md and in the parser's doc comments. Otherwise this is good to go.

[odersky]

E.g.

  lazy val StringBuilderType: TypeRef      = ctx.requiredClassRef("scala.collection.mutable.StringBuilder")
  def StringBuilderClass(implicit ctx: Context): ClassSymbol = StringBuilderType.symbol.asClass

But I meant to go over Definitions anyway, trying to avoid the duplication and make it safe by design. The problem with the lazy val pattern as you wrote it is that it would not work in interactive mode if PolyFunction was edited. Then
the system would hang on to the first version computed instead of the edited ones. I agree that's a rather esoteric use case. So we can leave it for now.

[smarter]

Otherwise LGTM too

[milessabin]

Feedback addressed ... I'll merge when it goes green unless anyone objects.

[milessabin]

Green now ... 🎉

[biboudis]

We lack documentation in the Reference > New Types section.

[aappddeevv]

Did any documentation on this ever get written? I did not see any on the dotty site or in github.

[smarter]

Nope, documentation will follow once the implementation is complete.

[aappddeevv]

Thanks. I had a specific and I think obvious need for this and AnyKind (if I understand these concepts correctly) working together. I'll hold off.

[SethTisue]

documentation will follow once the implementation is complete

is it time, now? This came up over at scala/scala-lang#1186 (comment) (Vincenzo's blog post on tuples)

[smarter]

I still need to do type inference. Anyway I agree documentation would be nice, but I don't have time to deal with that right now.

[nafg]

Sorry for mixing in, and if things need more time we need to give them more time, but developers, myself included, don't give documentation enough importance. In some ways, having good documentation is more important than anything else. What is the purpose of the whole Dotty effort? One objective is to make life easier for existing Scala developers but I think the most important goal is to make Scala accessible and speaking to a wider audience. From that perspective, good documentation helps achieve that with or without Dotty. Dotty should help tremendously but the extent to which it does again depends on quality of documentation. Honestly I'm not sure what specific thing is being discussed here (I get emails for all repo events) so doing take this as referring to anything or insinuating anything. Just wanted to write that. If it takes hiring people specifically to do documentation properly (even though it's already quite good) I hope they can.

…

On Tue, Dec 1, 2020, 11:08 AM Guillaume Martres ***@***.***> wrote: I still need to do type inference. Anyway I agree documentation would be nice, but I don't have time to deal with that right now. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#4672 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAAYAUG4X5Z3GO7B54ZXGRLSSUIGVANCNFSM4FFH6GZA> .