Add TypeOf (first step towards transparent methods)

[gsps]

We ended up working around several limitations of the AnnotatedType infrastructure:

• First and foremost, we discovered that a custom kind of equality is required to (type-) compare TypeOfs: After typing some trees may have been transformed, e.g. certain Idents into TypeTrees, which in turn breaks the "naive" tree equality employed by AnnotatedType. Instead, we defined equality of TypeOf based on the top-level tree node: E.g., two TypeOfs with if as their top-level tree are equal if the types of their conds, thenbs and elsebs are.

• Similarly, we discovered that special handling is required for TypeOf in TypeMaps. One crucial aspect is that AnnotatedType would map over the underlying type and the tree separately, potentially causing the two to go out of sync. As an example, consider the following:

Let a: Boolean, b: Int, c: Int

                     .substBy(c.type, b.type)

{ if (a) b else c } +-------------------------> { if (a) b else b }

         +                                               +
         |                                               |
         |  .underlying                                  |  .underlying
         |                                               |
         v           .substBy(c.type, b.type)            v

b.type | c.type     +------------X------------>  b.type | b.type
= Int | Int                (doesn't hold)        = b.type
= Int

In other words, we can't rely on the lower path, so we instead propose to always derive the underlying type from the TypeOf's mapped-over tree (the top path).

• Similarly, without special handling, implementations of TreeAccumulator would actually ignore annotations. For instance, the dependency status of TermLambdas wouldn't take a TypeOf's tree into account, thus skipping some of the necessary substitutions. This can be fixed, of course, by making TreeAccumulator (or all of its relevant implementations) aware of annotations. Either way, making AnnotatedType work out of the box would require some additional investigation.

[dottybot]

.

[odersky]

test performance please

[odersky]

I added a comment to #4616 which tries to explore the solution space and some of the tradeoffs.

[OlivierBlanvillain]

@odersky I will try to address some of your concerns about TypeOf stated in this comment.

• It could be complex to guarantee that all type maps are applied correctly to terms.

• It's hard to keep terms in TypeOf and terms in the tree in sync under typemaps. To keep sharing, we have to deal with graphs instead of trees, and there is currently no infrastructure for that.

These two points vanish as soon as we stop caring about term and only focus on types. Indeed, once trees are lifted to types there is no need to "apply type maps to terms" or keep trees and types in sync, types are the source of truth on we are being normalized.

• It risks supporting not all of the term language (because of the complexity of doing so), which could lead to arbitrary restrictions what is supported and what is not.

This point is already addressed by the TypeOf where we lift everything to the type-level, but only give semantic to the following the subset of Scala expression made of if, pattern matchings and function calls. Everything else is, in a sense, still supported, but get lifted with its usual boring type. For instance, the following is a perfectly valid TypeOf type:

type Foo = {{
  case class Bar(i: Int)
  println(Bar(1))
  1 + 2
}}

But since we do not lift case class definition and side-effecting method calls in blocks, the above type is equal (and indistinguishable, from the point of view of all the infrastructure in typer) to the following:

type Foo = { 1 + 2 }

• It's potentially very costly to typecheck all the terms in the TypeOf types. It looks like a quadratic problem: Every subterm has another TypeOf type which largely shares the tree with the type of its children and parent. We need a way to exploit sharing to avoid the quadratic factor this implies.

The current implementation does not have any quadratic behavior and properly reuses the term level trees in the types. Everything is type-checked exactly once and lifted into a TypeOf when appropriate. I will try to illustrate the structure we have with an example. Suppose we are type checking the following term in a transparent context:

if (c1) (if (c2) t2 else e2) else e1

Type checking this term bottom up, typer will first assign the types of c2 t2 and e2:

if (c1) (if (c2: Boolean2) t2: B else e2: C) else e1

Then it will lift the if to the type level as follows:

if (c1) (if (c2: Boolean2) t2: B else e2: C): inner-if-type else e1

Where inner-if-type is the following type:

inner-if-type = TypeOf(underlying = Lub(B, C), tree = If(c2, t2, e2))

Where the B, C types and the c2, t2, e2 trees are pointers to the types and trees from the original if.

Type-checking then continues with e1: A, and c1: Boolean1 and finally hits the outer if:

{
  if (c1: Boolean2) (if (c2: Boolean2) t2: B else e2: C): inner-if-type else e1: A
}: outer-if-type

Where outer-if-type is the following type (with inner-if being a pointer to the inner if tree):

outer-if-type = TypeOf(underlying = Lub(inner-if, A), tree = If(c1, inner-if, e1))

[Blaisorblade]

For instance, the following is a perfectly valid TypeOf type:

So then

type Foo = {{
  case class Bar(i: Int)
  Bar(2)
}}

should get the usual type through avoidance and produce Any (or maybe Product with Serializable), right?

[OlivierBlanvillain]

@Blaisorblade I didn't try it, but this is what I would like it to be.

The point I was trying to make here is that even if some things do not make at the type-level, such as mutations and other side effects, the idea is that TypeOf types are able to capture everything, but will only make sense of a subset of the terms, namely if, pattern matching and function calls. Everything else is just "typed as usual", and that inferred type used as is on the type level. This is maybe better illustrated with var:

var i = 0

transparent def foo(j: Int) = {
  i += 1
  println(i)
  i + j
}

foo is transparent, so, even if absent from the source, it's return type is {{ i += 1; println(i); i + j }} which should be normalized to Int because of the instability of i.

[odersky]

It would be good to try to do the test cases in #4616: typelevel.scala, typelevel1.scala in this PR.

[odersky]

Here's a use case that seems hard for TypeOf but is easy if we reduce open terms.

  transparent def f(c: Boolean): Nat = {
    def g[X <: Nat](x: X): X = x
    g(if (c) Z else S(Z))
  }

  val f1 = f(true)
  val f2 = f(false)

The problem is that we need to prevent the type argument of g from being inferred as Nat. How can this be handled?

[Blaisorblade]

Based only on the formalization that I @gsps and @OlivierBlanvillain started sketching, I'd want X = if (c) Z else S(Z), which requires typing the argument transparently (as it arguably should). Since we call a non-transparent function, we then normalize this type — but if (c) Z else S(Z) is already normal. We didn't discuss this case, but one option seems that (since we're in a transparent body) the typer should produce g[if (c) Z else S(Z)](if (c) Z else S(Z)).
EDIT: does this make any sense?

[OlivierBlanvillain]

@Blaisorblade Yes, it makes sense, in this case the type argument of g should be inferred to be dependent. Currently dotc refuses to infer singleton types unless specified by the prototype. For instance:

def foo[X](x: X): X = x

foo(1)
// With -Xprint:front -Xprint-types:
// <<<Foo.foo:([X](x: X): X)>[Int]:((x: Int): Int)>(<1:Int(1)>):Int>
//                           ^ X = Int

This means that we need to adapt type inference to instantiate type parameters in transparent context to be as precise as possible.

[smarter]

Currently dotc refuses to infer singleton types unless specified by the prototype.

It does if you write [T <: Singleton]

[soronpo]

This means that we need to adapt type inference to instantiate type parameters in transparent context to be as precise as possible.

Also see discussion at scala/bug#10838

[OlivierBlanvillain]

Subsumed by #4806.