Choose Primitives for Typelevel and Meta Programming in Scala 3.0

[odersky]

Over the summer, we investigated a range of techniques to do typelevel and meta programming in
Scala.

• rewrite methods (used to be called transparent methods) Add transparent methods - untyped trees version #4616, Change in terminology for typelevel methods #4927.
• "typeof" Normalize TypeOf types (second step towards typed transparent methods) #4806, First steps to support dependent matches #4997
• match types Add match type #4964
• quote + splice + TASTY reflection (in master)

These are valuable experiments, but we still have to settle on a set of techniques to support in Scala 3.0. As always, we want a minimal set of constructs that covers the use cases we envision.

Use Cases

We classify use cases according to their priority.

High priority

These should definitely be supported:

1. As a minimal requirement, we want to do generic tuples of arbitrary size. These can used as building blocks for many other data-generic operations.
2. In particular, we want to support use cases arising in query languages (e.g., projections, joins). These should scale to large schemas with hundreds of columns.
3. We also want to provide good support in the area of typeclass derivation (which will probably need some other ingredients as well, which are not yet covered by the techniques discussed here).

Medium priority

These are "good to haves" if they are natural fits for the techniques we consider:

1. Sized data
2. Typed string interpolators

Low priority

These are probably out of scope for Scala 3.0, but might become interesting at some point in the future:

1. Refinement types
2. Theorem proving
3. Type providers

Concerns

To evaluate a combination of techniques, we should consider the following concerns.

1. Expressive and legible types,
2. Suitability for ensuring increased safety through type precision,
3. Separation of interfaces and implementatons, with support for separate compilation,
4. Avoid duplications between type level and term level,
5. Short compile times,
6. Efficient generated code,
7. Keep it simple and maintainable.

Note that some of these concerns conflict each other (e.g. 3/4).

Classification

A first classification of techniques is whether they support data generic programming through generic code, or/and whether they support specialization of code to specific types. Specialization is important for efficiency. The covered techniques support these as follows:

• data genericity: supported by match types, typeof, rewrite methods
• specialization: supported by rewrite methods, quote & splice

Evaluation

Quotes & splices are a given since they support blackbox macros and code introspection. My current tendency is to also take match types as a given. They are the only technique that ensures
separation between interface and implementation and they have better compile-time performance than the other techniques.

Match types can be combined with rewrite methods or typeof to achieve data genericity, but one might also use them with normal code, if we can come up with good typing rules that link match expressions with match types. So I believe further evaluation is needed whether match types should be complemented by some other typelevel technique, or whether they are good enough alone.

That leaves specialization. The minimalist standpoint here would be to use quote&splice for that, since we have it already. On the other hand, rewrite matches provide a lot of expressive power and convenience for specializing code (e.g. see how generic tuples can be specialized in #4964, file
library/src-scala3/scala/Tuple.scala). If we wanted to support that through quote&splice we'd need a rich semantic API that exposed the finer points of pattern matching. Or, alternatively, we keep rewrite matches in inlined code.

A Strawman Proposal

1. Keep and evolve match types
2. Implement typing rules so that a match expression can be checked to have a given expected match type.
3. Revert from rewrite methods to the preceding scheme for inlining.
4. Put inline after pickling, i.e. at the same time as ReifyQuotes which handles quotes and splices.
5. Keep the idea of rewrite matches (probably call them inline matches instead), which are executed at compile time in inlined code.
6. Keep some form of implicit matches but execute them at inlining time. That way, implicit matches can still compute implementations and prioritize between alternative implicits, but they cannot compute new types.

It's quite a bit of work, so we should discuss whether that's what we want before embarking on an implementation.

[odersky]

Why Drop Rewrite Methods?

Since I worked for much of the summer on rewrite methods, and pushed them to the point where they are now merged into master, I should explain why I now advocate dropping them.

Points in favor of rewrite methods:

• they are very powerful, can do generic programming and specialization in one abstraction.
• they avoid duplication between terms and types
• they lead to surprisingly simple code that can nevertheless produce complex types

However, there are also downsides:

• lack of separation of interface and implementation, since the implementation defines the type implicitly.
• complex implementation, since we need to serialize untyped trees and correlate typed and untyped versions in tricky ways.
• predictable typing relies on rewrite rules to be applied predictably, which is challenging. In practice, the system still feels fragile - one tends tries out some variations until something works.
• not-so-great performance since a lot of tree rewriting is involved, and tree rewriting is expensive (both asymptotically since it tends to lose sharing and in the constant factors).
• rewrite methods gain their power from inlining, which can lead to code explosion. This can be managed, but the question is whether typical users will know and apply the mitigations.

The main motivation to drop rewrite methods would be the adoption of match types. If we have match types, then rewrite methods become largely redundant. They overlap with match types in their generative aspects and they overlap with quotes&splices in their specialization power. Occam's razor then would suggest dropping them.

[Blaisorblade]

Match types can be combined with rewrite methods or typeof to achieve data genericity, but one might also use them with normal code, if we can come up with good typing rules that link match expressions with match types.

I mentioned in a meeting that these issues relates to GADTs — I ran into #4176 which is a partial example (tho not perfect) — it's a failed attempt to write length-indexed vectors with pure GADTs.

[odersky]

docs/reference/typelevel.md contains an informal spec for match types.

[arthurp]

Two questions from the unwashed masses:

1. Am I correct in understanding that the long term goal expressed here is to move meta-programming to match types for generating types and quoting/TASTY-trees and simple inlining for generating terms?
2. What is the current status of this plan? If I wanted to do some meta-programming in this framework, what features in master should I use and which should I avoid?

Thanks!

[biboudis]

Maybe we can close this now.

[abgruszecki]

Yeah, I think I'll just close this now.