Add dependent function types #3464

odersky · 2017-11-12T22:29:58Z

We now support dependent function types as long as there are no inter-parameter dependencies.
Assuming

class C { type T }

a dependent function type is written like this:

 (x: C) => x.T

It gets represented as a normal function type that approximates the result type together with a refinement that adds an apply method with the precise type. E.g. the type above would be represented as

Function1[C, C#T] { def apply(x: C): x.T }

~~For the moment, dependent function types cannot be implicit. Maybe we can lift that restriction in the future.~~

Dependent function types are important, because they are already in DOT, and they are probably a key feature to enable polymorphic effect systems.

nicolasstucki · 2017-11-13T16:12:44Z

We should have some neg tests for implicit dependent function types.

LPTK · 2017-11-14T15:04:19Z

This is great. Now we can almost have a nice first-class polymorphic lambda syntax.

> def baz(f: (t: C) => List[t.T] => List[t.T]): Int = 
    f(new C{type T = Int})(List(1,2,3)).head
> baz(t => (ls:List[t.T]) => ls.reverse)
res0: Int = 3

Unfortunately, we currently need to explicitly state the type of ls, and also the whole thing stops working when t is made implicit.

Ideally, is it reasonable to expect the following program to work?

def baz(f: implicit (t: C) => List[t.T] => List[t.T]): Int = f(new C{type T = Int})(List(1,2,3)).head
baz(ls => ls.reverse)

OlivierBlanvillain · 2017-11-14T10:21:23Z

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

+   */
+  def instantiateDependent(tp: Type, tparams: List[Symbol], vparamss: List[List[Symbol]])(implicit ctx: Context): Unit = {
+    val dependentVars = new TypeAccumulator[Set[TypeVar]] {
+      lazy val params = (vparamss :\ tparams)( _ ::: _)


It this equivalent to vparamss.flatten ::: tparams? I guess as order doesn't matter it would be (tparams :: vparamss).flatten

Both will not conserve the last param list in vparamss, this might be useful in all non type polymorphic methods with a single argument list ;)

(tparams :: vparamss).flatten is indeed much clearer.

OlivierBlanvillain · 2017-11-14T10:34:16Z

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

+        ParamRefNameString(tp) ~ ".type"
+      case tp: TypeParamRef =>
+        ParamRefNameString(tp) ~ lambdaHash(tp.binder)
+      case tp: SingletonType =>


I think something is wrong with the way dependent function types are printed:

scala> val depfun1: DF = (x: C) => x.m val depfun1: (C => ){apply: (x: C): } = <function1>

Should be fixed now.

OlivierBlanvillain · 2017-11-14T14:55:34Z

tests/pos/depfuntype.scala

+  // Reproduced here because the one from DottyPredef is lacking a Tasty tree and
+  // therefore can't be inlined when testing non-bootstrapped.
+  // But inlining `implicitly` is vital to make the definition of `ifun` below work.
+  inline final def implicitly[T](implicit ev: T): T = ev


Would changing implicitly to return ev.type instead of T help here?

The fact that adding inline changes how a method is typechecked doesn't seem like a great thing. I think @OlivierBlanvillain has some examples where it breaks working code.

I am a bit nervous about changing it to ev.type. The inferencer has to do major acrobatics to deal with implicit method types. It might interfere with something else. The current type of implicitly is simpler and clearer.

OlivierBlanvillain · 2017-11-14T14:57:16Z

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -1686,7 +1714,7 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
  }

  protected def makeImplicitFunction(tree: untpd.Tree, pt: Type)(implicit ctx: Context): Tree = {
-    val defn.FunctionOf(formals, resType, true) = pt.dealias
+    val defn.FunctionOf(formals, _, true) = pt.dealias.dropDependentRefinement


Since .dropDependentRefinement is always used after .dealias I guess the dealias could be pushed inside

OlivierBlanvillain · 2017-11-14T15:02:55Z

compiler/src/dotty/tools/dotc/typer/Typer.scala

+
+    args match {
+      case ValDef(_, _, _) :: _ =>
+        typedDependent(args.asInstanceOf[List[ValDef]])(


I'm a bit confused by this cast, args matches ValDef() and is casted to a List[ValDef]??

Oh I didn't see the ::

OlivierBlanvillain · 2017-11-14T15:17:56Z

compiler/src/dotty/tools/dotc/typer/Typer.scala

-      val (protoFormals, protoResult) = decomposeProtoFunction(pt, params.length)
+  def typedFunctionValue(tree: untpd.Function, pt: Type)(implicit ctx: Context) = {
+    val untpd.Function(args, body) = tree
+    val params = args.asInstanceOf[List[untpd.ValDef]]


Maybe type annotate args in the pattern above?

OlivierBlanvillain · 2017-11-14T15:19:38Z

tests/pos/depfuntype.scala

+  trait C { type M; val m: M }
+
+  type DF = (x: C) => x.M
+  val depfun1: DF = (x: C) => x.m


I like than both the type and the value have the same syntax :)

Yes. This is something that I really like about Scala in general.

smarter · 2017-11-14T23:17:03Z

compiler/src/dotty/tools/dotc/typer/Typer.scala

-      }
+    val funCls = defn.FunctionClass(args.length, isImplicit)
+
+    def typedDependent(params: List[ValDef])(implicit ctx: Context) = {


I would add a comment explaining to quickly describe what this function returns.

Tests indicate it's not needed anymore. Also: fix neg test error position.

For the moment we want to rule this out. There are quite a lot of bits we have to think through before we can allow this.

If the result type of a dependent function contains a type variable whose bounds refer to the function's parameters, that type variable has to be instantiated before the method type is formed. Otherwise, if the type variable is instantiated later the method result type will refer to the original parameter symbols instead of the method types ParamRefs.

`isFunctionType` nor returns true for dependent as well as non-dependent function types. `isNonDepFunctionType` returns true only for the latter.

The change that TermParamRefs are Singletons caused a change how they are printed, which this commit reverts. We had before def f(x: T): x.type def f(x: T): x.type # M Once TermParamRefs were singletons we got: def f(x: T): T (x) def f(x: T): x.M With this commit we now get: def f(x: T): x.type def f(x: T): x.M

The missing case was discovered after inlining `implicitly`. It produced a type mismatch in Ycheck after lambda lift.

Given a dependently typed function value like this one: def f: (x: C) => D => x.T => E we did not propagate information about the subsequent types `D` and `x.T` to the result type of the closure with parameter `(x: C)`. Doing so is a bit tricky because of the dependency. But it's necessary to infer the types of subsequent parameters. Test case: eff-dependent.scala

odersky requested a review from OlivierBlanvillain November 13, 2017 16:21

OlivierBlanvillain reviewed Nov 14, 2017

View reviewed changes

smarter reviewed Nov 14, 2017

View reviewed changes

odersky force-pushed the add-depfuns branch 2 times, most recently from 93bf1f8 to 07ab554 Compare November 15, 2017 17:32

nicolasstucki added the stat:needs rebase label Nov 24, 2017

odersky added 13 commits November 27, 2017 15:44

Add syntax for dependent function types

66b6280

Handle dependent function types in Typer

e31aa08

Drop AllowDependendFunctions mode bit

e15ebaa

Tests indicate it's not needed anymore. Also: fix neg test error position.

Fix typing of dependent closures

33869c3

Dependent function types may not be implicit

382e4ce

For the moment we want to rule this out. There are quite a lot of bits we have to think through before we can allow this.

Refine isFunctionType

5cb78bb

`isFunctionType` nor returns true for dependent as well as non-dependent function types. `isNonDepFunctionType` returns true only for the latter.

Implement implicit dependent function types

9b6d0c0

Add case for Inlined to TypedTreeCopier

9106bf1

The missing case was discovered after inlining `implicitly`. It produced a type mismatch in Ycheck after lambda lift.

Print dependent function types correctly in RefinedPrinter

1e753c3

Address reviewers comments

b6642e6

odersky force-pushed the add-depfuns branch from 07ab554 to 28a29ea Compare November 27, 2017 14:52

odersky merged commit 817fe72 into scala:master Nov 27, 2017

liufengyun deleted the add-depfuns branch November 29, 2017 15:57

Atry mentioned this pull request Dec 21, 2017

Cannot call a refined function that has a call-by-name parameter scala-js/scala-js#3232

Closed

LPTK mentioned this pull request Jan 22, 2018

Sketch of possible typelevel extension of principled metaprogramming #3844

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add dependent function types #3464

Add dependent function types #3464

odersky commented Nov 12, 2017 •

edited

Loading

nicolasstucki commented Nov 13, 2017

LPTK commented Nov 14, 2017 •

edited

Loading

OlivierBlanvillain Nov 14, 2017

nicolasstucki Nov 14, 2017

odersky Nov 15, 2017

OlivierBlanvillain Nov 14, 2017

odersky Nov 15, 2017

OlivierBlanvillain Nov 14, 2017

smarter Nov 14, 2017

odersky Nov 15, 2017 •

edited

Loading

OlivierBlanvillain Nov 14, 2017

OlivierBlanvillain Nov 14, 2017

OlivierBlanvillain Nov 14, 2017

OlivierBlanvillain Nov 14, 2017

odersky Nov 15, 2017

OlivierBlanvillain Nov 14, 2017

esarbe Nov 21, 2017

smarter Nov 14, 2017

Add dependent function types #3464

Add dependent function types #3464

Conversation

odersky commented Nov 12, 2017 • edited Loading

nicolasstucki commented Nov 13, 2017

LPTK commented Nov 14, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

odersky Nov 15, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

odersky commented Nov 12, 2017 •

edited

Loading

LPTK commented Nov 14, 2017 •

edited

Loading

odersky Nov 15, 2017 •

edited

Loading