Document polymorphic function types

Author: LPTK

docs/docs/reference/new-types/dependent-function-types.md

@@ -3,17 +3,16 @@ layout: doc-page
 title: "Dependent Function Types"
 ---
 
-A dependent function type describes functions where the result type may depend
-on the function's parameter values. Example:
+A dependent function type is a function type whose result depends
+on the function's parameters. For example:
 ```scala
 trait Entry { type Key; val key: Key }
 
 def extractKey(e: Entry): e.Key = e.key          // a dependent method
+
 val extractor: (e: Entry) => e.Key = extractKey  // a dependent function value
-//            ║   ⇓ ⇓ ⇓ ⇓ ⇓ ⇓ ⇓   ║
-//            ║     Dependent     ║
-//            ║   Function Type   ║
-//            ╚═══════════════════╝
+//             ^^^^^^^^^^^^^^^^^^^
+//             a dependent function type
 ```
 Scala already has _dependent methods_, i.e. methods where the result
 type refers to some of the parameters of the method. Method

docs/docs/reference/new-types/polymorphic-function-types.md

@@ -0,0 +1,48 @@
+---
+layout: doc-page
+title: "Polymorphic Function Types"
+---
+
+A polymorphic function type is a function type which accepts type parameters.
+For example:
+```scala
+// A polymorphic method:
+def foo[A](xs: List[A]): List[A] = xs.reverse
+
+// A polymorphic function value:
+val bar: [A] => List[A] => List[A]
+//       ^^^^^^^^^^^^^^^^^^^^^^^^^
+//       a polymorphic function type
+       = [A] => (xs: List[A]) => foo[A](xs)
+```
+Scala already has _polymorphic methods_, i.e. methods which accepts type parameters.
+Method `foo` above is an example, accepting a type parameter `A`.
+So far, it
+was not possible to turn such methods into polymorphic function values like `bar` above,
+which can be passed as parameters to other functions, or returned as results.
+
+In Dotty this is now possible. The type of the `bar` value above is
+
+```scala
+[A] => List[A] => List[A]
+```
+
+This type describes function values which take a type `A` as a parameter,
+then take a list of type `List[A]`, and return a list of the same type `List[A]`.
+
+[More details](https://github.com/lampepfl/dotty/pull/4672)
+
+### Relationship With Type Lambdas
+
+Polymorphic function types are not to be confused with
+[_type lambdas_](new-types/type-lambdas.md).
+While the former describes the _type_ of a polymorphic _value_,
+the latter is an actual function value _at the type level_.
+
+A good way of understanding the difference is to notice that
+**_type lambdas are applied in types,
+whereas polymorphic functions are applied in terms_**:
+One would call the function `bar` above
+by passing it a type argument `bar[Int]` _within a method body_.
+On the other hand, given a type lambda such as `type F = [A] =>> List[A]`,
+one would call `F` _withing a type expression_, as in `type Bar = F[Int]`.

docs/docs/reference/overview.md

@@ -107,7 +107,7 @@ These are additions to the language that make it more powerful or pleasant to us
  - [Enums](enums/enums.md) provide concise syntax for enumerations and [algebraic data types](enums/adts.md).
  - [Parameter Untupling](other-new-features/parameter-untupling.md) avoids having to use `case` for tupled parameter destructuring.
  - [Dependent Function Types](new-types/dependent-function-types.md) generalize dependent methods to dependent function values and types.
- - [Polymorphic Function Types](https://github.com/lampepfl/dotty/pull/4672) generalize polymorphic methods to dependent function values and types. _Current status_: There is a proposal, and a prototype implementation, but the implementation has not been finalized or merged yet.
+ - [Polymorphic Function Types](new-types/polymorphic-function-types.md) generalize polymorphic methods to dependent function values and types. _Current status_: There is a proposal, and a prototype implementation, but the implementation has not been finalized or merged yet.
  - [Kind Polymorphism](other-new-features/kind-polymorphism.md) allows the definition of operators working equally on types and type constructors.
  - [@targetName Annotations](other-new-features/targetName.md) make it easier to interoperate with code written in other languages and give more flexibility for avoiding name clashes.