Implement AppliedTermRef (singleton types for term-level applications) #3887

gsps · 2018-01-22T22:09:55Z

This PR implements AppliedTermRef, a singleton type representing a term-level application precisely. AppliedTermRefs are currently only introduced when they are stable, that is, when both the function and the arguments are.

The PR includes several additional changes to allow interaction and testing of AppliedTermRefs:

Previously no methods were marked stable, making it impossible to take advantage of the new singletons. As a starting point, we now mark methods on primitive value classes stable. Until an effect system capable of proving purity has landed, it might make sense to allow users to assume purity for user-defined methods (e.g. using an annotation).
Similarly to other precise types AppliedTermRefs are widened away unless specifically expected on declaration sites. This prompts the need for an explicit syntax of singleton types more complex than p.a.t.h.type. For this purpose we add an alternative syntax for singleton types: a type tree of the form { expr } is translated to the singleton type T of expr, provided that T is stable.

A simple example:

val x = 1
val y: {x} = x
implicitly[{x + 1} =:= {y + 1}]  // works

To Dos:

~~Bug: Missing denotation / NoType upon accessing underlying type of inter-parameter dependency.~~ Deferred. I suggest tackling this as a separate issue -- I think the problem lies in how parameter types are integrated into MethodTypes and existed before this PR, but afaict could not be exercised previously.
Implement translation of AppliedTermRef for sbt API extraction. Not sure how to proceed with this. Can we map AppliedTermRefs to existing xsbti.api.Trees, or do we need a new subclass?

dottybot

Hello, and thank you for opening this PR! 🎉

All contributors have signed the CLA, thank you! ❤️

Commit Messages

We want to keep history, but for that to actually be useful we have
some rules on how to format our commit messages (relevant xkcd).

Please stick to these guidelines for commit messages:

Separate subject from body with a blank line

When fixing an issue, start your commit message with Fix #<ISSUE-NBR>:

Limit the subject line to 72 characters

Capitalize the subject line

Do not end the subject line with a period

Use the imperative mood in the subject line ("Added" instead of "Add")

Wrap the body at 80 characters

Use the body to explain what and why vs. how

adapted from https://chris.beams.io/posts/git-commit

Have an awesome day! ☀️

gsps · 2018-01-24T12:06:18Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

@@ -861,6 +861,11 @@ object Parsers {
      }
    }

+    def emptyRefinementOrSingletonExpr(): Tree = {


Maybe call this refinementOfEmptyOrSingletonExpr().

gsps · 2018-02-04T21:08:44Z

Rebased on top of master, but the most recently merged PR (#3841) seems to interfere, as now the fromtasty version of the added test fails. Investigating.

Blaisorblade · 2018-02-12T15:33:17Z

Wow! Isn’t this supporting what OCaml calls applicative functors? That would be exciting news, I can elaborate why.

Do you also support type members of such applications? That would be a logical consequence.

To elaborate a bit (not sure if this will be clear): this would enable usable type members on implicits. Without such a feature, two separate occurrences of implicitly[Ord[(A, B)].FooTypeMember (assuming implicits foroa: Ord[A], ob: Ord[B], and implicit def ordPair[A: Ord, B: Ord]: Ord[(A, B)]) would not be compatible types, because they’re ultimately ordPair(oa, ob).FooTypeMember. (You’d also need a stricter type for implicitly, def implicitly[T](t: T): t.type = t, but this should work). If ordPair is marked as pure/stable, separate occurrences of implicitly[Ord[(A, B)].FooTypeMember would become type compatible.

For proper credit, this isn’t my idea: it goes back to a talk by Derek Dreyer in 2009, and I and Tillmann Rendel discussed applications to Scala a few years ago.

gsps · 2018-02-12T17:23:39Z

Indeed, this PR should enable applicative functors as in OCaml (though I have no experience with OCaml in that regard). I haven't written any test cases involving implicit search, specifically, but in principle that should work too. Feel free to play with the branch and let me know if it doesn't behave as you'd expect!

Blaisorblade · 2018-02-12T18:16:39Z

I should definitely do that! It’ll take me a while to get productive and be able to do this though — I’m already commenting on more issues I can look at seriously!

gsps · 2018-04-21T11:34:45Z

test performance please

dottybot · 2018-04-21T11:35:26Z

performance test scheduled: 1 job(s) in queue, 0 running.

dottybot · 2018-04-21T13:26:14Z

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/3887/ to see the changes.

Benchmarks is based on merging with master (f2bb231)

gsps · 2018-04-21T13:34:43Z

@liufengyun When I try to access the performance test results at http://dotty-bench.epfl.ch/3887/ I get a 404, any idea why?

Blaisorblade · 2018-04-21T15:06:45Z

@gsps That link works here now.

gsps · 2018-04-21T16:22:15Z

Right, now it works for me too, I guess there's some post-processing phase.

smarter

Your commit messages should contain a blank line between the subject and the body, see https://gist.github.com/robertpainsi/b632364184e70900af4ab688decf6f53 for example.

smarter · 2018-04-28T14:29:27Z

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

+            // Need to be more permissive when checking later phases, applications may have been rewritten
+            isSubType(tp1, tp2.resType)
+          case tp1: AppliedTermRef =>
+            tp1.args.size == tp2.args.size && isSubType(tp1.fn, tp2.fn) &&


sameLength(tp1.args, tp2.args)

smarter · 2018-04-28T14:30:12Z

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

+      case tp2: AppliedTermRef =>
+        def compareAppliedTerm = tp1 match {
+          case _ if !ctx.phase.isTyper =>
+            // Need to be more permissive when checking later phases, applications may have been rewritten


Can you give an example?

smarter · 2018-04-28T14:31:00Z

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

+            isSubType(tp1, tp2.resType)
+          case tp1: AppliedTermRef =>
+            tp1.args.size == tp2.args.size && isSubType(tp1.fn, tp2.fn) &&
+              (tp1.args zip tp2.args).forall(t => isSubType(t._1, t._2))


Slightly cleaner: (tp1.args, tp2.args).zipped.forall(isSubType)

smarter · 2018-04-28T14:34:08Z

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -561,6 +561,17 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
            false
        }
        compareTypeBounds
+      case tp2: AppliedTermRef =>


Any reason to have this in thirdTry and not firstTry? Also I think it'd be good to have more testcases that stress-test the subtype checks for AppliedTermRef. For example, what happens when an AppliedTermRef is hidden in a type alias?

We do have a test that relies on a type application:

val t: Id[{a + 1}] = a + 1

I'll also add one that relies on a simple alias.

smarter · 2018-04-28T14:36:06Z

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -148,6 +148,7 @@ object Types {
    /** Does this type denote a stable reference (i.e. singleton type)? */
    final def isStable(implicit ctx: Context): Boolean = stripTypeVar match {
      case tp: TermRef => tp.termSymbol.isStable && tp.prefix.isStable || tp.info.isStable
+      case tp: AppliedTermRef => tp.fn.isStable && tp.args.forall(_.isStable)


Aren't all AppliedTermRefs stable by definition?

I'd think they can't be stable if the arguments aren't stable; OTOH, I suspect AppliedTermRef with unstable arguments shouldn't be just unstable but illegal.

That's what I meant.

In principle f(unstableThing) is still meaningful, if you think of it as the image of f on set unstableThing. E.g., we could still type sign(impure()): 1.type where def impure(): PositiveInt. That being said, I think it's fine to just make AppliedTermRefs stable by construction for now, and I'll come back to this in my branch if I find a compelling use-case.

smarter · 2018-04-28T14:52:13Z

compiler/src/dotty/tools/dotc/core/tasty/TastyFormat.scala

@@ -416,6 +416,7 @@ object TastyFormat {
    METHODtype + implicitOffset + erasedOffset
  }

+  final val APPLIEDTERMREF = 180


Need to add this to the comment listing all tags at the top of this file and to bump the MinorVersion of TASTY. Also may need to add a case to TastyPrinter (To check if TastyPrinter is working correctly, enable "pickling" in Printers.scala)

smarter · 2018-04-28T14:54:44Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

@@ -863,7 +863,7 @@ object Parsers {
          makeTupleOrParens(inParens(argTypes(namedOK = false, wildOK = true)))
        }
      else if (in.token == LBRACE)
-        atPos(in.offset) { RefinedTypeTree(EmptyTree, refinement()) }
+        atPos(in.offset) { inBraces(emptyRefinementOrSingletonExpr()) }


If you're changing the grammar, it'd be nice to update the grammar comment above (and reflect the update in https://github.com/lampepfl/dotty/blob/master/docs/docs/internals/syntax.md)

smarter · 2018-04-28T14:55:45Z

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

@@ -60,6 +60,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
          homogenize(tp.ref)
        case AppliedType(tycon, args) =>
          tycon.dealias.appliedTo(args)
+        case tp: AppliedTermRef =>
+          homogenize(tp.underlying)


That seems pretty drastic to me, it means that AppliedTermRef will always be widened before being pretty-printed with -Ytest-pickler, so you may miss differences.

smarter · 2018-04-28T14:56:13Z

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

@@ -141,6 +143,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
        ParamRefNameString(tp) ~ ".type"
      case tp: TypeParamRef =>
        ParamRefNameString(tp) ~ lambdaHash(tp.binder)
+      case tp: AppliedTermRef =>
+        toTextRef(tp) ~ ".type"


shouldn't you wrap in { and } to reflect the syntax instead?

Indeed, though it does require some state to track when we hit the first AppliedTermRef. Is it okay to keep this kind of flag in PlainPrinter itself?

I guess so, we already have state for rectypes.

smarter · 2018-04-28T15:00:18Z

compiler/src/dotty/tools/dotc/sbt/ExtractAPI.scala

@@ -445,6 +446,9 @@ private class ExtractAPICollector(implicit val ctx: Context) extends ThunkHolder
        val apiTycon = apiType(tycon)
        val apiArgs = args.map(processArg)
        api.Parameterized.of(apiTycon, apiArgs.toArray)
+      case tp: AppliedTermRef =>
+        val apiTps = (tp.fn :: tp.args).map(apiType)
+        withMarker(combineApiTypes(apiTps: _*), appliedTermRefMarker)


Could you add an sbt scripted test to check that this is working properly? See https://github.com/lampepfl/dotty/tree/master/sbt-dotty/sbt-test/source-dependencies/by-name for an example.

LPTK · 2018-05-22T21:02:37Z

This is really exciting for the reason @Blaisorblade mentioned. It could help solve a long-lasting problem in Scala (and other languages with type classes but no dependent types).

I've just played a little bit with it, but my experimentation was hampered because of this:

scala> class Ord[A]
scala> implicit object io extends Ord[Int]
scala> implicit def lo[A](implicit ord: Ord[A]): Ord[List[A]] = new Ord
scala> val r: {lo(io)} = lo(io)
1 |val r: {lo(io)} = lo(io)
  |       ^^^^^^^^
  |       Ord[List[A]] is not stable
  |
  |       where:    A is a type variable which is an alias of Int

Is there currently a way (annotation) to tell Dotty that the lo function is stable, or this is yet to be added?

Also, it would be nice and generally more consistent if we could write type f(x).T instead of having to do {f(x)}#T.

gsps · 2018-05-22T21:16:27Z

There isn't in this branch, but the ptyper one has it, i.e., scala.annotation.assumePure. If you're feeling brave, https://github.com/gsps/dotty/tree/implement-ptype ;-) I noticed just recently that the REPL is somewhat broken, but I'm in the middle of the somewhat major change that is moving to dotty-compiled inox, so that'll have to wait a bit.

I agree on the syntax, and I'm not sure what would be the preferred notation here. It's a pity that in general we can't just use term-level syntax (without the curly braces) to denote singleton types, since the type and the term namespaces might clash.

LPTK · 2018-05-22T21:29:23Z

I agree on the syntax, and I'm not sure what would be the preferred notation here.

The thing is what comes before .T should be a stable term even in current Scala. So it makes sense to allow f(x).T as meaning {f(x)}#T. Syntax {f(x)}.T wouldn't be consistent.

Blaisorblade · 2018-05-24T09:55:35Z

It's a pity that in general we can't just use term-level syntax (without the curly braces) to denote singleton types, since the type and the term namespaces might clash.

We have a few exceptions, but they can be tricky to handle — Int => 1 is valid syntax, but it's hard for Dotty to always tell it's in fact a type and to not crash on class Foo extends Int => 1 (see #4487).

odersky · 2019-01-12T10:52:23Z

I believe if we want to revive this we need a decision on syntax, and a clear goal. For me the goal would be to implement applicative functors. But that should be fleshed out in detail first before we make a move on the underlying type structure. Otherwise we just increase entropy.

anatoliykmetyuk · 2021-07-27T13:54:00Z

There was no activity on this one for a long while, so let's close it.

dottybot reviewed Jan 22, 2018

View reviewed changes

gsps force-pushed the implement-appliedTerm branch 2 times, most recently from aa29fe1 to 41e3353 Compare January 24, 2018 11:15

gsps commented Jan 24, 2018

View reviewed changes

gsps assigned smarter and odersky Jan 24, 2018

gsps force-pushed the implement-appliedTerm branch 3 times, most recently from af18383 to 25d7675 Compare February 4, 2018 18:52

gsps force-pushed the implement-appliedTerm branch from 25d7675 to d585468 Compare February 4, 2018 22:40

gsps assigned OlivierBlanvillain Feb 9, 2018

gsps force-pushed the implement-appliedTerm branch from d585468 to 81b4c13 Compare March 9, 2018 15:26

gsps force-pushed the implement-appliedTerm branch 6 times, most recently from fd1d5d9 to 2715a53 Compare April 21, 2018 11:07

smarter reviewed Apr 28, 2018

View reviewed changes

LPTK mentioned this pull request Jun 25, 2018

Add transparent methods - untyped trees version #4616

Merged

smarter assigned gsps and unassigned smarter, odersky and OlivierBlanvillain Dec 10, 2018

odersky added the stat:on hold label Jan 12, 2019

gsps added 6 commits February 17, 2020 12:09

Add AppliedTermRef type

1e5e86a

Add curly-brace singleton type syntax for AppliedTermRef

6dcc75d

Subtyping, Stable primitives & cleaned-up creation of AppliedTermRef

1159370

Add AppliedTermRef pickling and (preliminary) pretty printing

058c673

Fix AppliedTermRef pretty printing

10e182b

Add existing tests and a new one inspired by recent issue

aa832f8

gsps force-pushed the implement-appliedTerm branch from 3396b0f to aa832f8 Compare February 17, 2020 16:25

gsps added 2 commits February 18, 2020 10:55

Fix homogenize and add TODO for summoning

0261183

Adapt check-init test to not fail on unrelated pure expression warning

aa67ec8

anatoliykmetyuk closed this Jul 27, 2021

OlivierBlanvillain mentioned this pull request May 16, 2022

Add compiletime.ops.string.CharAt #14431

Merged

Implement AppliedTermRef (singleton types for term-level applications) #3887

Implement AppliedTermRef (singleton types for term-level applications) #3887

Conversation

gsps commented Jan 22, 2018 • edited Loading

dottybot left a comment

Choose a reason for hiding this comment

Commit Messages

Choose a reason for hiding this comment

gsps commented Feb 4, 2018

Blaisorblade commented Feb 12, 2018

gsps commented Feb 12, 2018

Blaisorblade commented Feb 12, 2018

gsps commented Apr 21, 2018

dottybot commented Apr 21, 2018

dottybot commented Apr 21, 2018

gsps commented Apr 21, 2018

Blaisorblade commented Apr 21, 2018

gsps commented Apr 21, 2018

smarter left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smarter Apr 28, 2018 • edited by allanrenucci 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

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

LPTK commented May 22, 2018

gsps commented May 22, 2018

LPTK commented May 22, 2018

Blaisorblade commented May 24, 2018

odersky commented Jan 12, 2019

anatoliykmetyuk commented Jul 27, 2021

gsps commented Jan 22, 2018 •

edited

Loading

smarter Apr 28, 2018 •

edited by allanrenucci

Loading